Software environment for the formal specification and verification of dynamic systems
CosyVerif is a software environment whose goal is the formal specification and verification of dynamic systems.
This environment consists of two software tools: CosyDraw, the graphical interface; and Alligator, an integration framework web service. CosyVerif is enlarged with the existing verification tools developed in our laboratories (founding members or partners).
Support different formalisms and offer the possibility to create and integrate new tools
Provide a graphical interface for every formalism
Include verification tools called via the interface as a web service
Platform for verification of complex systems
Petite vidéo de la toute jeune version 2 de CosyVerif, un environnement de vérification développé conjointement par le @LIP6_lab, le @LipnLab et le @lmf_lab (tous trois de l'@INS2I_CNRS)
CosyVerif is launching its new website! come to http://www.cosyverif.org and check it out for yourself !
End of summer internship on formalisms for Hdadech Nizar and Paul Panganiban. Cosy now has modular expressions. Great job!
Luca Saiu is at #unige for 3 days to work on #CosyVerif!
The development of CosyVerif has been decided and it is supported by three partners of the Parisian verification group, MeFoSyLoMa, which is composed of seven teams. The founding members of CosyVerif are LMF, LIP6, and LIPN.
First, these members aim at sharing their tools, comparing and supporting industrial case studies and finally making them long-lasting. Second, they also want to promote the practice of formal verification in industry and thus they intend to ease the task of integration of new formalisms and tools.
CosyVerif is managed by a steering committee consisting of researchers and engineers. It decides strategic orientations as well as technical choices.
Three formalisms are supported: attack-defense trees, automata, and Petri nets, the latter two with extensions.
Most of the tools are related to Petri nets. Some of them perform structural analyses like invariant computations while other tools perform behavioural analyses: symbolic reachability graph building, unfolding, stochastic simulations, etc. Finally some of them transform high-level nets into low-level ones.
All the developed software are open source and free software tools.
Alligator is published under the GNU Affero General Public License (AGPL), version 3.
CosyDraw is published under the GNU General Public License (GPL), version 3.