13.2 Translatable RSL constructs13.2 Translatable RSL constructs
13 SAL Translator 13 SAL Translator
13.4 Confidence condition verification 13.4 Confidence condition verification
13.3 Writing transition systems and LTL assertions

13.3 Writing transition systems and LTL assertions

Model checking is a formal method which consists basically in algorithmically verify if a model satisfies properties. The model is usually expressed as a transition system. On the other hand, properties are written as formal specifications, often using temporal logic formulas. Basically there are three kinds of temporal logic formulas: LTL , CTL and CTL*.

In the context of RAISE development method, model checking is used early in development. Between the different kinds of RAISE specification styles, the applicative style is used. To use model checking specifying RSL code, it is necessary [16],

So, in order to use model checking techniques on RSL, it is necessary to represent transition systems and one of the kinds of temporal logic formulas (in particular, LTL assertions). Since none of these topics had a direct representation in RSL, it was extended adding features for writing transition systems and LTL assertions. Subsections 13.3.2 and 13.3.3 describe how write transition systems and LTL assertions respectively. Previously, a little background about model checking is presented in subsection 13.3.1

13.3.1 About Model Checking

Model checking is a very popular technique used for ensuring the correctness of hardware and software systems. Properties such as safety and liveness can be checked to assure correctness of systems, specially concurrent systems. It is a complete and automatic technique, but it only checks a model (not the real system).

Nowadays there are many model checkers, the main ones are SPIN, SMV and SAL. In particular, SAL is proposed for enabling model checking in RSL through the translator.

The model checking process consists of three steps: model specification, properties specifications and verification. The model specification is a mathematical model of the system, properties specification formally specify the desired behaviour of the system and finally the verification checks if model satisfies the specification.

Model specification

The model is often expressed as a transition system, a directed graph consisting of nodes and edges (a computational tree). Each node has associated a set of atomic propositions. Nodes represent states of a system, edges represent possible transitions, and atomic propositions represent basic properties that hold at a point of execution.

Model checking is based on the calculation and the representation of all possible reachable states by the system, so the size of the computation increases exponentially with respect to the size of the problem. Several techniques have been developed to solve this issue. In particular, symbolic model checking and abstraction are two of the most used.

Specification of properties

Desired behaviour of the system is specified with a formal language, a temporal logic. With temporal logic the static notion of truth is replaced by a dynamic one, in which the formulas may change their truth values as the system evolves from state to state.

The Computation Tree Logic CTL* is the most expressive temporal logic. It is used to describe properties of computation trees. CTL* formulas are composed of path quantifiers and temporal operators.

There are two types of formulas in CTL*: state formulas and path formulas. State formulas are true in a specific state and path formulas are true along a specific path.

These formulas allow one to specify different requirements of systems, properties such as, reachability, safety, liveness and fairness. In particular, safety and liveness refer to,

There are two sublogics of CTL*: Branching-time logic and linear-time. In branching-time temporal logic temporal, operators quantify over the paths that are possible from a given state. In linear-time temporal logic, operators are provided for describing events along a single computation path.

Computation Tree Logic (CTL) is a branching-time logic and it is a restricted subset of CTL* in which each of the temporal operators X, F, G, U and R must be immediately preceded by a path quantifier.

Linear Temporal Logic (LTL), on the other hand, is a linear time logic and consists of formulas that have the form (A f), where f is a path formula in which the only state subformulas permitted are atomic propositions.

13.3.2 Writing transition systems in RSL

To describe transition system inside RAISE's specification code, it is necessary to write following the grammar described below (an example about how to write a transition system can be found in subsection 13.3.4).

                                     
 Transition_system_decl ::= "transition_system" {Base_module}+,
 

Base_module ::= "["id"]" ["in" variable_decl] "local" variable_decl "in" Transition_decls "end"

 

Transition_decls ::= {Transition_decl}+[=]

 

Transition_decl ::= Single_guarded_command | Multiple_guarded_command

 

Single_guarded_command ::= ["["id"]"] logical-value_expr " ==>" Update_exprs |

  ["[" id "]"] " else" "==>" Update_exprs
 

Multiple_guarded_command ::= "([=]" variable_decl ":-" Single_guarded_command ")"

 

Update_exprs ::= {id ":=" value_expr}*,

 

All variables declared as "in" are considered inputs to the transition system. The value for these variables will be initialized by the model checker. On the other hand, all variables declared as "local" represent the actual state of the transition system. If these variables are not initialized then the model checker will initialize them to any value. So the tool imposes the existence of an initial value for every local variable.

13.3.3 Writing LTL assertions in RSL

To describe LTL assertions inside RAISE's specification code, it is necessary write following the grammar described below (an example about how to write LTL assertions can be found in subsection 13.3.4).

