This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
CHARMY: A Framework for Designing and Verifying Architectural Specifications
May/June 2009 (vol. 35 no. 3)
pp. 325-346
ASCII Text
x 
 
Patrizio Pelliccione, Paola Inverardi, Henry Muccini, "CHARMY: A Framework for Designing and Verifying Architectural Specifications," IEEE Transactions on Software Engineering, vol. 35, no. 3, pp. 325-346, May/June, 2009.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2008.104,
author = {Patrizio Pelliccione and Paola Inverardi and Henry Muccini},
title = {CHARMY: A Framework for Designing and Verifying Architectural Specifications},
journal ={IEEE Transactions on Software Engineering},
volume = {35},
number = {3},
issn = {0098-5589},
year = {2009},
pages = {325-346},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.104},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - CHARMY: A Framework for Designing and Verifying Architectural Specifications
IS - 3
SN - 0098-5589
SP325
EP346
EPD - 325-346
A1 - Patrizio Pelliccione,
A1 - Paola Inverardi,
A1 - Henry Muccini,
PY - 2009
KW - Software architectures
KW - model checking.
VL - 35
JA - IEEE Transactions on Software Engineering
ER -
 
Patrizio Pelliccione, Università dell' Aquila, L'Aquila
Paola Inverardi, Università dell' Aquila, L'Aquila
Henry Muccini, Università dell' Aquila, L'Aquila
Introduced in the early stages of software development, the Charmy framework assists the software architect in making and evaluating architectural choices. Rarely, the software architecture of a system can be established once and forever. Most likely poorly defined and understood architectural constraints and requirements force the software architect to accept ambiguities and move forward to the construction of a suboptimal software architecture. Charmy aims to provide an easy and practical tool for supporting the iterative modeling and evaluation of software architectures. From an UML-based architectural design, an executable prototype is automatically created. Charmy simulation and model checking features help in understanding the functioning of the system and discovering potential inconsistencies of the design. When a satisfactory and stable software architecture is reached, Java code conforming to structural software architecture constraints is automatically generated through suitable transformations. The overall approach is tool supported.

