My colleague Habtom K. Gidey was presenting our second release of FACTum Studio at the 16th International Conference on Formal Aspects of Component Software taking place these days in Amsterdam.
The new version now supports the modeling of behavior for component types in terms of finite-state machines and the verification of corresponding contracts using model checking.
Soon we will provide a preprint of our FACS paper which describes all the extensions in detail and demonstrates them by means of a running example.
Dr. Diego Marmsoler 