JAIST Repository
https://dspace.jaist.ac.jp/

Title

Model Checking Conformance of Design Model to Its
Formal Specification

Author(s)Vu, Dieu‑Huong; Chiba, Yuki; Yatake, Kenro; Aoki,
Toshiaki

Citation

Research report (School of Information Science,
Japan Advanced Institute of Science andTechnology), IS‑RR‑2014‑001: 1‑18

Issue Date

2014‑04‑18

TypeTechnical Report

Text version

publisher

URL

http://hdl.handle.net/10119/12069

RightsDescription

リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）

Japan Advanced Institute of Science and Technology

Model Checking Conformance of Design Modelto Its Formal Specification
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
School of Information Science,
Japan Advanced Institute of Science and Technology{huongvd, chiba, k-yatake, toshiaki}@jaist.ac.jp

Abstract. 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 aredescribed in Event-B and Promela/Spin, respectively. As a case study,
we show an experiment of applying our framework to the conformancecheck of the specification and the design of OSEK/VDX OS.
Keywords: Specification, Design, Simulation Relation, Model Checking

1

Introduction

In a general process of software development, we start from informal requirements which target software is expected to satisfy. Such requirements are translated into formal specifications in order to describe them properly. We thendevelop system designs as models of implementations. Finally, we construct implementations based on the designs using programming languages. In this development process, it is expected that designs satisfy requirements described byformal specifications, because this allows incorrect designs to be revised before
significant investments are paid for actual implementations.
For verifying designs with respect to their specifications, existing works focus
on the cases 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 [17]. Specifically, we define the2semantics 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 ofreactive systems, and present the case where specifications and designs are described in Event-B [1] and Promela/Spin [9], respectively. Event-B is effective
for describing event driven systems, and Promela can also describe functionsof reactive systems as a set of (inline) functions. Figure 1 summarizes our approach. Firstly, we describe specification formally in Event-B model [19]. This
is to remove ambiguity and inconsistency in the specification which is written
in a natural language. Then, we generate execution sequences from this formal
specification. This is performed by a tool called execution sequence generator.
Execution sequences are represented as an LTS, and from each state, verification
conditions which must be met by the corresponding state of the design are generated. Finally, we apply model checking [3] to the design in combination withthe execution sequences to check the verification conditions. By this, we cancheck the correspondence of state transitions, or simulation relation, between
the execution sequences and the design. This ensures that the design conforms
to the specification.
Informal Specification
Specification
in Event-B

Design in Promela

Generate

Model Check
Simulation Relation

Execution Sequences

Fig. 1: Scenario for the formal verification of the design

In this paper, we present the formal definition of our framework, and as a casestudy, we show an experiment of applying our framework to the conformancecheck of the specification and the design of OSEK/VDX OS [15] (OSEK OS, forshort).
The paper is organized as follows: In Section 2, we show the definitions of
LTS and simulation relation. In Section 3 and 4, we present the definitions ofspecifications and designs, respectively. In Section 5, we present the definitionof our verification framework. In Section 6 and 7, we present a case study ofverifying OSEK OS, and discuss the effectiveness of our framework. In Section
8, we cite related work. In Section 9, we conclude this paper.

2

Preliminaries

In this section, we introduce the definitions of LTS and simulation relation.
First, we show the definition of LTS which is used to represent semantics ofspecifications and designs.
Definition 1. (LTS). A labeled transition system ( LTS, for short) is a tuple
hQ, Σ, δ, Ii where Q is a non-empty set of states, Σ is a set of actions, δ ⊆3

