Formal Methods && Tools Group

FMT has developed the following tools

KandISTI : a framework for the exploration, analysis and model checking of models, specified in a variety of languages, abstractly modeled as doubly labeled transition systems, supporting a branching-time, parametric, state-and-event based logic. This framework is composed by the following tools:

  • UMC: a framework for the exploration, analysis and model checking of models based on networks of interacting UML statecharts
  • FMC: a framework for the exploration, analysis and model checking of models based on networks of automata (specified in process algebra which include constructs from the CCS/CSP/LOTOS process algebras)
  • CMC: a framework for the exploration, analysis and model checking of models based on COWS specifications, in the context of Service Oriented Analysis
  • VMC: a framework for the exploration, analysis and model checking of models based on Model Transition Systems, in the context of Product Variability Analysis

QuARS: Quality Analyzer of Requirements Specification

Topochecker: a spatio-temporal model checker based on closure spaces and Kripke frames

VoxLogicA: a tool for analysing images using spatial logics and model checking

FMCAT: a tool for designing behavioural contracts expressed as automata, for composing them, and for applying most permissive controller synthesis to compute orchestrations and choreographies. The main characteristic is the adaptation of the synthesis algorithm to product lines and semi-controllable transitions.

Other no longer available tools

  • JACK, JACK2,JACK3: (Just Another Concurrency Kit)
  • HAL: History-dependent Analysis Laboratory - Pi-calculus verification environment with tcl/tk interface
  • HAL-on-Line: The whole HAL environment on-line
  • AMC: ACTL model checker for fc2 automators
  • BMC: BDD based ACTL model checker for fc2 networks / regular CCS / regular LOTOS specification
  • WCS: WCS (Witness and Counterexample Server): Witness and Counterexample Automata Generator for ACTL