MightyL is a tool to convert formulas written in the MITL logic into a set of timed automata, whose synchronous product accepts the language of the formula. Those automata can then be analysed using classical tools such as UppAal or LTSMin, to check for emptiness of the formula or perform model-checking, for instance.
Online Demo
Unfortunately, due to a drastic change in the web security policies at ULB, the online demo is no more available for the moment.
Downloads
- The Source code of MightyL for the pointwise semantics (zip file). This is the download to install MightyL directly on your machine. It requires a working version of OCaml.
- A virtual machine where everything is intalled (3.2GB). Requires a working version of VirtualBox.
References
MightyL has been written and is maintained by Hsi-Ming Ho. The MightyL team is composed of:
- Thomas Brihaye, Mathematics Department, at UMONS, Mons, Belgium.
- Hsi-Ming Ho, University of Sussex, UK
- Gilles Geeraerts, Formal methods and Verification group at ULB, Brussels, Belgium
- Arthur Milchior, Google
- Benjamin Monmege, Laboratoire d’Informatique Fondamentale at the Université Aix-Marseille, Marseille, France
The project has received support from the Belgian National Fund of Scientific Research (F.R.S./FNRS), through grant PDR SyVeRLo.
The main publication documenting MightyL is:
- Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho and Benjamin Monmege. MightyL: A Compositional Translation from MITL to Timed Automata. In the Proceedings of CAV 2017, Lecture Notes in Computer Science, 10426, Springer, 2017