A Tile Logic Based Approach for Software Architecture Description Analysis

Aïcha Choutri, Faiza Belala, Kamel Barkaoui

.

DOI: 10.4236/jsea.2010.311126                

Abstract

A main advantage of Architecture Description Languages (ADL) is their aptitude to facilitate formal analysis and verification of complex software architectures. Since some researchers try to extend them by new techniques, we show in this paper how the use of tile logic as extension of rewriting logic can enforce the ability of existing ADL formalisms to cope with hierarchy and composition features which are more and more present in such software architectures. In order to cover ADL key and generic concepts, our approach is explained through LfP (Language for rapid Prototyping) as ADL offering the possibility to specify the hierarchical behaviour of software components. Then, our contribution goal is to exploit a suitable logic that allows reasoning naturally about software system behaviour, possibly hierarchical and modular, in terms of its basic components and their interactions.

Keywords

Tile Logic, LfP Model, Software Architecture, Hierarchical Composition

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	D. Garlan and B. Schmerl, “Architecture-Driven Modelling and Analysis,” Proceedings of the 11th Australian Workshop on Safety Related Programmable Systems (SCS’06), Vol. 69, 2006, pp.3-17.
[2]	P. Zhang, H. Muccini and B. X. Li, “A Classi?cation and Comparison of Model Checking Software Architecture Techniques,” The Journal of Systems and Software, Vol. 83, No. 5, May 2010, pp. 723-744.
[3]	D. Regep, “LfP: un langage de spécification pour supporter une démarche de développement par prototypage pour les systèmes répartis,” thèse de doctorat, Université de Paris VI, 2003.
[4]	R. Bruni, “Tile logic for Synchronized Rewriting of Concurrent Systems,” PhD. Thesis, Computer Science Department, University of Pisa, Pisa, 1999.
[5]	J. Meseguer, “Conditional Rewriting Logic as a Unified Model of Concurrency,” Journal of Theoretical Computer Science, Vol. 96, No. 1, April 1992, pp. 73-155.
[6]	C. Jerad and K. Barkaoui, “On the Use of Rewriting Logic for Verification of Distributed Software Architecture Description Based LfP,” 16th IEEE International Workshop on Rapid System Prototyping (RSP'05), June 2005, pp. 202-208.
[7]	C. Jerad, K. Barkaoui and G. Touzi, “A. Hierarchical Verification in Maude of LfP Software Architectures,” Lecture Notes in Computer Science, Vol. 4758, 2007, pp. 156-170.
[8]	D. C. Lukham, “Rapide: A language Toolset for Simulation of Distributed System by Partial Ordering of Events,” DIMACS Workshop on Partial Order Methods in Verification (POMIV), 1996, pp. 329-358. http://pavg.stanford.edu/rapide/rapide-pubs.html
[9]	R. J. Allen, “Formal Approach to Software Architecture,” PhD. Thesis, University of Carnegie Mellon, Pittsburgh, May 1997.
[10]	C. Braga and A. Sztajnberg, “Towards a Rewriting Semantics for a Software Architecture Description Language,” Proceedings of the Brazilian Workshop on Formal Methods, Vol. 95, May 2004, pp. 149-168.
[11]	R. Bruni, J. Fiadeiro, I. Lanese, A. Lopes and U. Montanari, “New Insights into the Algebraic Properties of Architectural Connectors,” International Federation for Information Processing, Vol. 155, 2004, pp. 367-380.
[12]	R. Bruni, U. Montanari and U. Sassone, “Observational Congruences for Dynamically Reconfigurable Tile Systems,” Theoretical Computer Science, Vol. 335, No. 2-3, May 2005, pp. 331-372.
[13]	D. Hirsch and U. Montanari, “Consistent Transformations for Software Architecture Styles of Distributed Systems,” Workshop on Distributed Systems, Vol. 28, 1999.
[14]	F. Arbab, R. Bruni, D. Clarke, I. Lanese and U. Montanari, “Tiles for Reo,” Lecture Notes in Computer Science, Vol. 5486, 2009, pp. 37-55
[15]	A. Choutri, F. Belala and K. Barkaoui, “Towards a Tile Based LfP Semantics,” Second International Conference on Research Challenges in Information Science (RCIS 2008), June 2008, pp. 9-16.
[16]	C. Bouanaka, A. Choutri and F. Belala, “On Generating Tile System for Software Architecture: Case of a Collaborative Application Session,” ICSOFT’07, Barcelone, 2007, pp. 123-126.
[17]	F. Gilliers, “Développement par prototypage et Génération de Code à partir de LfP, un langage de modélisation de haut niveau,” thèse de doctorat, Université P. & M. Curie, Paris, 2005.
[18]	R. Bruni, J. Meseguer and U. Montanari, “Tiling Transactions in Rewriting Logic,” Electronic Notes in Theoretical Computer Science, Vol. 71, April 2004, pp. 90-109.
[19]	J. Meseguer and U. Montanari, “Mapping Tile Logic into Rewriting Logic,” Lecture Notes in Computer Science, Vol. 1376, 1998, pp.62-91.
[20]	M. Clavel, F. Duran, E. Eker, S. N. Marti-Oliet, Lincoln, P. J. Meseguer and C. Talcott, “Maude 2.0 Manual,” June 2003. http://maude.cs.uiuc.edu
[21]	S. Eker, J. Meseguer and A. Sridharanarayanan, “The Maude LTL Model Checker and Its Implementation,” Proceedings of the 10th International Conference on Model Checking Software, 2003, pp. 230-234.
[22]	R. Bruni, A. LIuch and U. Montanari, “Hierarchical Design Rewriting with Maude,” Electronic Notes Theore- tical Computer Science, Vol. 238, No. 3, June 2009, pp. 45-62.