LTL_Property_decl ::= "ltl_assertion" {LTL_assertion}+,

LTL_assertion ::= "["id"]" id "|-" LTL_expr

LTL_expr ::= logical_value_expr

The LTL temporal operators "G", "F", and "X" are allowed in LTL_exprs as function symbols.

13.3.4 An example

In some kind of the systems, such as a lift, it is important check certain properties, like safety and reliability. After modelling the system, it is possible to check these properties, using the model checking technique. Details of this problem, can be found in [16]. As was mentioned before, to use the model checking technique in the applicative RAISE style, it is necessary: to make a system finite, to define all the functions explicitly, to add a transition system, and to specify the LTL assertions.

First the example will be shown, a finite system will be done and all functions will be explicitly defined. Later the transition system and LTL assertions will be specified.

The problem

Suppose that it is necessary to provide the control software for a lift in a building of 3 floors. The lift has to control different hardware components: cage, door, button, indicator, floor and motor.
Assumptions
Description

Cage is single doored and it will presumably change its position, direction and speed. Doors are open or closed or perhaps in intermediate positions. Buttons are pressed (and lit) or cleared (and unlit).

The lift must serve a number of floors numbered consecutively. In each floor there are doors which must only be open when the lift is stationary at the floor. In each floor there are buttons. Except the top floor, there is a button to request the lift to stop there and then go up. Except the bottom floor, there is a a button to request the lift to stop there and then go down. Inside the lift also there is a button for each floor to request the lift to go to the floor.

RSL specification

A lift is an example of an asynchronous system. This is, there are external stimuli that may arrive at any time (for example, buttons may be pressed at any time).

Following the RAISE development style, first it is necessary to consider the objects of the system and whether they will have dynamic state. In this case, the cage, the doors and the buttons will have dynamic state and hence be modelled as RSL objects.

The system must be specified and for this, it is necessary to formulate the type module for the system. This last one is called TYPES and later defined, it will instantiate as the global object "T".

                                     
 scheme
 TYPES =
 class
 value
 min_floor : Nat = 0, max_floor : Nat = 2
 
 type
 Floor = {| n : Nat • n ∈ {min_floor .. max_floor} |},
 Door_state == open | shut,
 Button == bup0 | bup1 | bdown1 | bdown2 | blift0 | blift1 | blift2,
 Button_state == lit | clear,
 Direction == up | down,
 Movement == halted | moving,
 Requirement :: here : Bool after : Bool before : Bool
 
 value
 next_floor : Direction × Floor -~-> Floor
 next_floor(d, f) ≡
 if d = up then f + 1 else f - 1 end
 pre is_next_floor(d, f),
 
 is_next_floor : Direction × Floor → Bool
 is_next_floor(d, f) ≡
 if d = up then f < max_floor else f > min_floor end,
 
 invert : Direction → Direction
 invert(d) ≡ if d = up then down else up end
 end

Note that the type "Floor" has been defined as a subtype of Int. As it is supposed that there are three floors, it is possible to be explicit about what buttons there will be: two “up” buttons for floors 0 and 1), two “down” buttons for floors 1 and 2, and a lift button (inside the lift cage) for each floor.

The type "Requirement" is used to control the cage. It calculates, according to the button states, the current floor, and the current direction whether the cage is required to stop here, after or before.

Finally, note that the function "next_floor" indicates that f+1 is directly above floor f, and f-1 directly below it.

