XCheck

From SE Wiki
Jump to: navigation, search

XChek

XChek is a multi-valued symbolic model checker. It is a generalization of an existing symbolic model checking algorithm to an algorithm for amulti-valued extension of CTL (XCTL). Given a system and a XCTL property, XChek returns the degree to which the system satisfies the property.

The main features of Chek are the following:

  • Multi-valued logics: 2-valued, 3-valued, upset, 4-valued disagreements, etc. Users can define their own logics.
  • Multiple model formats: reads SMV and GCLang models. Multi-valued models are specified in XML.
  • Proof-like counterexamples: proof rules are used to generate counterexamples. Counterexamples can be generated statically or dynamically, and various viewers are available.

Website: XChek and user manual