CHARMY: an extensible tool for architectural analysis

ABSTRACT

CHARMY is a framework for designing and validating architectural specifications. In the early stages of the software development process, the CHARMY framework assists the software architect in the design and validation phases. To increase its usability in an industrial context, the tool allows the use of UML-like notations to graphically design the system. Once the design is done, a formal prototype is automatically created for simulation and analysis purposes. The framework provides extensibility mechanisms to enable the introduction of new design and analysis features.

REFERENCES

• 1: ADML: Architecture Description Markup Language. http://www.opengroup.org/architecture/adml/adml_home.htm, Last Modified: December 2002. Open Group.
• 2: A. Bucchiarone, H. Muccini, P. Pelliccione, and P. Pierini. Model-Checking plus Testing: from Software Architecture Analysis to Code Testing. In Proc. Int. Workshop on Integration of Testing Methodologies, ITM '04. LNCS n.3236.
• 3: M. Autili, P. Inverardi, P. Pelliccione. Graphical Scenarios for Specifying Temporal Properties: an Automatic Approach. Technical report, University of L'Aquila, April 2005.
• 4: M. Caporuscio, P. Inverardi, and P. Pelliccione. Formal analysis of architectural patterns. In First European Workshop on Software Architecture - EWSA 2004, 21-22 May 2004, St Andrews, Scotland, UK. LNCS n.3047.
• 5: Mauro Caporuscio , Paola Inverardi , Patrizio Pelliccione, Compositional Verification of Middleware-Based Software Architecture Descriptions, Proceedings of the 26th International Conference on Software Engineering, p.221-230, May 23-28, 2004
• 6: Charmy Project. Charmy web site. http://www.di.univaq.it/charmy, February 2004.
• 7: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2001.
• 8: D. Compare, P. Inverardi, P. Pelliccione, and A. Sebastiani. Integrating model-checking architectural analysis and validation in a real software life-cycle. In FME 2003, LNCS 2805, pages 114--132, Pisa, 2003.
• 9: Formal Methods for Software Architectures. Tutorial book on Software Architectures and Formal Methods. Eds. M. Bernardo and P. Inverardi, LNCS 2804, 2003.
• 10: David Garlan, Software architecture: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.91-101, June 04-11, 2000, Limerick, Ireland [doi>10.1145/336512.336537]
• 11: G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, September 2003.
• 12: P. Pelliccione, P. Inverardi, and H. Muccini. Charmy: A framework for Designing and Validating Architectural Specifications. Submitted for publication. Technical report, University of L'Aquila, April 2005.
• 13: jSpin - A Java GUI for Spin. http://stwww.weizmann.ac.il/g-cs/benari/jspin/.
• 14: Nenad Medvidovic , Richard N. Taylor, A Classification and Comparison Framework for Software Architecture Description Languages, IEEE Transactions on Software Engineering, v.26 n.1, p.70-93, January 2000 [doi>10.1109/32.825767]
• 15: P. Pelliccione, H. Muccini, A. Bucchiarone, and F. Facchini. TeStor: Deriving Test Sequences from Model-based Specifications 8th International SIGSOFT Symposium on Component-based Software Engineering. May 2005, St. Louis, Missouri, USA. LNCS 3489, pp. 267--282.
• 16: Judith A. Stafford , Alexander L. Wolf, Architecture-level dependence analysis in support of software maintenance, Proceedings of the third international workshop on Software architecture, p.129-132, November 01-05, 1998, Orlando, Florida, United States [doi>10.1145/288408.288441]
• 17: xADL 2.0 Architecture Description Language. http://www.isr.uci.edu/projects/xarchuci/, 2005.
• 18: J. Zhao Software Architecture Slicing. In Proceedings of the 14th Annual Conference of Japan Society for Software Science and Technology (1997).

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Design, Verification

Keywords:
model checking, software architectures