For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
A Framework for Verifying the Conformance of Design to Its Formal Specifications
Dieu-Huong VU Yuki CHIBA Kenro YATAKE Toshiaki AOKI
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2015/06/01
Online ISSN: 1745-1361
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
formal specification, design model, formal verification, model checking, simulation relation,
Full Text: PDF(1.6MB)>>
Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. The existing works focus on verifications where the specifications are described using temporal logics or using the same languages as that used to describe the designs. Our work considers cases where the specifications and the designs are described using different languages. To verify such cases, we propose a framework to check if a design conforms to its specification based on their simulation relation. Specifically, we define the semantics of the specifications and the designs commonly as labelled transition systems (LTSs). We appreciate LTSs since they could interpret information about the system and actions that the system may perform as well as the effect of these actions. Then, we check whether a design conforms to its specification based on the simulation relation of their LTS. In this paper, we present our framework for the verification of reactive systems, and we present the case where the specifications and the designs are described in Event-B and Promela/Spin, respectively. We also present two case studies with the results of several experiments to illustrate the applicability of our framework on practical systems.