Welcome to UMC
|
UMC is a verification framework developed at the FM&&T Laboratory of ISTI-CNR for the definition,
exploration, analysis and model checking of system designs represented as a set of (UML) state machines.
Starting with the selection of the "Model Definition ..." command on the left it is possible to browse examples of system designs or experiment with the creation and analysis of new models. The available documentation about this framework (see the provided links) is unfortunately not very recent, but we hope to fix the gap in a near future. In the meanwhile, the online Syntax Help and the interactive syntax driven model editing feature allow to get a partial but still meaningful idea of the supported constructs. |
| Documentation The Structure of UMC Models (vers. 3.7) The Structure of UMC Logics(vers. 3.3) ... other ... | Sample Code: Some examples of UMC models Support and Bug Reports: franco.mazzanti@isti.cnr.it |
Download:
A binary distribution of the command-line oriented version of UMC for Linux/ SunSparc/ Windows/ Mac OSX is available.
The full framework (http server code + binaries) for MacOS is also available upon request,
also in the form of a desktop MacOS application.
A selection of deprecated legacy version of UMC are still accessible online.
Requirements:
Any modern browser with javascript, HTML5 and SVG support.
| Author/Contact/Support: | Credits: |
|
Franco Mazzanti franco.mazzanti@isti.cnr.it http://fmt.isti.cnr.it/~mazzanti |
Graphics generated with GraphViz
(http://www.graphviz.org/) Graph minimization with ltsconvert of the MCRL2 toolset (http://mcrl2.org/) Text editing supported by ACE (http://ace.ajax.org) Software developed with Adacore Gnat Ada (http://www.adacore.com) |
If you plan to cite the KandISTI/UMC toolset in your academic papers, you can use one of the following references:
• M.H. ter Beek, A. Fantechi, S. Gnesi, F. Mazzanti
From EU projects to a family of model checkers
Lecture Notes in Computer Science Volume 8950, 2015, Pages 312-328
• Stefania Gnesi and Franco Mazzanti:
An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems
Lecture Notes in Computer Science 6582, pp. 390-407, 2011
• M.H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti
A state/event-based model-checking approach for the analysis of abstract system properties
Science of Computer Programming 76, 2 (2011), 119 - 135.
The pictures on the left side represent paintings of Wassily Kandinsky (1866 - 1944).
The painter view of the world has evolved in time from "ground" to "abstract".
We suggest a similar approach also for the analysis of computing systems.
