From SE Wiki
Revision as of 16:37, 22 December 2010 by (Talk)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search


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


VaqTree is a tool that efficiently exploits the resolution proof produced by a successful run of BMC to detect vacuity of LTL properties. The goal of this tool is to detect a significant amount of vacuity when compared to the naive method, with faster runtimes. Results will be presented at FMCAD '07.

Website: VaqTree, test data and results


TReMer (Tool for Relationship-Driven Model Merging) is a proof-of-concept tool for merging models constructed during a collaborative model-based development process. The tool offers two different approaches for merge, one for merging conceptual models in requirements elicitation, and another for merging behavioural models used in design and implementation. The former approach provides a generic solution based on category theory for combining structural models represented as graphs; and the latter provides a semantics-based solution for constructing behaviour-preserving merges of Statecharts models.

WebSite: TReMer and Case-Studies