Simple Example of Formal Verification of MPL Models

Project Page
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)
       :model (on (indicator-lamp ?name))
       :type :ok-mode
       :transitions ((turn-off :when (off (command-in ?name)) :next off)
                     (:otherwise :persist)))
       :model (off (indicator-lamp ?name))
       :type :ok-mode
       :transitions ((turn-on :when (on (command-in ?name)) :next on)
                      (:otherwise :persist)))
      :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
    command-in : {on_, off_, no-command_};
    indicator-lamp : {on_, off_};
    _mode : {on_, off_, broken_};
    _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
    switch : switch;
    _broken := switch._broken;
  MODULE main
    switch-module : switch-module;
    _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_
  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_)
       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