[1] Formal Methods for Software Architectures, Tutorial book on software architectures and formal methods, M. Bernardo and P.Inverardi, eds. Springer, 2003.
[2] J. Aldrich, “Using Types to Enforce Architectural Structure,” Proc. Working IEEE/Int'l Federation for Information Processing (IFIP) Conf. Software Architecture, pp.211-220, 2008.
[3] R. Allen and D. Garlan, “A Formal Basis for Architectural Connection,” ACM Trans. Software Eng. and Methodology, vol. 6, no. 3, pp.213-249, July 1997.
[4] M. Autili, P. Inverardi, and P. Pelliccione, “Graphical Scenarios for Specifying Temporal Properties: An Automated Approach,” Automated Software Eng., vol. 14, no. 3, pp.293-340, Sept. 2007.
[5] H. Baumeister, F. Hacklinger, R. Hennicker, A. Knapp, and M. Wirsing, “A Component Model for Architectural Programming,” Electronic Notes in Theoretical Computer Science, vol. 160, pp.75-96, 2006.
[6] A. Bucchiarone, D. Di Ruscio, H. Muccini, and P. Pelliccione, “From Requirements to Code: An Architecture-Centric Approach for Producing Quality Systems,” Chapter of The Book Model-Driven Software Development: Integrating Quality Assurance, IRM Press, CyberTech Publishing and Idea Group Reference Imprints, 2008.
[7] R.J. Büchi, “On a Decision Method in Restricted Second Order Arithmetic,” Proc. Int'l Congress of Logic, Methodology and Philosophy of Science, pp.1-11, 1960.
[8] F. Budinsky, D. Steinberg, E. Merks, R. Ellersick, and T. Grose, Eclipse Modeling Framework. Addison Wesley, 2003.
[9] M. Caporuscio, P. Inverardi, and P. Pelliccione, “Formal Analysis of Architectural Patterns,” Proc. European Workshop Software Architecture, 2004.
[10] M. Caporuscio, P. Inverardi, and P. Pelliccione, “Compositional Verification of Middleware-Based Software Architecture Descriptions,” Proc. Int'l Conf. Software Eng., 2004.
[11] Charmy Project, Charmy Website, http://www.di.univaq.itcharmy and http://sourceforge.orgcharmy, June 2008.
[12] E.M. Clarke, O. Grumbeg, and D.A. Peled, Model Checking. MIT Press, 2001.
[13] D. Colangelo, D. Compare, P. Inverardi, and P. Pelliccione, “Reducing Software Architecture Models Complexity: A Slicing and Abstraction Approach,” Proc. Formal Techniques for Networked and Distributed Systems Conf., 2006.
[14] D. Compare, P. Inverardi, P. Pelliccione, and A. Sebastiani, “Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle,” Proc. Int'l Symp. Formal Methods, 2003.
[15] D. Compare, P. Inverardi, and A. Wolf, “Uncovering Architectural Mismatch in Dynamic Behavior,” Science of Computer Programming, vol. 33, no. 2, pp.101-131, Feb. 1999.
[16] P. Gagnon, F. Mokhati, and M. Badri, “Applying Model Checking to Concurrent UML Models,” Object Technology, vol. 7, no. 1, pp.59-84, 2008.
[17] D. Garlan, R.T. Monroe, and D. Wile, “Acme: Architectural Description of Component-Based Systems,” Foundations of Component-Based Systems, Cambridge Univ. Press, 2000.
[18] H. Goldsby, B.H.C. Cheng, S. Konrad, and S. Kamdoum, “A Visualization Framework for the Modeling and Formal Analysis of High Assurance Systems,” Proc. Int'l Conf. Model Driven Eng. Languages and Systems, 2006.
[19] C.A.R. Hoare, “Communicating Sequential Processes,” Comm. ACM, vol. 21, no. 8, pp.666-677, 1978.
[20] C. Hofmeister, P. Kruchten, R.L. Nord, H. Obbink, A. Ran, and P. America, “A General Model of Software Architecture Design Derived from Five Industrial Approaches,” J. Systems and Software, vol. 80, no. 1, pp.106-126, 2007.
[21] G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Sept. 2003.
[22] L. Lamport, “What Good Is Temporal Logic?” Proc. Int'l Federation of Information Processing Ninth World Congress, 1983.
[23] J. Magee and J. Kramer, Concurrency: State Models & Java Programs, second ed. John Wiley & Sons, 2006.
[24] J. Magee, J. Kramer, and D. Giannakopoulou, “Behaviour Analysis of Software Architectures,” Proc. Working IEEE/Int'l Federation for Information Processing Conf. Software Architecture, 1999.
[25] W.E. McUmber and B.H.C. Cheng, “A General Framework for Formalizing UML with Formal Languages,” Proc. Int'l Conf. Software Eng., 2001.
[26] H. Muccini, A. Bertolino, and P. Inverardi, “Using Software Architecture for Code Testing,” IEEE Trans. Software Eng., vol. 30, no. 3, pp.160-171, Mar. 2004.
[27] D. Peled, P. Pelliccione, and P. Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 5-Volume Set, Chapter Model Checking. Wiley, 2009.
[28] P. Pelliccione, “CHARMY: A Framework for Software Architecture Specification and Analysis,” PhD thesis, Computer Science Dept., Univ. of L'Aquila, May 2005.
[29] P. Pelliccione, H. Muccini, A. Bucchiarone, and F. Facchini, “Testor: Deriving Test Sequences from Model-Based Specifications,” Proc. Int'l Symp. Component-Based Software Eng., 2005.
[30] P. Pelliccione, M. Tivoli, A. Bucchiarone, and A. Polini, “An Architectural Approach to the Correct and Automatic Assembly of Evolving Component-Based Systems,” J. Systems and Software, doi:http://dx.doi.org/10.1016j.jss.2008.05.030, 2008.
[31] J.E. Perez-Martinez and A. Sierra-Alonso, “UML 1.4 Versus UML2.0 as Languages to Describe Software Architectures,” Proc. European Workshop Software Architecture, 2004.
[32] D.E. Perry and A.L. Wolf, “Foundations for the Study of Software Architecture,” ACM SIGSOFT Software Eng. Notes, vol. 17, no. 4, pp.40-52, Oct. 1992.
[33] Robby, E. Rodriguez , M.B. Dwyer, and J. Hatcliff, “Checking Strong Specifications Using an Extensible Software Model Checking Framework,” Proc. Int'l Conf. Tools and Algorithms for the Construction of Analysis of Systems, Mar. 2004.
[34] S. Roh, K. Kim, and T. Jeon, “Architecture Modeling Language Based on UML 2.0,“ Proc. Asia-Pacific Software Eng. Conf., 2004.
[35] M. Shaw and D. Garlan, Software Architecture: Perspectives on an Emerging Discipline. Prentice-Hall, 1996.
[36] J.A. Stafford, A.L. Wolf, and M. Caporuscio, The Application of Dependence Analysis to Software Architecture Descriptions. Springer-Verlag, 2003.
[37] The SAE Architecture Analysis and Design Language (AADL), http:/www.aadl. info/, 2009.
[38] M. Tivoli and P. Inverardi, “Failure-Free Coordinators Synthesis for Component-Based Architectures,” Science of Computer Programming, vol. 71, no. 3, pp.181-212, 2008.
[39] S. Uchitel, J. Kramer, and J. Magee, “Incremental Elaboration of Scenario-Based Specifications and Behavior Models Using Implied Scenarios,” ACM Trans. Software Eng. and Methodologies, vol. 13, no. 1, pp.37-85, 2004.

Index Terms:
Software architectures, model checking.
Citation:
Patrizio Pelliccione, Paola Inverardi, Henry Muccini, "CHARMY: A Framework for Designing and Verifying Architectural Specifications," IEEE Transactions on Software Engineering, vol. 35, no. 3, pp. 325-346, May-June 2009, doi:10.1109/TSE.2008.104
Usage of this product signifies your acceptance of the Terms of Use.