Q × Σ × Q is a transition relation, and I ⊆ Q is a set of initial states. We writea(p, a, p0 ) ∈ δ as p → p0 ∈ δ.
Then, we define n-steps transition relation.
Definition 2. (n-steps transition relation). Let M = hQ, Σ, δ, Ii be an LTS, Σ +the set of non-empty strings of Σ, and p and p0 states. We say p0 is reachable
a a2 ...an 0p ∈ δ + ),from p with respect to a string a1 a2 ...an ∈ Σ + by δ (denoted p 1 −→ai
a1
if there exist states p1 , p2 , ..., pn−1 ∈ Q such that p → p1 ∈ δ, pi−1 → pi ∈ δ foran 0p ∈ δ.
2 ≤ i ≤ n − 1, and pn−1 →Finally, we define the simulation relation based on the above definitions.
Definition 3. (Simulation relation). Let M1 = hQ1 , Σ1 , δ1 , I1 i and M2 = hQ2 ,Σ2 , δ2 , I2 i be LTSs, and f : Σ1 → Σ2+ a function from Σ1 to Σ2+ . Suppose a
relation ⊆ Q1 × Q2 is given. M 2 simulates M 1 with respect to  if for allaq1 , q10 ∈ Q1 , q2 ∈ Q2 , a ∈ Σ1 such that q1  q2 and q1 → q10 ∈ δ1 , there existf (a)q20 ∈ Q2 such that q10  q20 and q2 → q20 ∈ δ2+ . If M 2 simulates M 1 with respectto , we denote M 1M 2.

3

Specifications

3.1

Specification in Event-B

A reactive system is the system that responds to external events. A reactive system is captured as a collection of services which respond to the invocations fromthe outside. Event-B is the specification language which is useful to model theevent-driven systems like the reactive systems. Formal specification described in
Event-B is as a highly abstracted level description of the systems. This description mainly consists of state variables, operations on the variables, and stateinvariant. The variables are typed using set theoretic constructs such as sets,
relations, and functions. The events (operations) specify substitutions, whichallow both deterministic and nondeterministic state transitions. Figure 2 illustrates a part of the formal specification of OSEK OS described in Event-B: (i)the variables represent sets of entities managed by OSEK OS for instance tasks,
resources, and the ready queue; and (ii) the events describe system services suchas task activation, task termination, and resource getting. System services represent the interface between the operating system and the outside. Behavior of
events is described by value assignments to variables.
3.2

Formalization

We introduce the notion of models for specifications in our framework. Ourmodel of specifications is based on Event-B, but not restricted to it.
V is the set of variables. D is the domain, which is the set of values. Exp is theset of expressions in specifications. An expression may contain variables in V,
values in D, arithmetic operator, and set operators. BExp is the set of boolean

4

VARIABLES tasks, res, inr, evt, t_state, rdyQu, pri
INVARIANTS
ta,tb·ta tasks tb tasks tstate(ta)=run tstate(tb)=run ta=tb
EVENTS
activateTask =any twhere grd1 : t  tasks, grd2 : t_state(t) = susthen act1 : t_state(t) := Rdy, act2 : rdyQu := rdyQu  {t}endchainTask =any t1, t2
where grd1 : t1, t2  tasks, grd2 : t_state(t1) = run, grd2 : t_state(t2) = susthen act1 : t_state(t1) := sus, act2 : t_state(t2) := rdy, act3 : rdyQu := rdyQu  {t2}endFig. 2: A specification of OSEK OS in Event-B

expressions (BExp ⊂ Exp). A substitution is a mapping from V to Exp. We
note that value assignments are also substitutions because D ⊆ Exp. ACT isthe set of substitutions for specifications. A guard is a boolean expression. GRD
is the set of guards. An event is a pair hg, ai of a guard g and a substitution a.
E is the set of events. If e = hg, ai then we write grd(e) = g and act(e) = a. A
state is a value assignment. [exp]σ denotes the interpretation of the value of an
expression exp in a state σ. We say a guard g holds in a state σ iff [g]σ = tt. Init
is the initialization, which is the set of events whose guards hold for any stateseand actions are value assignments. We denote σ −→ σ 0 for an event e = hg, ai
00
and states σ and σ if σ(g) holds and σ = {v 7→ [a(v)]σ | v ∈ V }.
Sematics of specifications is provided by specification models.
Definition 4. (Specification models). A specification model is a tuple S =hVS , DS , ΣS , InitS , Invi where VS ⊆ V is the set of variables used in S, DS ⊆ D
is the domain in S, ΣS ⊆ E is the set of events defined in S, InitS ∈ Init
is the initialization of S, and Inv ∈ BExp is the invariant of S. An LTS derived from the specification model S is defined as MS = hQS , ΣS , δS , IS i wheree
QS = {σ | σ : VS → DS }, δS = {σ −→ σ 0 | σ, σ 0 ∈ QS , e ∈ ΣS }, andIS = {act(e) | e ∈ InitS }.

4

Designs and Environments of target system

4.1

Design in Promela

In Promela, service functions of reactive systems can be described by using
inline functions. The left hand side of Figure 3 illustrates a design of OSEK
OS. We call this model a design model. It is constructed based on the informal
specification of OSEK OS and described in about 2800 lines of Promela code,
according to the approach in [2]. It first defines data structures such as tsk,
res, and ready which represent an array of tasks, an array of resources, andready queues, respectively. Following these data structure, a set of functions aredefined. For example, _ActivateTask and _TerminateTask are the functions toperform activation and termination of tasks, respectively.
Since a reactive system only defines a set of functions, it cannot operate byitself. To operate it, we need an environment which calls functions to the reactive
system. In the case of operating systems, an environment means a software

5

typedef TCB {int id, pr, dpr, }typedef RCB {int id, pr, tid, }TCB tsk[5];
RCB res[5];int ready[25];inline _schedule() { }inline _DeclareTask(tid, pr) { }inline _ActivateTask(tid) { }inline _ChainTask(tid, id) { }inline _TerminateTask(tid) { }inline _GetTaskState(tid) { }typedef Taskinfor { }Taskinfor tsk1, tsk2, tsk3;/* Invocations */_DeclareTask(tsk1.id, tsk1.pr1);_DeclareTask(tsk2.id, tsk2.pr2);_DeclareTask(tsk3.id, tsk3.pr3);_ActivateTask(tsk1.id);_ChainTask(tsk1.id, tsk2.id);_ChainTask(tsk2.id, tsk3.id);_ActivateTask(tsk2.id);_TerminateTask(tsk3.id);_TerminateTask(tsk2.id);_ActivateTask(tsk3.id);

Fig. 3: A design model of OSEK OS and its environment in Promela

application running on it. The right hand side of Figure 3 shows an example of anenvironment for the OSEK OS design. We call this model an environment model.
It first defines entities in the environment such as tasks and resources. Then, it
defines a sequence of function calls to the OSEK OS. By combining the designand environment, we can make a closed system which can operate by itself. We
call this model a combination model. In terms of Promela, a combination model
can be obtained by including the Promela code of the design into that of theenvironment model. As we explain later, an environment model is constructedfrom the specification model, and input to Spin to check simulation relation.
4.2

Formalization

P is the set of parameters (function arguments). A parameterized expression
may contain constants, variables, parameters and arithmetic operators. The setof parameterized expression is denoted as PExp. A p-substitution (function body)
is a mapping from V to PExp. The set of p-substitution is denoted as PSubst. Id
is the set of identifiers (used as function names). For the simplicity, we assume
that functions has only one parameter. Design models are defined as follows.
Definition 5. (Design model). A design model is a tuple D = hVD , DD , PD , F,
ΣD , ID i where VD ⊆ V is the set of variables used in D, DD ⊆ D is the domain of
D, PD ⊆ P is a finite set of parameters for D, F is a set of function identifiers
defined as F = {id(p) | id ∈ Id, p ∈ PD }, ΣD is a relation such that ΣD ⊆F × PSubst, and ID ⊆ {σ | σ : VD → DD } a set of value assignments from VD
to DD .
Environment models are defined as follows.
Definition 6. (Environment model). An environment model for a design model
D is a tuple E = hVE , DE , ΣE , IE i where VE ⊆ V is a set of variables used in E,
DE = DD is the domain of E, ΣE is a set of invocations to D such that ΣE ⊆{id(v) | id ∈ Id, v ∈ VE }, and IE is a set of value assignments from VE to DD . An
LTS derived from the environment model E is defined as ME = hQE , ΣE , δE , IE i
where QE = {σ | σ : VE → DE }, δE ⊆ QE × ΣE × QE , and IE ⊆ QE .
A combination of a design and an environment describes the execution of
the design according to the environment. An expression in combination contains

6

constants from D, variables in V, and arithmetic operators. The set of expressions
in combinations is denoted as Exp0 . A substitution for combinations is a mappingfrom V to Exp0 . The set of substitutions for combinations is denoted as SubstDE.
For a mapping π from P to V and a parameterized expression pexp ∈ PExp,
pexpπ is the result of replacing each parameter p appearing in pexp by π(p).
Combination models are defined as LTS as follows.
Definition 7. (Combination model). Let D = hVD , DD , PD , F, ΣD , ID i be a design model and E = hVE , DE , ΣE , IE i an environment model.
id(v)1. We denote σ −→ σ 0 for an invocation id(v) ∈ ΣE and states σ and σ 0 if
there exist (id(p), a) ∈ ΣD and a mapping π : PD → VE such that π(p) = v
and σ 0 = {v 7→ [a(v)π ]σ | v ∈ VD ∪ VE }.
2. The combination model of D and E (denoted as D·E) is an LTS hQD·E , ΣD·E ,δD·E , ID·E i where QD·E is the set of value assignments from VD ∪ VE to Did(v)( states for the combination model), ΣD·E = ΣE , δD·E = {σ −→ σ 0 | σ, σ 0 ∈QD·E , id(v) ∈ ΣE }, and ID·E = ID ∪ IE is the set of initial states of D andE.

5

Verifying Simulation Relations by Model Checkers

In this section, we present an approach for checking designs against their formal
specifications based on simulation relations. We first present an overview, then,we present formal definitions.
5.1

Overview

In our framework, the initial inputs are pairs of formal specifications and designs of reactive systems. Suppose that M1 and M2 be two LTSs. We define M2
simulates M1 based on semantics of LTSs by extending the given relation on thestates. The states are value assignments which are mappings from the variables
to the values. Therefore, the relation on states of M1 and those of M2 are established based on mappings R and C where R is the mapping from variablesof M1 to those in M2, C is the mapping from values in M1 to those in M2. The
left hand side of Figure 4 shows a relation between state p of M1 and state q ofM2. p relates to q based on R and C because u = sus in state p corresponds tov = 1 in state q with mappings R(u) = v and C(sus) = 1. M2 simulates M1 if
for each transition in M1 from state p to state p0 and p relates to state q of M2,
there exists state q 0 and a corresponding transition in M2 from q to q 0 such thatp0 relates to q 0 . In the right hand side of Figure 4, a line arrow connecting p to
p0 represents a one-step transition from p to p0 , and a dashed arrow connecting
q to q 0 represents an n-step transition from q to q 0 . To check whether M2 simulate M1, we check if there exists a reachable state q 0 from q such that v = 2
corresponding to u = rdy in p0 with mappings R(u) = v and C(rdy) = 2.
Figure 5 shows steps to verify the simulation between a specification and adesign using model checkers Spin: (step 1) Giving bounds for the verification

7[u=sus][u=sus][u=rdy]

p

p

p'

M1

R(u)=v,C(sus)=1
M2

R(u)=v,C(sus)=1

R(u)=v,C(rdy)=2

q

q

q'

[v=1]

[v=1]

[v=2] ?

Fig. 4: Simulation Relationand generate execution sequences from Event-B specification within the bounds,(step 2) Generating environments of the target system and assertions from theexecution sequences and the given mappings between elements in the design andthose in the specification, and (step 3) Model checking simulation relation in
Spin.
Mappings
Specification
in Event-B
BoundsExecution
Sequence
Generator

Execution
Sequences

Designin Promela
Promela Code
Generator

Environment

Spin Model Checker

Assertions

Fig. 5: Checking simulation relation of the design and its formal specification (steps)

Giving Bounds In a specification, there may be infinitely many states andtransitions of target system because variables in Event-B obtain values in unbounded domains. Model checking does an exhaustive check of the system. It
needs a representation of the system as a finite set of all possible states. So,
abstract types in Event-B must be replaced by concrete types. Also, types haveinfinite ranges of values like Int and Nat must be restricted as finite ranges.
By such restriction, the state space and the set of transitions explored from
Event-B specification become finite sets. This makes the LTS explored from thespecification finite. We define such restrictions as bounds of the verification.
Generating execution sequences from specification In order to generate
execution sequences, or LTS, from the specification and bounds, the generator
computes all possible transitions and reachable states. Every computed statemust satisfy the invariant. Started at the initialization, the generator enumerates all possible values for the constants and variables of the specification thatsatisfy the initialization and the invariant to compute the set of initial states.
To compute all possible transitions from a state, the generator finds all possible
values for event parameters of an individual event to evaluate the guard of thatevent. If the guard holds in the given state, the generator computes the effect of
the event based on substitution of that event. When new states are generated,
we repeat this process to these states until no new states are generated.
Generating Evironment In order to verify that designs simulate their formal
specifications, environments of the target systems are constructed and combined

8with designs. As the result of such combination, we obtain combination models
which become the inputs of model checkers. Since environments trigger specificbehavior of designs by calling functions to the design, we construct environmentsby representing possible behavior described in their specifications. For this, we
generate execution sequences as an LTS from the specification and generate theenvironment by translating the LTS into Promela. The LTS represents possible
execution sequences of the specification within the input bounds as illustrated
in Figure 6(a)).
typedef Taskinfor { }Taskinfor tsk1, task2, task3;_DeclareTask(task1.id, task1.pr1);_DeclareTask(task2.id, task2.pr2);_DeclareTask(task3.id, task3.pr3);s0:
s0:(sus,sus,sus)
if:: _ActivateTask(task1.tid) -> goto s1;
AT(t1)
AT(t2)
Translation:: _ActivateTask(task2.tid) -> goto s2;
intos1:(run,sus,sus) s2:(sus,run,sus)
Promela :: _ActivateTask(task2.tid) -> goto s3;
codefi;
AT(t2)
AT(t3)s1:
if
s3:(run,rdy,sus) s4:(sus,rdy,run):: _ActivateTask(task2.tid) -> goto s4;:: _ActivateTask(task3.tid) -> goto s5;
TT(t3)
CT(t1,t3):: _TerminateTask(task1.tid) -> goto s0;s5:(sus,sus,run):: _ChainTask(task1.tid, task2.tid)-> goto s2;:: _ChainTask(task1.tid, task3.tid)-> goto s3;
CT(t2,t3)TT(t3)fi;s6:(sus,run,sus)...
AT: _ActivateTask, CT: _ChainTask, TT: _TerminateTask
t1: task1.tid, t2: task2.tid, t3: task3.tid

