System

Description

LTL

 

Spin

 http://spinroot.com/spin/whatispin.html

Check Linear Prepositional temporal logic properties

Transfer linear prepositional temporal logic to buchi automata. Wide used model checker

Complexity is N*2O(n). in which N is the total state of the system and n is the number of sub formula of the prepoerty we want to check

System input language: Promela(Process or Protocol Meta Language). Have declarations. Variables, finite length array, Symbolic constants, structure, processes, etc, so you can build a finite state machine/kripke structure out of it.

Property language: verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic

Common used verifier, have support

 

 

3VMC

http://www.cs.tau.ac.il/~yahave/3vmc.htm

3VMC is a tool for analysis and verification of concurrent systems. 3VMC is geared towards verification of concurrent software, it supports dynamic allocation of objects and threads and does not put an a priori bound on the number of allocated objects and threads. 3VMC provides a powerful abstraction mechanism based on 3-valued logic. 3VMC is an extension of the TVLA framework.

Main features:

  • On-the-fly verification of safety properties and general LTL properties.
  • A powerful abstraction mechanism based on 3-valued logic - this allows verification of programs that manipulate heap-allocated data structures. Abstraction also applies to dynamically allocated threads. 3VMC is able to handle programs with an unbounded number of allocated objects and threads.
  • Program behavior is modeled using transition systems. The transition system is specified using the TVM language.
  • Automatic state-space symmetry reduction.
  • Property-guided abstraction (still experimental).

·        Desired properties can be formulated as assertions or as a general Buchi automata.

System input language: modeled using transition systems. The transition system is specified using the TVM language.

For academic only. No support

 

 

 

 

 

CTL

CTL*

 

Rainbow

http://www.cs.man.ac.uk/fmethods/projects/AHV-PROJECT/ahv-project.html

Check CTL* Prepositional temporal logic properties

Using game to do the checking

 

Can’t handle conditions while transfer from state to state

System input language: modeled using kripke structure, no conditions while transfer from state to state

Property language: verification of branching time temporal constraints; by directly formulating the constraints in temporal logic CTL

 

SMV

http://www-2.cs.cmu.edu/~modelcheck/smv.html

Tour: http://www-2.cs.cmu.edu/~modelcheck/tour.htm

a symbolic model checker for CTL, support concurrency.

handles prepositional CTL,

System input language: The system is described by a high-lever description program language. Which is transferred into OBDD(ordered binary decision diagram), OBDD will make the verification easy. no input is involved.

Property language: verification of branching time temporal constraints; by directly formulating the constraints in prepositional temporal logic CTL. The CTL properties write as it is CTL formula following the keyword ”SPEC”.

SMV was able to determine CTL formula is violated, and to produce a counterexample to show why this happens

*

SF2SMV

http://www.ece.cmu.edu/~webk/sf2smv/

An practice extension to SMV

Formal Verification of Stateflow Diagrams(which is build by Matlab 6.0) Using SMV. Sf2smv transforms Matlab Stateflow diagram to SMV model file for model checking purpose(using Matlab stateflow toolbox—simulate finite state machine).

Can check properties like:

  • Testing for Reachability.  This refers to the ability to test if a state or set of states is reachable from a specified set of initial states.
  • Testing for paths.  This refers to the ability to find a path or trajectory of the system, from a specified initial state to a specified terminal state.  This property is particularly useful for finding conditions leading to error states.
  • Testing ranges of variables.  This refers to the ability to test if variables in a system are within their desired ranges.  It is useful for checking if the system satisfies application requirements.
  • Finding loops.  Loops occur when the system progresses through a set of states indefinitely.  Loops are considered errors because once a system runs into a loop the system cannot proceed to other states.

 

System input language: modeled using Matlab’s Stateflow toolbox.  Sf2smv transforms Matlab Stateflow diagram to SMV model file for model checking purpose(using Matlab stateflow toolbox—simulate finite state machine).

Can handle conditions while transfer from state to state, have actions, input, is event-driven. Have input variables.(but you need to supply the range)

Property language: verification of branching time temporal constraints; by directly formulating the constraints in prepositional temporal logic CTL. The CTL properties write as it is CTL formula following the keyword ”SPEC”.

Restrictions

There are a few restrictions when using the old SF2SMV:

  • SF2SMV will not work with Stateflow diagrams with multi-level local event broadcast.
  • SF2SMV does not support multiple Stateflow diagrams.

