Verimag

Kronos

Kronos is a tool for model-checking of timed automata against specifications expressed using the real-time temporal logic TCTL. Additional modules are Minim, for time-abstracting bisimulation for timed automata and Optikron, an optimization package for reducing the number of clocks. Kronos is based on difference-bounds matrices (DBM). A discrete time version using BDD encodings is implemented in the SMI tool.

Voir en ligne : Tool Web Page

Contact | Plan du site | Site réalisé avec SPIP 2.1.26 + AHUNTSIC [CC License]

Visiteurs connectés : 8 ; visites : 391220