(a)

(b)

Fig. 6: Generation of environment from LTS

In Figure 6(a), the rectangles represent the states and the labeled arrows
represent the events that are enabled in each states. For example, three events
AT(t1), AT(t2), and AT(t3) are enabled in state s0, and five events TT(t1),AT(t2), AT(t3), CT(t1,t2), and CT(t1,t3) are enabled in state s1. In ourframework, the states are defined as the value assignments; however, we show
them here as values, e.g. (sus, sus, sus), for readability.
The LTS is translated into the environment (e.g. from (a) to (b) of Figure6). For this translation, we define a mapping from the events in the LTS to
the function calls in the environment. In general, it is one-to-many mapping;
however, in the case of reactive systems like OSEK OS, it is one-to-one mapping.
For example, in the sample case, we map the event ActivateTask(t1) in the
LTS to a function call _ActivateTask(task1.tid) in the environment. The
states and transitions in the LTS are represented by labels and if-statementsin the environment. The combination between the design and the environment
becomes a direct input to the model checker in step 3 of the framework.

Generating Assertions The desirable behaviors of the target system obtained
from the Event-B specification are encoded in imperative assertion statements
which will be added into appropriate locations in the environment and justified
by Spin model checker. Assertions are generated using the mapping R from thevariables in the specification to those in the design, and the mapping C fromthe values in the specification to those in the design.