Function call actions and complex mathematical expression are not supported.

 

 

 

 

FO

 

3TAP

http://i12www.ira.uka.de/~threetap/

Check First order logic properties.

Can’t check temporal logic at all

 

SVC

http://chicory.stanford.edu/SVC/

The Stanford Validity Checker (SVC for short) is a research tool to check the validity of formulas expressed in a subset of first-order logic. SVC is an attractive tool for formal verification because of its efficient and automatic decision procedures.

Can’t check temporal logic at all

 

 

 

 

 

 

 

 

FOTL

 

Mind

http://www.csc.liv.ac.uk/~alexei/FOTL/

Three Value logic analyzer, it is a program correctness checker.

 

MONA

http://www.math.tau.ac.il/~rumster/TVLA/

TVLA is a “yacc”-like framework for automatically constructing static-analysis algorithms from operational semantics, where the operational semantics are specified using logic formulae.

The system ‘s description is based on first-order predicate logic with transitive closure. An additional input to TVLA is an abstract representation of all the memory state at the beginning of the analyzer program.

 

The input to TVLA consists of two fi
les: (i) a TVS (Three Valued logical Structure) file containing a textual representation of the input structures and (ii) a TVP (Three Valued Program) file, which includes the operational semantics and the association of the operational semantics with the edges of the control  graph (CFG) of the analyzed program.

Three value: meaning sometimes it will say “I don’t know”

  • Output: a finite set of all structures that satisfied with all the operational semantic and properties.

System input language: first-order logic with transitive closure.

 

TVLA only supports predicates of arity <3; such logical structure can be thought of as directed graph.

Property language: output descriptor. Properties can be extracted by evaluating formulae with transitive closure and equality, but without function symbols and constant symbols

System theoretical base: the embedding theorem

 

  • Any formula that evaluates to a definite value in a 3-valued structure evaluate to the sane value in all the 2-valued structures embedded into that structure.

Reference:

 

For academic only. No support

Used in shape analysis

No temporal logic used. But can temporal logic being express by second-order logic?

 

WS1S

  • Weak monadic second-order theory of 1 successor function “+1” and “0”
  • First term interpreted as numbers
  • Monadic means: “only unary predicate can be interpreted as second order variables” thus, the second order terms denote the set of natural numbers
  • Weak mean those set are finite

Theory base for of MONA.

Despite its name, WS1S is a simple and natural notation. Being a variation of first-order logic, WS1S is formalism with quantifiers and Boolean connectives. Its interpretation, however, is tied to arithmetic somewhat weakened to keep the formalism decidable. In WS1S, first-order variables denote natural numbers, which can be compared and subjected to addition with constants. WS1S also allows second-order variables while remaining decidable; each such variable is interpreted as a finite set of numbers.

WS1S and its generalization WS2S [TW68, Don70], which is interpreted over the infinite binary tree, can be used to express problems ranging from hardware verification to formal linguistics.

Unfortunately, the space and time requirements for translating formulas to automata have been shown to be non-elementary

 

 

TVLA

Three Value logic analyzer, it is a program correctness checker.

http://www.math.tau.ac.il/~rumster/TVLA/

TVLA is a “yacc”-like framework for automatically constructing static-analysis algorithms from operational semantics, where the operational semantics are specified using logic formulae.

The system ‘s description is based on first-order predicate logic with transitive closure. An additional input to TVLA is an abstract representation of all the memory state at the beginning of the analyzer program.

 

 

 

The input to TVLA consists of two fi
les: (i) a TVS (Three Valued logical Structure) file containing a textual representation of the input structures and (ii) a TVP (Three Valued Program) file, which includes the operational semantics and the association of the operational semantics with the edges of the control  graph (CFG) of the analyzed program.

Three value: meaning sometimes it will say “I don’t know”

Output: a finite set of all structures that satisfied with all the operational semantic and properties.

System input language: first-order logic with transitive closure.

 

TVLA only supports predicates of arity <3; such logical structure can be thought of as directed graph.

Property language: output descriptor. Properties can be extracted by evaluating formulae with transitive closure and equality, but without function symbols and constant symbols

System theoretical base: the embedding theorem

 

Any formula that evaluates to a definite value in a 3-valued structure evaluate to the sane value in all the 2-valued structures embedded into that structure.

Reference:

 

For academic only. No support

Used in shape analysis