After defining the TYPE module and the object T, it is necessary to define modules for the cage, the buttons and the doors and from them to construct the lift system type. In particular, the definition of BUTTONS module and the CAGE module are shown.

                                     
 scheme BUTTONS = hide required_here, required_beyond in
 class
  type
 Buttons ::
 up0 : T.Button_state ↔ re_up0
 up1 : T.Button_state ↔ re_up1
 down1 : T.Button_state ↔ re_down1
 down2 : T.Button_state ↔ re_down2
 lift0 : T.Button_state ↔ re_lift0
 lift1 : T.Button_state ↔ re_lift1
 lift2 : T.Button_state ↔ re_lift2
 
  value
 clear : T.Floor × Buttons →Buttons
 clear(f, bs) ≡
 case f of
 0 → re_up0(T.clear, re_lift0(T.clear, bs)),
 1 → re_down1(T.clear, re_up1(T.clear, re_lift1(T.clear, bs))),
 2 → re_down2(T.clear, re_lift2(T.clear, bs))
 end,
 
 press : T.Button × Buttons → Buttons
 press(b, bs) ≡
 case b of
 T.bup0 → re_up0(T.lit, bs),
 T.bup1 → re_up1(T.lit, bs),
 T.bdown1 →re_down1(T.lit, bs),
 T.bdown2 → re_down2(T.lit, bs),
 T.blift0 → re_lift0(T.lit, bs),
 T.blift1 → re_lift1(T.lit, bs),
 T.blift2 → re_lift2(T.lit, bs)
 end,
 
 is_clear : T.Button × Buttons → Bool
 is_clear(b, bs) ≡
 case b of
 T.bup0 → up0(bs) = T.clear,
 T.bup1 → up1(bs) = T.clear,
 T.bdown1 → down1(bs) = T.clear,
 T.bdown2 → down2(bs) = T.clear,
 T.blift0 → lift0(bs) = T.clear,
 T.blift1 → lift1(bs) = T.clear,
 T.blift2 → lift2(bs) = T.clear
 end,
 
 check : T.Direction × T.Floor × Buttons → T.Requirement
 check(d, f, bs) ≡
 T.mk_Requirement(
 required_here(d, f, bs),
 required_beyond(d, f, bs),
 required_beyond(T.invert(d), f, bs)),
 
 required_here : T.Direction × T.Floor × Buttons → Bool
 required_here(d, f, bs) ≡
 case f of
  0 → lift0(bs) = T.lit \/ up0(bs) = T.lit,
  1 →
  lift1(bs) = T.lit \/
  case d of
  T.up →
  up1(bs) = T.lit \/
  down1(bs) = T.lit /\
  lift2(bs) = T.clear /\
  down2(bs) = T.clear,
  T.down →
  down1(bs) = T.lit \/
  up1(bs) = T.lit /\
  lift0(bs) = T.clear /\
  up0(bs) = T.clear
  end,
 2 → lift2(bs) = T.lit \/ down2(bs) = T.lit
 end,
 
 required_beyond : T.Direction × T.Floor × Buttons → Bool
 required_beyond(d, f, bs) ≡
 let f′ = T.next_floor(d, f) in
 required_here(d, f′, bs) \/
 T.is_next_floor(d,f′) /\
 let f′′ = T.next_floor(d, f′) in
 required_here(d, f′′, bs)
 end
 end
 end

In the definition type of the BUTTONS module, it is possible to see that there are two "up" buttons on floors 0 and 1, and two "down" buttons on floors 1 and 2. There is a lift button inside the lift cage for each of the three floors.

                                     
 scheme CAGE =
 class
 type
 Cage ::
 direction : T.Direction
 movement : T.Movement
 floor : T.Floor
 
 value
 /* generators */
 move : T.Direction × Cage -~-> Cage
 move(d′, m) ≡
 mk_Cage(d′, T.moving, T.next_floor(d′, floor(m)))
 pre T.is_next_floor(d′, floor(m)),
 
 halt : Cage → Cage
 halt(m) ≡ mk_Cage(direction(m), T.halted, floor(m))
 end

After defining the CAGE, DOORS and BUTTONS modules, it is possible to construct the lift system type,

                                     
 scheme LIFT =
 class
 object C : CAGE, DS : DOORS, BS : BUTTONS
 
 type
 Lift ::
 cage : C.Cage
 doors : DS.Doors
 buttons : BS.Buttons

Also, it is necessary to define functions to operate the lift system, such as "move", "halt", "check_buttons", "is_clear", and "press". The function "move" should specify that the lift is moved from a floor to the next floor in the given direction. The function "halt" should specify that the cage is halted, doors at the current floor are opened and buttons for the current floor are cleared. The functions "check_buttons", "is_clear", and "press" should specify the access to the corresponding functions of BUTTONS. Finally the function "next" should calculate what to do next in any state, according to the current requirement. The specification of these functions is shown below.

                                     
 value
 move : T.Direction × T.Movement × Lift -~-> Lift
 move(d, m, l) ≡
 mk_Lift(
  C.move(d, cage(l)),
  if m = T.halted
  then DS.close(C.floor(cage(l)), doors(l))
  else doors(l)
  end, buttons(l))
 pre T.is_next_floor(d, C.floor(cage(l))),
 
 halt : Lift → Lift
 halt(l) ≡
 mk_Lift(
  C.halt(cage(l)),
  DS.open(C.floor(cage(l)), doors(l)),
  BS.clear(C.floor(cage(l)), buttons(l))),
 
 check_buttons : Lift → T.Requirement
 check_buttons(l) ≡
 BS.check(
  C.direction(cage(l)), C.floor(cage(l)),
  buttons(l)),
 
 is_clear : T.Button × Lift → Bool
 is_clear(b, l) ≡ BS.is_clear(b, buttons(l)),
 
 press : T.Button × Lift → Lift
 press(b, l) ≡
 mk_Lift(cage(l), doors(l), BS.press(b, buttons(l))),
 
 next : Lift -~-> Lift
 next(l) ≡
 let
 c = cage(l),
 ds = doors(l),
 bs = buttons(l),
 r = check_buttons(l),
 d = C.direction(c)
 in
 case C.movement(c) of
 T.halted →
 case r of
 T.mk_Requirement(_, true, _) →
 move(d, T.halted, l),
 T.mk_Requirement(_, _, true) →
 move(T.invert(d), T.halted, l),
 _ → l
 end,
 T.moving →
 case r of
 T.mk_Requirement(true, _, _) → halt(l),
 T.mk_Requirement(_, false, false) → halt(l),
 T.mk_Requirement(_, true, _) →
 move(d, T.moving, l),
 T.mk_Requirement(_, _, true) →
 move(T.invert(d), T.moving, l)
 end
 end
 end
 pre can_next(l),
 
 can_next : Lift → Bool
 can_next(l) ≡
 let c = cage(l), r = check_buttons(l) in
 (T.after(r) ⇒
  T.is_next_floor(C.direction(c), C.floor(c))) /\
 (T.before(r) ⇒
  T.is_next_floor(
 T.invert(C.direction(c)), C.floor(c)))
 end