9

Assertions represent the constraints on the simulation relation between thespecification and the design. In Figure 7, the above illustrates an execution
sequence explored from specification and the below illustrates that of the design.
Here, t, u are variables, and sus, rdy, run, wait are values, which are defined in
the specification. a, b are variables, and 1, 2, 3, 4 are values, which are definedin the design.
Value of variables in states p0 , p1 , p2 , · · · of the specification are evident
from the LTS. Value of variables in state q0 of the design is assigned evidently.
It is obvious that q0 relates to p0 because values of variables in these two statespreserve given R and C. However, the other states q1 , q2 , · · · reached from q0
are not evident. We use a model checker to explore these states of the design andcheck whether q1 , q2 , · · · relate to p1 , p2 , · · · , respectively. In order to ensure
the simulation relation, for example for state q1 , we expect that a = 2 and b = 1
to comply with R(t) = a, R(u) = b, and C(sus) = 1, C(rdy) = 2. Hence, inorder to check if q1 relates to p1 , an assertion for state q1 is defined by a = 2
and b = 1. Such assertions are automatically generated from the interpretationsof states explored from the specification (step 2 of the framework), and they areembedded in the corresponding states of the environment as an assert statementof Promela.

Mappings:

R(t)=aR(u)=bC(sus)=1
C(rdy)=2
C(run)=3C(wait)=4[u = sus][t = sus]p0[u = sus][t = rdy]p1[u = rdy][t = rdy]p2

q0[a = 1][b = 1]q1[a = 2][b = 1] ?

q2[a = 2] ?
[b = 2]...

...

Fig. 7: Execution sequences of specification and design

Checking of simulation relation In the last step, we input the combination
model and the assertions to Spin to check the simulation relation of the specification and the design. If no counter example is found, then we say the design
conforms to the formal specification within the input bounds.
5.2

Formalization

We now give formal definitions of the relation between states, the bound, simulation relation of two LTSs within the given bound, and steps in the framework.
Definition 8. (Relation between states). Let S = hVS , DS , ΣS , InitS , Invi be a
specification model, MS = hQS , ΣS , δS , IS i the LTS derived from by S, D =hVD , DD , PD , ID(PD ), ΣD (PD ), ID i a design model, E = hVE , DE , ΣE , IE i anenvironment model for D, and D·E = hQD·E , ΣD·E , δD·E , ID·E i the combination
model of D and E. We say a state σD·E ∈ QD·E relates to a state σS ∈ QS basedon mappings R : VS → VD and C : DS → DD (denoted σS R,C σD·E ), if forany x ∈ VS and y ∈ VD , R(x) = y implies C(σS (x)) = σD·E (y).

