Patrizio Pelliccione

Dipartimento di Informatica, Università degli Studi dell'Aquila
Via Vetoio, I-67010 L'Aquila (Italy)


Charmy is a tool which allows the specification of a software system SA through diagrammatic, UML-based notations, and the validation of the architectural specification conformance with respect to certain functional requirements. Charmy offers a graphical user interface to draw state diagrams and scenarios, used to specify the SA behavior and the functional requirements, respectively. A translation engine automatically derives formal specifications out of the diagrammatic notations, and the SPIN model-checker is used for automatic verification on such specifications. XMI is the output format of Charmy. Moreover, the framework provides extensibility mechanisms via a plugin-based architecture) to enable the introduction of new features and to help the integration with other existing analysis tools. The tool main benefits are that it is UML-based (thus easily integrable in industrial development processes), it automatically produces a formal prototype of the SA and modelchecks it with SPIN (without requiring formal languages skills), and it is extensible, due to its plugin architecture.