Formal Methods && Tools Group

The FMT group 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

Other 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