10

It is obvious that R,C is a relation between the states. We omit R and C
from R,C if they are clear from the context.
Definition 9. (Bounds). Bounds for LTS hQ, Σ, δ, Ii are defined as a pair B =hG, Hi of mappings G and H where G : 2Q → 2Q , G(Q) ⊆ Q, and Q0 ⊆ Q00
implies G(Q0 ) ⊆ G(Q00 ) and H : Q × Σ → {tt, f f } and for any state p ∈ Q,
there exist finitely many actions a ∈ Σ such that H(p, a) = tt.
For specifications in Event-B, we set bounds for range of values that variables
can obtain to finite sets. By this restriction, the state space and the set of events
applicable in each state become finite. We give mapping X for implementing
such bounds to generate LTSs. X is mapping from variables to finite sets ofvalues. We use ESX (σ) to denote the set of all events which are applicable to σ
and satisfy restrictions defined by X.
Suppose S = hVS , DS , ΣS , InitS , Invi be a specification model and hQS , ΣS ,
δS , IS i a LTS derived from S. With the mapping X, we define mappings G and
H as follows: G(QS ) = {σ ∈ QS | ∀v ∈ VS .σ(v) ∈ X(v))}, G(IS ) ⊂ G(QS ),and H(σ, e) = tt iff e ∈ ESX (σ).
Definition 10. (Bounded LTS). An LTS obtained by restricting an LTS M =
b Ii,
b Σ,
b δ,
b where Qb=hQ, Σ, δ, Ii by bounds B = hG, Hi is defined as M ↓B = hQ,a0bbG(Q), Σ = {a | ∀p ∈ Q, a ∈ Σ, H(p, a) = tt}, δ = {p −→ p ∈ δ | H(p, a) = tt},and Ib = G(I).
Definition 11. (Simulation relation of two LTSs within bounds). Let M1 andM2 be two LTSs, and B be bounds. The simulation relation of M1 and M2 withinbounds B is defined as M1 B M2 if M1 ↓B  M2 . If M1 B M2 holds, we say
M2 satisfies M1 within B.
Generating execution sequences from specification The algorithm tocompute execution sequences from a specification model is presented in (Algorithm 1). Inputs of the algorithm are a specification model S, and bounds B =hG, Hi which is implemented by X. Output is a bounded LTS. The algorithm
uses two data structures: QU EU E storing reachable states, and V ISIT ED storing visited states. It uses two routines to access QU EU E: Push(QU EU E,hσi)
adds state σ as an element into QU EU E, Pop(QU EU E) returns the head of
QU EU E. In each step of while loop, one state is removed from QU EU E, andreachable states from the state are computed. The algorithm terminates when
QU EU E becomes an empty set.
Generating Environments An environment is generated from the LTS of a
specification model. First, we define correspondence of states between the specification and the environment. Let S = hVS , DS , ΣS , InitS , Invi be a specification
model, MS = hQS , ΣS , δS , IS i the LTS derived from S, E = hVE , DE , ΣE , IE ian environment model, and ME = hQE , ΣE , δE , IE i the LTS derived from E.
We say a state σE ∈ QE corresponds to a state σS ∈ QS based on mappings

11

b Ii
b Σ,
b δ,
b from S and X where B = hG, Hi,
Algorithm 1 Generating S↓B = hS,
G(QS ) = {σ ∈ QS | ∀v ∈ VS .σ(v) ∈ X(v))}, G(IS ) ⊂ G(QS ), and H(σ, e) = tt
iff e ∈ ESX (σ))
1: QU EU E = empty
2: V ISIT ED = empty
3: Sb = emptyb = empty
4: Σb
5: δ = empty
6: Ib = empty
7: for each σ0 ∈ G(IS ) do
8:
Push(QU EU E, hσ0 i)
9:Sb = Sb ∪ {σ0 }10:Ib = Ib ∪ {σ0 }11: end for
12: while QU EU E 6= empty do
13:
hσi = Pop(QU EU E)
14:
V ISIT ED = V ISIT ED ∪ {σ}b = {e | H(σ, e) = tt}
15:
E
b 6= empty then
16:
if E
b do
17:
for each event e = (g, a) ∈ E
18:
σ 0 = {v 7→ [(act(e))(v)]σ |v ∈ VS }19:
if σ 0 6∈ V ISIT ED then20:
Push(QU EU E,hσ 0 i)
21:
Sb = Sb ∪ {σ 0 }22:
end ifb=Σ
b ∪ {e}23:Σe24:
δb = δb ∪ {σ → σ 0 }25:
end for26:
end if
27: end while
28: return S↓B

R0 : VS → VE and C : DS → DD (denoted σS R0 ,C σE ), if for any x ∈ VS andy ∈ VE , R0 (x) = y implies C(σS (x)) = σE (y).
Then, we define correspondence between events in the specification and functions in the design. For the target is a reactive system, this is defined by a mapping f : ΣS → ΣD·E . This means that an event in the specification corresponds
to a function call in environment.
Finally, we define an LTS for the environment model E based on the specification S as ME = hQE , ΣE , δE , IE i where QE = {σE | ∃σS ∈ QS , σS R0 ,C σE }a00, ΣE = {a | a ∈ F, ∃e ∈ ΣS , f (e) = a}, δE = {σE −→ σE| σE , σE∈000QE , a ∈ ΣE , ∃σS , σS ∈ QS , σS R0 ,C σE , σS R0 ,C σE }, and IE = {σE |∃σS ∈ IS , σS R0 ,C σE }.

