Using B Formal Method to Define Software Architecture Behavioral Concepts


(*) Corresponding author


Authors' affiliations


DOI's assignment:
the author of the article can submit here a request for assignment of a DOI number to this resource!
Cost of the service: euros 10,00 (for a DOI)

Abstract


Software architecture is an important key that guarantees services and an effective analysis tool that ensures efficient verification properties of software systems. This is confirmed by using architecture description languages (ADL). The precise semantics of B method and its powerful data abstraction allow software architects to specify architectural elements behavior explicitly, to verify their semantics using powerful tools that are designed for the B method. In this paper,  we define the behavioral aspects of software architecture using the B method. We use this formal method to define the behavioral aspects of COSA, which is a metamodel for software architecture. We also provide a B formal specification of the proposed aspects.
Copyright © 2017 Praise Worthy Prize - All rights reserved.

Keywords


Software Architecture; ADLs; Transition; Behavioral Concepts; B Method

Full Text:

PDF


References


N. Medvidovic, R.N. Taylor, A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering, Vol. 26. N°. 1. 2–57, 2000.

A. Smeda, M. Oussalah, T. Khammaci, A multi-paradigm approach to describe software systems, WSEAS Transactions on Computers, vol. 3, N°. 4, 936-941, 2004.

M. Oussalah, A. Smeda, T. Khammaci, An explicit definition of connectors for component based software architecture. In: Proceedings of the 11th IEEE Conference Engineering of Computer Based Systems (ECBS’2004), Czech Republic (May 2004).

D.E. Perry, A.L. Wolf, Foundations for the Study of Software Architecture. ACM SIGSOFT Software Engineering Notes, Vol. 17, N°. 4, pp.40-52, 1992.

M. Shaw, D. Garlan, Software Architecture: Perspectives on an Emerging Discipline. Prentice-Hall, Upper Saddle River, (1996).

J. Magee, N. Dulay, S. Eisenach, J. Kramer, Specifying Distributed Software Architectures. In Proceedings of the 5th European Software Engineering Conference, (September 1996).

D.C.Luckham, L.M.Augustin, J.V. Kenny, D. Bryan, W. Mann, Specification and Analysis of System architecture using Rapid. IEEE Transactions on Software Engineering, Vol. 21, N°. 4, 336-355, 1995.

A. Allen, D. Garlan, A Formal Basis of Architectural Connection. ACM Transitions on Software Engineering and Methodology, Vol. 6, N°. 3, pp. 213 – 249, 1997.

M. Graiet, M.T. Bhiri, F. Dammak, J.P. Giraudin, Adaptation d’UML 2.0 à l’ADL Wright. In Proceedings of the 1PstP Conference Francophone sur les Achitectures Logicielles (CAL’06), pp.83- 96, 2006.

F. Oquendo, π-ADL: an Architecture Description Language Based on the Higher Order Typed π-calculus for Specifying Dynamic and Mobile Software Architecture. Int. ACM SIGSOFT Software Engineering Notes, Vol. 29. N°. 4, January 2004.

F. Oquendo, S. Cimpan, H. Verjus, The Archware ADL: Definition of the Abstract Syntax and Formal Semantics. Deliverable D1.1b. Archware RTD Project IST-2001-32360.

Kozen D, Results on the Propositional (-calculus. Theoretical Computer Science. Vol. 27, pp. 333 -354, 1992.

Milner R, Communicating and Mobile Systems: the π-calculus. ISBN 052164320, Cambridge University, Press.

Kozen D, Results on the Propositional m-calculus. Theoretical Computer Science. Vol. 27, pp. 333 -354, 1992.

J.R. Abrial, The B-Book: Assigning Programs to Meanings. Cambridge University Press, (Aug 1996).

R.N. Taylor and N. Medvidovic, A Component and Message-based Architectural Styles for GHI software. IEEE Transactions on Software Engineering, Vol. 22, No. 6, June 1996.

P. Behm, P. Desforges, and J.M. Meynadier, M’ET’EOR: An Industrial Success in Formal Development", An invited talk at the 2PndP Int. B conference, LNCS 1939, (April 1998).

A. Alti, T. Khammaci, A. Smeda, Representing and Formally Modeling COSA Software Architecture with UML 2.0 Profile, (2007) International Review on Computers and Software (IRECOS), 2 (1), pp. 30-37.

B-ecore Limited: Oxford, United Kingdom, HTUhttp://www.b-core.comUTH .

Stéria Méditerranée: Aix-en-Provence, France, HTUhttp://www.atelierb.societe.comUTH .

J.R. Abrial, Introducing Dynamic Constraints in B, In D. Bert (Ed.), B’99: Recent Advances in the Development and Use of the B Method, (LNCS: Springer-Verlag, 1998, 83-128).


Refbacks

  • There are currently no refbacks.


Please send any question about this web site to info@praiseworthyprize.com
Copyright © 2005-2024 Praise Worthy Prize