Simple Example of Formal Verification of MPL Models

 
Project Page
Publications
People
Related Sites

 

 
The Robotics Institute
Carnegie Mellon University
NASA Ames Research Center

This page shows a simple example of the automatic translation and explanation of MPL (Livingstone) models.

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))
  (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))))

  (defmodule switch-module (?name)
    (: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_


Last Updated: June 30, 2000 reids+@cs.cmu.edu