π-Method: a model-driven formal method for architecture-centric software engineering

ABSTRACT

Software systems have become increasingly complex and are often used in highly dynamic, distributed and mobile environments. Formal development of such software systems in order to guarantee their completeness and correctness is a large research challenge. This article presents the π-Method, a novel formal method that has been designed in the ArchWare European Project to address model-driven development of safe software systems. It is a well-founded theoretically method relying on formal foundations: its formal language for architecture description is based on the π-calculus, for architecture analysis on the μ-calculus, and for architecture transformation and refinement on the rewriting logic. The π-Method, like formal methods such as B, FOCUS, VDM, and Z, aims to provide full support for formal development of software systems. However, unlike these methods that do not provide any architectural support, the π-Method has been built from scratch to formally support architecture-centric component-based model-driven development. Furthermore, a major impetus behind defining formal languages and method is that their formality renders them suitable to be manipulated by software tools. Indeed, a comprehensive toolset supporting formal model-driven engineering has been developed.

REFERENCES

• 1: Oquendo F., Warboys B., Morrison R. (Eds.): Software Architecture, Springer-Verlag, LNCS 3047, May 2004.
• 2: Flavio Oquendo, π-ADL: an Architecture Description Language based on the higher-order typed π-calculus for specifying dynamic and mobile software architectures, ACM SIGSOFT Software Engineering Notes, v.29 n.3, May 2004 [doi>10.1145/986710.986728]
• 3: Flavio Oquendo, π-ARL: an architecture refinement language for formally modelling the stepwise refinement of software architectures, ACM SIGSOFT Software Engineering Notes, v.29 n.5, September 2004 [doi>10.1145/1022494.1022517]
• 4: Flavio Oquendo, Formally refining software architectures with π-ARL: a case study, ACM SIGSOFT Software Engineering Notes, v.29 n.5, September 2004 [doi>10.1145/1022494.1022518]
• 5: Derniame J-C., Oquendo F.: Key Issues and Future Directions in Software Process Technology. Novática Journal, Special Issue on Software Process Technologies (invited paper), No. 171, September-October 2004 and co-printed at the European Journal: CEPIS Upgrade, Vol. V, No. 5, October 2004.
• 6: Oquendo F.: Les architectures logicielles. Encyclopédie de l'informatique et des systèmes d'information, Editions Vuibert (In French) (To appear in 2006, In French).
• 7: Flavio Oquendo, Formally modelling software architectures with the UML 2.0 profile for π-ADL, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006 [doi>10.1145/1108768.1108773]
• 8: Alloui I., Oquendo F.: Describing Software-intensive Process Architectures using a UML-based ADL. Proceedings of the Sixth International Conference on Enterprise Information Systems (ICEIS'04), Porto, Portugal, April 2004.
• 9: Blanc-Dit-Jolicoeur L., Braesch C., Cimpan S., Leymonerie F., Oquendo F.: Towards a Business Process Formalisation based on an Architecture-centred Approach. Proceedings of the Sixth International Conference on Enterprise Information Systems (ICEIS'04), Porto, Portugal, April 2004.
• 10: Ratcliffe O., Cimpan S., Oquendo F., Scibile L.: Formalization of an HCI Style for Accelerator Restart Monitoring. Proceedings of the First European Workshop on Software Architecture (EWSA'04), Lecture Notes in Computer Science, Springer Verlag, St Andrews, UK, May 2004.
• 11: Oquendo F., Warboys B., Morrison R., Dindeleux R., Gallo F., Garavel H., Occhipinti C.: Arch Ware: Architecting Evolvable Software. Proceedings of the First European Workshop on Software Architecture (EWSA'04), European Projects in Software Architecture -- Invited Paper, Lecture Notes in Computer Science, Springer Verlag, St Andrews, UK, May 2004.
• 12: Azaiez S., Oquendo F.: GAMA: Towards Architecture-centric Software Engineering of Mobile Agent Systems. Proceedings of the Third International Workshop on Software Engineering for Large-Scale Multi-Agent Systems (SELMAS 2004) at the IEEE/ACM International Conference on Software Engineering (ICSE 2004), Edinburgh, UK, May 2004.
• 13: Support for Evolving Software Architectures in the ArchWare ADL, Proceedings of the Fourth Working IEEE/IFIP Conference on Software Architecture (WICSA'04), p.69, June 12-15, 2004
• 14: Azaiez S., Pourraz F., Verjus H., Oquendo F.: Validation by Animation: Animating Software Architectures based on the π-Calculus. Proceedings of the Third Workshop on System Testing and Validation (SV'04), Paris, France, December 2004.
• 15: Ratcliffe O., Scibile L., Cimpan S., Oquendo F.: Towards an Inductive Definition and Evolution of Architectural Styles. Proceedings of the Seventeenth International Conference on Software and Systems Engineering and their Applications (ICSSEA'04), Paris, France, December 2004.
• 16: Revillard J., Benoit E., Cimpan S., Oquendo F.: Architecture-Centric Development for Intelligent Instrument Design. IEEE International Conference on Computational Intelligence for Measurement Systems and Applications (CIMSA 2005), Giardini Naxos, Italy, July 2005.
• 17: Jerome Revillard , Sorana Cimpan , Eric Benoit , Flavio Oquendo, Intelligent Instrument Design With ArchWare ADL, Proceedings of the 5th Working IEEE/IFIP Conference on Software Architecture (WICSA'05), p.249-250, November 06-10, 2005 [doi>10.1109/WICSA.2005.40]
• 18: Olivier Ratcliffe , Sorana Cimpan , Flavio Oquendo, Case Study on Architecture-Centered Design for Monitoring Views at CERN, Proceedings of the 5th Working IEEE/IFIP Conference on Software Architecture (WICSA'05), p.213-214, November 06-10, 2005 [doi>10.1109/WICSA.2005.20]
• 19: Manset D., McClatchey R., Oquendo F., Verjus H.: "A Model-Driven Approach for Grid Services Engineering", Proceedings of the Eighteenth International Conference on Software and Systems Engineering and their Applications (ICSSEA'05), Paris, France, December 2005.
• 20: Oquendo F.: UML 2.0 Profile for the ArchWare Architecture Description Language. Deliverable D1.8, ArchWare European RTD Project, IST-2001-32360, June 2005.
• 21: Oquendo F.: Tutorial of the ArchWare Architecture Description Language. Deliverable D1.9, ArchWare European RTD Project, IST-2001-32360, June 2005.
• 22: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 23: Robert John Allen , David Garlan, A formal approach to software architecture, 1997
• 24: Allen R., Douence R., Garlan D.: Specifying and Analyzing Dynamic Software Architectures. In Fundamental Approaches to Software Engineering, LNCS 1382, Springer Verlag, 1998.
• 25: M. Bernardo , P. Ciancarini , L. Donatiello, Architecting Software Systems with Process Algebras, University of Bologna, 2001
• 26: Marco Bernardo , Paolo Ciancarini , Lorenzo Donatiello, Detecting Architectural Mismatches in Process Algebraic Descriptions of Software Systems, Proceedings of the Working IEEE/IFIP Conference on Software Architecture (WICSA'01), p.77, August 28-31, 2001 [doi>10.1109/WICSA.2001.948411]
• 27: Binns P., Engelhart M., Jackson M., Vestal S.: Domain-Specific Software Architectures for Guidance, Navigation, and Control. International Journal of Software Engineering and Knowledge Engineering. 1996.
• 28: Bolusset T., Oquendo F.: Formal Refinement of Software Architectures Based on Rewriting Logic, ZB2002 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, Grenoble, Janvier 2002.
• 29: Brown A. W.: An Introduction to Model Driven Architecture -- Part I: MDA and Today's Systems. The Rational Edge, February 2004.
• 30: Chaudet C., Greenwood M., Oquendo F., Warboys B.: Architecture-Driven Software Engineering: Specifying, Generating, and Evolving Component-Based Software Systems. IEE Journal: Software Engineering, Vol. 147, No. 6, UK, December 2000.
• 31: Christelle Chaudet , Flavio Oquendo, p-SPACE: A Formal Architecture Description Language Based on Process Algebra for Evolving Software Systems, Proceedings of the 15th IEEE international conference on Automated software engineering, p.245, September 11-15, 2000
• 32: Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 33: Robert DeLine, Toward user-defined element types and architectural styles, Joint proceedings of the second international software architecture workshop (ISAW-2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops, p.47-49, October 16-18, 1996, San Francisco, California, United States [doi>10.1145/243327.243351]
• 34: Jean-Claude Fernandez , Hubert Garavel , Alain Kerbrat , Laurent Mounier , Radu Mateescu , Mihaela Sighireanu, CADP - A Protocol Validation and Verification Toolbox, Proceedings of the 8th International Conference on Computer Aided Verification, p.437-440, August 03, 1996
• 35: Fischer M. J., Ladner R. E.: Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences Vol. 18, 1979.
• 36: Garavel H.: Compilation et Vérification de Programmes LOTOS. Thèse de Doctorat, Univ. Joseph Fourier (Grenoble), November 1989. Chapter 9: Vérification (In French).
• 37: Garavel H., Lang F., Mateescu R.: An Overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter, Vol. 4, August 2002.
• 38: David Garlan , Robert Allen , John Ockerbloom, Exploiting style in architectural design environments, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.175-188, December 06-09, 1994, New Orleans, Louisiana, United States
• 39: David Garlan , Robert Monroe , David Wile, Acme: an architecture description interchange language, Proceedings of the 1997 conference of the Centre for Advanced Studies on Collaborative research, p.7, November 10-13, 1997, Toronto, Ontario, Canada
• 40: David Garlan , Robert T. Monroe , David Wile, Acme: architectural description of component-based systems, Foundations of component-based systems, Cambridge University Press, New York, NY, 2000
• 41: Greenwood M., Balasubramaniam D., Cimpan S., Kirby N. C., Mickan K., Morrison R., Oquendo F., Robertson I., Seet W., Snowdon R., Warboys B., Zirintsis E.: Process Support for Evolving Active Architectures, Proceedings of the 9th European Workshop on Software Process Technology, LNCS 2786, Springer Verlag, Helsinki, September 2003.
• 42: Jan Friso Groote , Radu Mateescu, Verification of Temporal Properties of Processes in a Setting with Data, Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, p.74-90, January 04-08, 1999
• 43: Maritta Heisel , Nicole Lévy, Using LOTOS Patterns to Characterize Architectural Styles, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.818-832, April 14-18, 1997
• 44: Paola Inverardi , Alexander L. Wolf, Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model, IEEE Transactions on Software Engineering, v.21 n.4, p.373-386, April 1995 [doi>10.1109/32.385973]
• 45: Paola Inverardi , Alexander L. Wolf , Daniel Yankelevich, Static checking of system behaviors using derived component assumptions, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.3, p.239-272, July 2000 [doi>10.1145/352591.352593]
• 46: Kerschbaumer A.: Non-Refinement Transformation of Software Architectures. Proceedings of the ZB2002 International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, Grenoble, Janvier 2002.
• 47: Kozen D.: Results on the Propositional μ-Calculus. Theoretical Computer Science 27:333--354, 1983.
• 48: Leymonerie F., Cimpan S., Oquendo F.: Extension d'un langage de description architecturale pour la prise en compte des styles architecturaux: application à J2EE. Proceedings of the 14th International Conference on Software and Systems Engineering and their Applications. Paris, December 2001 (In French).
• 49: Leymonerie F., Cimpan S., Oquendo F., État de l'art sur les styles architecturaux: classification et comparaison des langages de description d'architectures logicielles. Revue Génie Logiciel, No. 62, September 2002 (In French).
• 50: David C. Luckham , John J. Kenney , Larry M. Augustin , James Vera , Doug Bryan , Walter Mann, Specification and Analysis of System Architecture Using Rapide, IEEE Transactions on Software Engineering, v.21 n.4, p.336-355, April 1995 [doi>10.1109/32.385971]
• 51: Jeff Magee , Naranker Dulay , Susan Eisenbach , Jeff Kramer, Specifying Distributed Software Architectures, Proceedings of the 5th European Software Engineering Conference, p.137-153, September 25-28, 1995
• 52: Martí-Oliet N., Meseguer J., Rewriting Logic: Roadmap and Bibliography. Theoretical Computer Science, 2001.
• 53: Mateescu R., Garavel H., XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. Proceedings of the 1st International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998.
• 54: Medvidovic N., Taylor R.: A Classification and Comparison Framework for Architecture Description Languages. Technical Report UCI-ICS-97-02, Department of Information and Computer Science, University of California. Irvine, February 1997.
• 55: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 56: Monroe R.: Capturing Software Architecture Design Expertise with ARMANI. Technical Report CMU-CS-98-163, Carnegie Mellon University, January 2001.
• 57: Mark Moriconi , Xiaolei Qian , R. A. Riemenschneider, Correct Architecture Refinement, IEEE Transactions on Software Engineering, v.21 n.4, p.356-3, April 1995 [doi>10.1109/32.385972]
• 58: Moriconi M., Riemenschneider R. A.: Introduction to SADL 1.0: A Language for Specifying Software Architecture Hierarchies. Computer Science Laboratory, SRI International, Technical Report SRI-CSL-97-01, March 1997.
• 59: Morrison R.: On the Development of S-algol. PhD Thesis, University of St Andrews, 1979.
• 60: Jan Philipps , Bernhard Rumpe, Refinement of Pipe-and-Filter Architectures, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.96-115, September 20-24, 1999
• 61: RAPIDE Design Team: Guide to the RAPIDE 1.0. Language Reference Manuals, Stanford University, July 1997.
• 62: Rongviriyapanish S., Levy N.: Variations sur le Style Architectural Pipe and Filter. Actes du Colloque sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'00), Grenoble, France, January 2000.
• 63: Sangiorgi, D., Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD Thesis, University of Edinburgh, 1992.
• 64: Colin Stirling, Modal and temporal properties of processes, Springer-Verlag New York, Inc., New York, NY, 2001
• 65: Manfred Broy , Ketil Stølen, Specification and development of interactive systems: focus on streams, interfaces, and refinement, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 66: Strachey C.: Fundamental Concepts in Programming Languages. Oxford University Press, Oxford, 1967.
• 67: Tennent R. D.: Language Design Methods based on Semantic Principles. Acta Informatica 8, 1977.
• 68: David Wile, AML: An Architecture Meta-Language, Proceedings of the 14th IEEE international conference on Automated software engineering, p.183, October 12-15, 1999
• 69: Oquendo F.: The Arch Ware Architecture Refinement Language. Deliverable D6.1b, ArchWare European RTD Project, IST-2001-32360, December 2003.
• 70: Oquendo F. et al.: The ArchWare Architecture Description Language: Abstract Syntax and Formal Semantics. Deliverable D1.lb, ArchWare European RTD Project, IST-2001-32360, December 2002.
• 71: Radu Mateescu , Flavio Oquendo, π-AAL: an architecture analysis language for formally specifying and verifying structural and behavioural properties of software architectures, ACM SIGSOFT Software Engineering Notes, v.31 n.2, March 2006 [doi>10.1145/1118537.1118541]
• 72: Alloui I., Garavel H., Mateescu R., Oquendo F.: The ArchWare Architecture Analysis Language: Syntax and Semantics. Deliverable D3.lb, ArchWare European RTD Project, IST-2001-32360, January 2003.
• 73: Brian Warboys , Bob Snowdon , R. Mark Greenwood , Wykeen Seet , Ian Robertson , Ron Morrison , Dharini Balasubramaniam , Graham Kirby , Kath Mickan, An Active-Architecture Approach to COTS Integration, IEEE Software, v.22 n.4, p.20-27, July 2005 [doi>10.1109/MS.2005.86]
• 74: Warboys B. C., Greenwood R. M., Robertson I., Morrison R., Balasubramaniam D., Kirby G., Mickan K.: The ArchWare Tower: The Implementation of an Active Software Engineering Environment using a π-calculus based Architecture Description Language. Proceedings of the Second European Workshop on Software Architecture (EWSA'05), Pisa, Italy, Springer-Verlag, LNCS, 2005.
• 75: IEEE Std 1471-2000: IEEE Recommended Practice for Architectural Description of Software-Intensive Systems, October 2000.
• 76: John Fitzgerald , Peter Gorm Larsen, Modelling systems: practical tools and techniques in software development, Cambridge University Press, New York, NY, 1998
• 77: Miller J., Mukerji J.: MDA Guide Version 1.0.1, Document Number: OMG/2003-06-01, Object Management Group, June 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

General Terms:
Design, Languages

Keywords:
architecture analysis languages, architecture description languages, architecture transformation/refinement languages, architecture-centric software engineering, component-based software engineering, formal methods, model-driven development, software architectures