12Generating Assertions The relation on states between the LTS of specification model and the combination model is given based on the mappings
R : VS → VD and C : DS → DD . Verification conditions are generated asfollows:
1. Forof the combination, the assertion is:
V initialization0(σDE(y) = C(σS0 (x))) (y = R(x)),
x∈VS0
2. For all (reachable) states σS , σS0 ∈ QS and σD·E , σD·E
∈ QD·E such thatef (ei )

i
+
0
0
σS −→
−→ σD·E∈ δD·E, and σS R,C σD·E , the assertion
V σS ∈0 δS↓B , σD·E
0is
(C(σS (x)) = σD·E (y)) (y = R(x)).

x∈VS

After this step, these conditional expressions are defined as inputs of model
checkers. During the execution of the combination, the model checker will verify
the reachable states of the combination against these conditions. At the end of
the verification, one therefore can conclude that for any reachable state σS of thespecification within the given bounds, there exists a reachable state σD·E of the
combination such that σS R,C σDE . As a result, the verification of simulation
between the design and the specification has completed within the bounds.

6

Case study

We implemented our framework as a generator that produces (i) the LTS of thebounded specification, (ii) the environment in Promela, and (iii) the assertions.
As an application of our framework to a practical system, we conducted anexperiment to verify that a design of OSEK OS in Promela conforms to its
formal specification in Event-B. We have illustrated these two models partiallyin Figure 3 and Figure 2.
Firstly, bounds are set for the verification by restricting range of values forevery variables in Event-B specification. As shown in Figure 2, variables tasks,
res, evt, and inr define entities managed by OSEK OS such as tasks, resources,
events, and interrupt routines; variable pri defines the priority assigned to tasks,
resources, and interrupt routines; and variable t state defines the task state.
Table 1 illustrates examples of the bounds in which each row shows values ofthe bounds that can be used in separate experiment. Here, because of the space
limitation, we show restricted ranges of values for tasks, pri, res, evt, and inr,
respectively.
According to our framework, we can set ranges so that they contain different
entities such as tasks, resources, events, and interrupt routines as example No.3
of Table 1. In our experiments, we perform separate experiments in which somecases deal with distinct groups of system services of the target system; the othercases check the relation between different groups. This helps us to avoid thestate explosion but preserve important behavior of the target system.
All experiments are conducted on an Intel(R) Core(TM) i7 Processor at
2.67GHz running Linux. Verification results outputted by Spin are shown in13
Table 1: Examples of the bounds
No. Restricted Ranges for tasks, pri., res., evt., inr.
1 {t1, t2}, {1, 2}, {}, {}, {}2 {t1, t2}, {1}, {}, {evt1}, {}, {}3 {t1, t2, t3}, {1, 2, 3, 6, 4, 7}, {res1}, {evt1}, {inr1, inr2}
4 {t1, t2}, {1}, {res1}, {}, {}5 {t1, t2}, {1}, {evt1}, {}, {}6 {t1, · · · , t9}, {1}, {}, {}, {}7 {t1, · · · , t10}, {1}, {}, {}, {}8 {t1}, {1}, {}, {}, {}Table 2. Here, the first column (“No.”) represents experiment number. The next
column presents size of ranges for variables task, pri, res, evt, and inr. Values
in this column express bounds of the verification. Column “LTS Generation”
shows statistic of the execution sequence generator. Here, columns “#State”,
and “#Trans” present the number of distinct states and that of transitions
appearing in the execution sequences; column “Time” present the time taken(s) for the generation. Column “Model Checking” presents statistic of the model
checker including total actual memory usage √for distinct verification, the time
taken (s), and the verification result in which indicates the successful result neither error returned. As mentioned in Section 3, groups of system services of
OSEK OS are task management, resource management, event mechanism, andinterruption management. In the table, experiments No.1-No.15 are performed
to check the task management of OSEK OS. In these cases, we set ranges fortasks and pri. Experiments No.16-No.20 are performed to check relation between
task management, resource management, event mechanism, and interruption
management; therefore, we set ranges for task, pri, res, evt, and inr. Since
OSEK OS schedules the tasks based on task priorities, it behaves differently
with different patterns of assignment of task priorities. The best scenario toensure that every possible behavior is checked is to use all patterns to assign thetask priorities in such a way that each pattern is used in a distinct verification.
For each value for pri, except for the case where pri includes only one element(e.g pri = {1}), there are several patterns to assign the priority for the tasks. For
example, if there are two tasks with identifiers a and b; and the value domain for
the task priorities is defined as [1..2], it is obvious that there are 4 patterns to
assign the priority for the tasks. They are (1,1), (1,2), (2,1), and (2,2). Generally,
let n be size of the value domain for task priorities, there are nm patterns to
assign priorities for m tasks. When the value bounds increase, the number ofpatterns becomes significantly larger. For preliminary verification, we categorize
the patterns into groups where OSEK OS with one pattern behaves almost thesame as other patterns in the group. Then we select typical patterns in groups
to use in our experiments. In sample case above, patterns (1,1) and (2,2) are
categorized in the same group; and both patterns (2,1) and (1,2) belong to14another group. We choose patterns (1,1) and (1,2) as typical patterns to use inexperiments. This is reflexed in cases No.1-No.15 of the table.

Table 2: Experiment Outputs
No.

