Publications ©

Home     Top

 

Technical reports 

Home     Top

 

Other presentations

Home     Top

 

Tools

  • CMC: an on-the-fly model checker and interpreter for COWS
    CMC is a tool supporting specification and verification of COWS terms. In particular, CMC supports model checking of SocL formulae and deriving all computations originating from a COWS term in an automated way. A prototypical version of CMC, developed by Franco Mazzanti at ISTI-CNR of Pisa, can be experimented via a web interface available at the address http://fmt.isti.cnr.it/cmc, or by downloading from the same address a binary distribution (for Linux, Solaris, Windows or MacOSX platforms). The CMC core consists of a command-line-oriented version of the model checker, which is a stand-alone program written in Ada. This executable core is wrapped with a set of CGI scripts handled by a web server to provide it with an HTML-oriented GUI.
    help     link    

  • UStoC: an compiler from UML4SOA to COWS
    UStoC is a software tool that automatises an encoding of the UML profile UML4SOA in the process calculus COWS. The COWS terms generated by UStoC are written in the syntax accepted by CMC.

  • Venus: A Verification ENvironment for UML models of Services
    Venus is a software tool that aims at automatising, as much as possible, the verification process of service models specified by using the UML4SOA profile, actually hiding to the (non-expert) user the underlying formal methods and theories. This way, developers can concentrate on modelling the high-level behaviour of the system and use Venus at an intuitive level for analysing it. Venus takes as an input service models specified by UML 2.0 activity diagrams according to the profile UML4SOA, while its theoretical bases are the process calculus COWS and the temporal logic SocL. Venus is composed of three main components: a graphical user interface, the automatic translator UStoC from UML4SOA into COWS, and the model checker  CMC supporting verification of SocL formulae over COWS terms.
    binaries     sources    old version

Home     Top

Theses

Home     Top

 

People

Post-doc       (fbanti 63481232298387chiocciola.GIF gmail.com)
Full Professor       (fantechi 63481232298387chiocciola.GIF dsi.unifi.it)
Director of Research at ISTI-CNR       (stefania.gnesi 63481232298387chiocciola.GIF isti.cnr.it)
Post-doc (lapadula 63481232298387chiocciola.GIF dsi.unifi.it)
PhD Student
(masi 63481232298387chiocciola.GIF math.unifi.it)
Researcher at ISTI-CNR       (franco.mazzanti 63481232298387chiocciola.GIF isti.cnr.it)
Associate Professor (pugliese 63481232298387chiocciola.GIF dsi.unifi.it)
Post-doc (tiezzi 63481232298387chiocciola.GIF dsi.unifi.it)