Tools

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

Contract Automata Toolkit: is a set of tools for contract automata. It currently features the Contract Automata Library (CATLib), the Contract Automata App (CATApp) and the Contract Automata Runtime Environment (CARE). CATLib is the main repository and implements contract automata and their operations, e.g., composition and synthesis. CATApp is a GUI front-end and CARE is a runtime environment for realising service applications specified using contract automata.
Available here: https://github.com/contractautomataproject
Website here: https://contractautomataproject.github.io/ContractAutomataLib/
Contact: davide.basile@isti.cnr.it

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