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

DOI Web Site 参考文献13件
  • VU Dieu-Huong
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • CHIBA Yuki
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • YATAKE Kenro
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • AOKI Toshiaki
    School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)

抄録

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.

収録刊行物

参考文献 (13)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