Size of Ranges
LTS Generation
Model Checking
tasks pri res evt inr #State #Trans Time(s) Memory(Mb) Time(s) Result√
11
1 0 0 0
2
2
1
128
3
√
2
2
1 0 0 0
4
10
1
128
3
√
3
2
2 0 0 0
4
10
1
128
3
√
4
3
1 0 0 0
8
36
1
128
3
√
5
3
3 0 0 0
8
36
1
128
3
√
6
4
1 0 0 0
16
112
1
129
4
√
7
4
3 0 0 0
16
112
1
129
4
√
8
5
1 0 0 0
32
320
1
133
5
√
9
5
3 0 0 0
32
320
1
130
4
√
10
6
1 0 0 0
64
864
1
164
10
√
11
6
3 0 0 0
64
864
1
132
10
√
12
7
1 0 0 0
128
2240
1
380
26
√
13
7
3 0 0 0
128
2240
1
324
26
√
14
8
3 0 0 0
256
5632
2
382
99
√
15
9
3 0 0 0
512
13824
3
430
362
√
16
5
7 0 0 2
128
1536
2
133
17
√
17
2
1 1 0 0
8
22
1
130
7
√
18
2
1 0 1 0
10
27
1
129
4
√
19
3
6 1 0 2
80
520
1
129
8
√
20
3
6 1 1 2
152
1036
2
132
14

From the experiment results, we can see that the time taken and the total
actual memory usage for the generation of the execution sequences from Event-B
specification and the verification of the simulation relation are reasonable. For
the model checking result, no errors were returned in all cases of experiments.
This is because the design of OSEK OS has already been reviewed carefully
by a lot of people including researchers and engineers. Still, this result offersa confidence on the conformance of the OSEK OS design with respect to its
specification within input bounds.

7

Discussion

OSEK OS is the operating system which is widely used in the automotive systems. Our approach is applied to verify a design of a practical system, that is,
OSEK OS design model. The approach directly checks the design against theformal specification. Although we show the experiments, when our approach is

15

applied to the operating system, it is not limited to this application. In the approach, the simulation relation is defined based on the given relation between
states of the formal specification and those of the combination (of the design andthe environment). In models, the states are all interpreted as value assignments.
The design is described as a collection of functions which update the value assignments. The environment is described as a collection of invocations. This styleof the models will be adopted not only for the operating systems but also otherreactive systems. In our case study, Promela is used as a specification language
to describe the design and the environment; however, our framework can be applied for designs described in not only Promela but also other languages as longas they can deal with a collection of functions for the design and sequences of
invocations for the environment.
We introduce a formalization of the bounds for verifying the simulation relation of the design and the formal specification with Event-B. The bounds areused to limit set of states and possible transitions of LTS associated to EventB model. This bound can be applied generally to any design and its formal
specification as long as the formal models of the inputs are defined as LTSs. In
Section 5, we present the interpretation of the bound in a concrete model, that
is, Event-B model. In the first step of interpreting the bounds in the specification, we restrict the range of values for every variable, constant, and parameter
defined in the specification. Next, we regard the typical bugs that can be foundin the verification with large value domain. For finding such bugs of the target system, in addition to restrict the range of values, one can restrict systemservices of target system. Intention of such additional restriction is to exclude
transitions not relevant to the bugs but to reduce size of model for which model
checking is feasible.
In order to apply our framework to practical systems, we need to define initialstates of the system by assigning initial values for every variable. Even thoughranges of values for every variable have been restricted to finite sets, there are a
lot of variations for initial states. In our case study, we assign initial states for
distinct cases by manually. It is necessary to find a mechanism to assign initialstates systematically.

8

Related Works

Verification of systems using model checking There are a number of works
on verification of systems using model checking. Commonly, in model checking,a system is modeled with a finite automaton and various desired properties
with temporal logic formulae. In [7], the authors translate Trampoline OS into
Promela and define the safety properties in temporal logic formulae. Spin isused to check the OS model against these formulae. In [20], the authors model
OSEK/VDX applications and the kernel in timed automata. Time properties arefocused and verified by model-checker UPPAAL in these works. Separately, ourinput models are an OS model and its formal specification which are describedin different specification language. We ensure that the design conforms to its

16

specification by utilizing Spin model checker to check the simulation relation of
the design and its formal specification. In context of bounded model checking
which is applied in [16][8], bounds are defined as the depth of the execution pathsof the target model. In our work, bounds are defined as restrictions of rangesof values in Event-B specification so that every type has infinite range of values
must be restricted as small range.
Verification of systems based on simulation relation FDR [6] is a refinement checker for the process algebra CSP. Inputs of FDR are the specifications
and the implementations written in the same language. Our framework accepts
the inputs written in different languages.
Theorem proving has been applied as a technique to verify systems basedon simulation relation. [18] verifies the simulation relation between run-time environments layers including application layer, operating system, and FlexRay.
[10] proves the simulation relation between abstract specification, executablespecification, and C program for the seL4 micro-kernel. In these two existing
works, Isabelle/HOL is used as a theorem prover for verification. Theorem proving ensures the correctness of system in universal scope; however, it generally
requires many interactive proofs with human-machine collaboration. Separately,
we use model checking as a technique of our verification. Range for types inthe system model is bounded due to limitation of model checking; however,
we get completely automatic verification and confidence on verification results.
Additionally, our approach utilize Spin model checker to accept input models
described in various specification languages.
The simulation of two LTSs was introduced in [13] in which the key point is
to find a relation between state spaces of two LTSs such that the simulation ruleholds. In our approach, the relation between state spaces of two LTSs is given.
Then, we need to check whether the simulation rule holds.
Generation of LTS from Event-B model [11] presents the ProB tool which
support interactively animating B models. Using ProB, users can see the current
state and set an upper limit on the number of ways that the same operation canbe executed. In our works, we firstly set finite ranges for types in Event-B specification, then, explore all possible execution sequences within defined ranges.
[4] and [5] define the semantic of Event-B model as labeled transition systems
to reason about behavioral aspects of specifications in Event-B. For a further
objective, that is to check if all behaviors which are possible in Event-B specification, are also possible in the design, we generate all possible behaviors from
Event-B specification within defined ranges. We precisely define the restrictionof ranges of values in Event-B specification as bounds of our verification; thengenerate the environment and the verification conditions based on the explored
execution sequences of Event-B specification within the input bound.
Construction of the environment of the operating system In previous
works, we verified the OSEK OS by constructing a general model of the envi-