The algorithm of the function "next" uses the current requirement. A requirement has three Boolean components: here, after, and before.

If the lift is halted then

If the lift is moving then

As the function "move" in CAGE is partial, it is necessary to define the precondition "can_next". It ensures that the requirement only will move to another floor when such a floor exists.

Transition System

The system has already been made finite and functions have already defined explicitly, so now the transition system will be specified. Such as was mentioned in subsection 13.3.2, to specify a transition system, it is necessary to decide about variables.

In this case, there is a single state variable Lift and it is possible to use just that. The initial state is chosen as: the lift halted with the doors open at floor 0, with all buttons clear.

Also, it is necessary to decide what the guarded commands for the transitions are. For this, the use of "next" with its precondition as guard is chosen. On the other hand, "press" is chosen too. A guard is needed for press: if this guard is not declared, the checking will fail when the lift must make progress, because the transition system will allow repeatable press transitions with no next transitions. So, "press" only is allowed when the button involved is clear.

                                     
 transition_system
 [L]
 local
 lift : Lift :=
 mk_Lift(
  C.mk_Cage(T.up, T.halted, 0),
  DS.mk_Doors(T.open, T.shut, T.shut),
  BS.mk_Buttons(
 T.clear, T.clear, T.clear, T.clear, T.clear,
 T.clear, T.clear))
 in
 ([] b : T.Button •
  [press]
  is_clear(b, lift) ⇒ lift′ = press(b, lift))
 []
 [next]
 can_next(lift) ⇒ lift′ = next(lift)
 end
LTL assertions

Now it is necessary to specify LTL assertions in order to verify properties that the lift must to have. An important property to verify is safety. To specify this property, suppose that a function "safe" in the scheme LIFT is defined as following,

                                     
 safe : Lift → Bool
 safe(l) ≡
 let c = cage(l), ds = doors(l) in
 (∀ f : T.Floor •
  (DS.door_state(f, ds) = T.open) =
  (C.movement(c) = T.halted /\ C.floor(c) = f))
 end

The LTL assertion for safety is,

                                     
 ltl_assertion
 [safe] L   G(safe(lift)),
 [req_safe] L   G(can_next(lift))

A LTL assertion will be useful to check that the lift eventually halts somewhere. This is written as,

                                     
 ltl_assertion
 [eventually_halts] L   G(F(C.movement(cage(lift)) = T.halted))

Another LTL assertion is defined to check that the lift is not permanently stationary on some floor. The specification intentionally asserts something we expect to be false, in this case that the lift never reaches floor 2,

                                     
 ltl_assertion
 [moves] L   G(C.floor(cage(lift)) < 2)

The assertion is invalid, so the model checker will generate a counter-example, such as the button lift2 is pressed and the lift moves from floor 0 to floor 1 and then continues to floor 2. Now it is possible to be sure that the lift is actually capable of useful behaviour.

Also it is important to specify liveness properties; for example, to specify for all floors that if a floor is requested from the lift then it must be eventually reached. This property for floor 0 is as follows,

                                     
 ltl_assertion
 [arrives0]
 L  
 G(
  BS.up0(buttons(lift)) = T.lit \/
  BS.lift0(buttons(lift)) = T.lit ⇒
  F(DS.d0(doors(lift)) = T.open))

Note that all assertions must refer to a transition system (L in this case). Also note that "G" (globally in all states) and "F" (now or in the future) can be used as LTL temporal operators.

Chris George, April 17, 2008

13.3 Writing transition systems and LTL assertions
13.2 Translatable RSL constructs13.2 Translatable RSL constructs
13 SAL Translator 13 SAL Translator
13.4 Confidence condition verification 13.4 Confidence condition verification