タイトル（掲載誌）Research report (School of Information Science, Japan Advanced Institute of Science and Technology)
一般注記出版タイプ： VoR
Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. Existing works focus on the verifications where specifications are described using temporal logics or using the same languages as that used to describe designs. In this paper, we consider cases where specifications and designs are described using different languages. For verifying 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 specifications and designs commonly as labelled transition systems (LTS), and check if a design conforms to its specification based on the simulation relation of their LTS. In this paper, we present our framework specialized for the verification of reactive systems, and we present the case where specifications and the designs are described in Event-B and Promela/Spin, respectively. As a case study, we show an experiment of applying our framework to the conformance check of the specification and the design of OSEK/VDX OS.
リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/12069
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