Checking the Conformance of a Promela Design to its Formal Specification in Event-B

Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. Existing works focus on verification tasks 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 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.