A Framework for Verifying the Conformance of Design to Its Formal Specifications

Dieu-Huong VU  Yuki CHIBA  Kenro YATAKE  Toshiaki AOKI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E98-D   No.6   pp.1137-1149
Publication Date: 2015/06/01
Publicized: 2015/02/13
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2014FOP0004
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
Keyword: 
formal specification,  design model,  formal verification,  model checking,  simulation relation,  

Full Text: PDF(1.6MB)>>
Buy this Article



Summary: 
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.