17ronment from scratch. The environment model is firstly described using UML[21] then translated into Promela. In the current work, we construct the environment based on the information obtained from the specification in Event-B and
we propose a flexible framework to check the design with respect to its formal
specification so that it can accept different specification languages of the input
models.
Combination of Event-B model and model checking The currently available tools such as ProB and Eboc [12] aim at the integration of model-checking
and Event-B to benefit from both approaches in the same development process. In this context, ProB and Eboc are both model checkers for Event-B. For
combination of model-checking using the Spin model checker and Event-B, [14]translate Event-B model into Promela model. We have not directly translated
Event-B code into Promela but generated the environment and assertions fromthe execution sequences of Event-B specification, then, use Spin to check thedesign in combination with the environment against assertions.

9

Conclusion

In this paper, we proposed an approach to verify the design against its formal
specification. Our framework includes (1) formalization of the simulation relation between two models of the same system; (2) formalization of the bound forthe verification of the simulation relation using model checking; (3) the formal
models of the specification, the design model, the environment, and the combination; (4) generation of the LTS associated with the Event-B specification
within the given bound; and (5) verification of the designs against their formal
specifications within input bounds using model checking. Based on our experiments, we discussed advantages and the applicability of the proposed approachin the engineering. The coverage of this verification is evaluated as how much of
the specification satisfied by the design. In the future work, we aim at enlarging the verification coverage to make our framework effective for the practicalverifications.

References
1. Abrial, J.R.: Modeling in Event-B: system and software engineering. Cambridge
University Press (2010)
2. Aoki, T.: Model checking multi-task software on real-time operating systems. In:
Proceedings of the 11th IEEE International Symposium on Object Oriented RealTime Distributed Computing (ISORC ’08). pp. 551–555 (2008)
3. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind
Series). The MIT Press (2008)
4. Bert, D., Cave, F.: Construction of finite labelled transition systems from B abstract systems. In: Proceedings of the 2nd International Conference on Integrated
Formal Methods (IFM ’00). Lecture Notes in Computer Science, vol. 1945, pp.
235–254 (2000)

18
5. Bert, D., Potet, M.L., Stouls, N.: Genesyst: a tool to reason about behavioral aspects of B event specifications. application to security properties. CoRR
abs/1004.1472 (2010)
6. Broadfoot, P.J., Roscoe, A.W.: Tutorial on FDR and its applications. In: Proceedings of the 7th International SPIN Workshop. Lecture Notes in Computer Science,
vol. 1885, pp. 322–322. Springer (2000)
7. Choi, Y.: Model checking trampoline os: a case study on safety analysis for automotive software. Softw. Test., Verif. Reliab. 24(1), 38–60 (2014)
8. Cordeiro, L., Fischer, B., Marques-Silva, J.: Smt-based bounded model checking
for embedded ansi-c software. IEEE Trans. Software Eng. 38(4), 957–974 (2012)
9. Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. AddisonWesley (2004)
10. Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating-system kernel. Communicationsof the ACM 53(6), 107–115 (2010)
11. Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method.
International Journal on Software Tools for Technology Transfer 10(2), 185–203(2008)
12. Matos, P., Fischer, B., Marques-Silva, J.: A lazy unbounded model checker for
event-b. In: Formal Methods and Software Engineering, Lecture Notes in Computer
Science, vol. 5885, pp. 485–503. Springer Berlin Heidelberg (2009)
13. Milner, R.: Communication and concurrency. PHI Series in computer science, Prentice Hall (1989)
14. MULLER, T.: Formal methods, model-cheking and rodin plugin development tolink event-b and spin (2009)
15. OSEK/VDX Group: OSEK/VDX operating system specification 2.2.3,
http://portal.osek-vdx.org/
16. Pradella, M., Morzenti, A., San Pietro, P.: Refining real-time system specifications through bounded model- and satisfiability-checking. In: Automated Software
Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on. pp.
119–127 (Sept 2008)
17. Reeves, S., Streader, D.: Guarded operations, refinement and simulation. Electron.
Notes Theor. Comput. Sci. 259, 177–191 (2009)
18. In der Rieden, T., Knapp, S.: An approach to the pervasive formal specification and verification of an automotive system: Status report. In: Proceedingsof the 10th International Workshop on Formal Methods for Industrial Critical Systems. pp. 115–124. FMICS ’05, ACM, New York, NY, USA (2005),
http://doi.acm.org/10.1145/1081180.1081195
19. Vu, D.H., Aoki, T.: Faithfully formalizing OSEK/VDX operating system specification. In: Proceedings of the 3rd Symposium on Information and Communication
Technology (SoICT ’12). pp. 13–20 (2012)
20. Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications
based on timed automata model. Real-Time Syst. 38(1), 39–65 (2008)
21. Yatake, K., Aoki, T.: Model checking of OSEK/VDX os design model based on
environment modeling. In: Proceedings of the 9th International Colloquium on
Theoretical Aspects of Computing (ICTAC ’12). pp. 183–197 (2012)