|:. News: The version 2.0 of the Charmy Tool is now available|
Charmy (CHecking ARchitectural Model consistencY) is a framework that aims at assisting the software architect in designing Software Architectures and in validating them against functional requirements. State machines and scenarios are the source notations for specifying Software Architectures and their behavioral properties. Model checking techniques are used to check the consistency between the software architecture and the functional requirements. The model checker SPIN is the verification engine in Charmy; a Promela specification and Buchi Automata, modelling the software architecture and the requirements respectively, are both derived from the source notations. SPIN takes in input such specifications and performs model checking. A software process is associated to the framework to help identifying and refining architectural models. Charmy supports also a compositional verification of properties and formal analysis of architectural patterns. Finally, Charmy is tool supported. It offers a graphical user interface which helps to specify the software architecture and automates the approach.