AbstractSmv

AbstractSmv

Allowing abstract variables in NuSMV

Background
  • NuSMV is a tool for formal verification using LTL, CTL and StateCharts.
  • An .smv file normally consists of the following parts: VAR (decaration of variables), ASSIGN (declaration of an automaton) and SPEC or LTLSPEC (decleration of the specification).
  • This program provides the user the ability to:
    • Use shortcuts for the "next" operator: when writing a specification like "the gate is open between the 3rd and the 7th time units", one usually writes something like X3,7(GATE_OPEN). Likewise, when writing a specification like "the gate is closed sometime between the 3rd and the 7th time units" one usually writes something like X 3,7(GATE_CLOSED). I don't know of any way to write these shortcuts in NuSMV (instead, one writes the conjunction or disjunction of all the options). This program allows the user to write these shorcuts.
    • Use abstract variables: When writing a long specification, it is convenient to divide it into parts, naming those parts and then combining them. For example, it might be comfortable to write "(assumption1 & assumption2) -> (reuirement1 & requirement2)". This program allows the user to write such abstract variables, by the introduction of a forth part to the .smv file called "ABSTRACTIONS".
Usage
  • Input: an .asmv fie. This is an .smv file, possibly with an additional section in its end called "ABSTRACTIONS". This section contains a line-seperated definitions of abstract variables that are used in the SPEC (or LTLSPEC) section. In addition, the .asmv file may contain formulas like "X3^5(LIGHT)" (meaning that the light is on between the 3rd and 5th time units) and "X3_5(LIGHT)" (meaning that the light is on sometime between the 3rd and the 5th time units).
  • Output: an .smv file that was obtained from the .asmv file by all the necessary replacements of shortcuts and abstract varaibles. The output file is saved in the input file's directory.
  • Execution:
Example
Downloads
Go back to my homepage