| Project Page | |
| Publications | |
| People | |
| Related Sites | |
 |
|
|
|
The following is a simple model of a switch and lamp. Basically, the
model describes a switch that can be in either nominal (on,
off) or fault (broken) modes. When in a nominal mode, the
indicator-lamp is either on or off, and the switch can be commanded to
turn on or off. In addition, at any time the switch can
non-deterministically transition to the broken (fault) mode, which has
no constraints on the value of the indicator-lamp.
(defvalues on-off-values (on off))
(defmodule switch-module (?name)
(defvalues on-off-command (on off no-command))
(defcomponent switch (?name)
(:inputs ((command-in ?name) :type on-off-command
:documentation "Command to turn switch on or off"))
(:outputs ((indicator-lamp ?name) :type on-off-values
:documentation "Observed value"))
(:background :initial-mode off)
(on
:model (on (indicator-lamp ?name))
:type :ok-mode
:transitions ((turn-off :when (off (command-in ?name)) :next off)
(:otherwise :persist)))
(off
:model (off (indicator-lamp ?name))
:type :ok-mode
:transitions ((turn-on :when (on (command-in ?name)) :next on)
(:otherwise :persist)))
(broken
:type :fault-mode
:probability 0.01
;; Once we decide the switch is broken, it stays broken
:transitions ((:otherwise :persist))))
(:structure (switch ?name)))
Given the above model, the translator produces the following SMV code,
which adheres to the semantics described above. This code can then be
used to verify properties of the models, such as consistency or
reachability of the various modes.
MODULE switch
VAR
command-in : {on_, off_, no-command_};
indicator-lamp : {on_, off_};
_mode : {on_, off_, broken_};
DEFINE
_fault_modes := {broken_};
_broken := (_mode in _fault_modes);
INIT (_mode = off_)
TRANS (((_mode = on_) & (command-in = off_)) -> (next(_mode) in (off_ union _fault_modes)))
TRANS (((_mode = on_) & !(command-in = off_)) -> (next(_mode) in (on_ union _fault_modes)))
TRANS (((_mode = off_) & (command-in = on_)) -> (next(_mode) in (on_ union _fault_modes)))
TRANS (((_mode = off_) & !(command-in = on_)) -> (next(_mode) in (off_ union _fault_modes)))
TRANS ((_mode = broken_) -> (next(_mode) = broken_))
INVAR ((_mode = on_) -> (indicator-lamp = on_))
INVAR ((_mode = off_) -> (indicator-lamp = off_))
MODULE switch-module
VAR
switch : switch;
DEFINE
_broken := switch._broken;
MODULE main
VAR
switch-module : switch-module;
DEFINE
_broken := switch-module._broken;
We have also worked on producing causal explanations of SMV
counter examples. Basically, we convert the SMV model to
propositional formulae and use the counter example to determine how to
set exogenous variables. A TMS (Truth Maintenance System) is used to
record logical dependencies, and these dependencies are then analyzed
to produce a concise explanation of why the given property is false.
To date, our tool has automatically produced explanations for simple
CTL formulae of the form "AG p". For instance, the following is an
explanation of why the property "the switch is never on" is false.
AG (!switch-module.switch.indicator-lamp = on_) is false because
In State 1
1. SWITCH-MODULE.SWITCH._MODE is initially OFF_
2. SWITCH-MODULE.SWITCH.COMMAND-IN is set to ON_
In State 2
3. SWITCH-MODULE.SWITCH._MODE non-deterministically transitions to ON_
based on 1, 2 and
switch-module.switch._mode = off_ & switch-module.switch.command-in = on_ -> next(switch-module.switch._mode) in (on_ union broken_)
4. SWITCH-MODULE.SWITCH.INDICATOR-LAMP is ON_
based on 3 and
switch-module.switch._mode = on_ -> switch-module.switch.indicator-lamp = on_
5. (!switch-module.switch.indicator-lamp = on_) is FALSE
based on 4
For comparison, the following is the original counter example
produced by SMV.
-- specification 'AG (!switch-module.switch.indicator-lamp = on_)' is false
-- as demonstrated by the following execution sequence
state 1.1:
_broken = 0
switch-module._broken = 0
switch-module.switch._broken = 0
switch-module.switch._fault_modes = broken_
switch-module.switch.command-in = on_
switch-module.switch.indicator-lamp = off_
switch-module.switch._mode = off_
state 1.2:
switch-module.switch.indicator-lamp = on_
switch-module.switch._mode = on_