Call for Paper - January 2023 Edition
IJCA solicits original research papers for the January 2023 Edition. Last date of manuscript submission is December 20, 2022. Read More

Model Checking BRS based AADL Specification

International Journal of Computer Applications
© 2012 by IJCA Journal
Volume 52 - Number 21
Year of Publication: 2012
Nadira Benlahrache
Faiza Belala
Taha A. Cherfia

Nadira Benlahrache, Faiza Belala and Taha A Cherfia. Article: Model Checking BRS based AADL Specification. International Journal of Computer Applications 52(21):43-52, August 2012. Full text available. BibTeX

	author = {Nadira Benlahrache and Faiza Belala and Taha A. Cherfia},
	title = {Article: Model Checking BRS based AADL Specification},
	journal = {International Journal of Computer Applications},
	year = {2012},
	volume = {52},
	number = {21},
	pages = {43-52},
	month = {August},
	note = {Full text available}


Although the architecture description language AADL differs from other ADLs by its possibility to describe both hardware and software aspects of a system, it does not provide a formal notation for describing the deployment operation which is crucial in systems where hardware and software components are tightly coupled such as embedded systems. In this paper, we show the relevance of bigraphical reactive systems (BRS) to formalize the deployment operation of AADL architectures. The proposed approach allows, firstly a formal description of the two structures of AADL architectures, namely the platform and the application scenario, and secondly a natural modelization of the installation and the reconfiguration of AADL specification thanks to composition and transformaton operations of BRS. To validate the obtained model, we use a model checker dedicated to BRS.


  • Medvidovic, N. and Taylor, R. N. 2000. A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Tran. on Soft. Eng. 26(1):70-93.
  • Zhang, P. Muccini, H. and Li, B. 2010. A classification and comparison of model checking software architecture techniques. Journal of Syst. Software. doi:10. 1016/j. jss.
  • Parrish, A. Dixon, B. and Cordes, D. 2001. A Conceptual Foundation for Component-Based Software Deployment. Journal of Systems and Software. 57(3): 193-200.
  • SAE. International Avionics Systems Division (ASD). 2004. Avionics Architecture Description Language Standard. Available: http://www. sae. org.
  • SEI. 2004. OSATE: An extensible Source AADL Tool Environment. SEI AADL Team technical Report.
  • Lasnier, G. Zalila, B. Pautet, L. and Hugues, J. 2009. OCARINA: An Environment for AADL Models Analysis and Automatic Code Generation for High Integrity Applications. In Reliable Soft. Tech. '09 LNCS - Ada Europe, France. 237–250.
  • Jensen, O. H. and Milner, R. 2004. Bigraphs and mobiles processes (revised). Technical Report 580, University of Cambridge, ISSN: 1476-2986.
  • Chang, Z. X. M. and Qi, Z. 2007. An Approach based on Bigraphical Reactive Systems to Check Architectural Instance Conforming to its Style. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE'07). 57-66.
  • Perrone, G. and Hildebrandt, T. 2012. A Model Checker for Bigraphs. In proceedings of the 27th ACM Sym. in Applied Computing ACM-SAC'12.
  • Farail, P. Gaufillet, P. Canals, A. Camus, C. L. Sciamma, D. Michel, P. Crégut, X. and Pantel, M. 2006. TOPCASED: An Open Source Development Environment for Embedded Systems. MDD Concepts to Experiments and Illustrations, ISTE Editor.
  • Milner, R. 2008. Bigraphs: a space for interaction. Available on web site: http://www. cl. cam. ac. uk.
  • Conforti, G. Macedonio, D. and Sassone, V. 2005, BiLog: Spatial Logics for Bigraphs. In Proc. of the 32th ICALP'05, LNCS, Springer Verlag editor. 3580. 766-778.
  • Bruni, R. Lafuente, A. L. Montanari,U. and Tuosto, E. 2007. Style-Based Architectural Reconfigurations. Bulletin of the European Association for Theoretical Computer Science, EATCS. 94:161-180.
  • Benlahrache, N. Belala, F. Barkaoui, K. 2011. Description formelle du déploiement d'architectures AADL basée sur les systèmes réactifs bigraphiques (BRS). CAL'2011, 5ème Conférence Francophone sur les Architectures Logicielles, Lille, France. 65-75.
  • Allen, R. Douence R. , and Garlan, D. 1998. Specifying and Analyzing Dynamic Software Architectures. In Proceedings of the 1998 Conf. on Fundamental Approaches to Soft. Eng. Lisbon, Portugal. 21-37. 11-79.
  • Bures, T. , Hnetynka, P. and Plasil, F. 2006. SOFA 2. 0: Balancing Advanced Features in a Hierarchical Component Model. SERA, pp. 40-48.
  • Belguidoum, M. and Dagnat, F. 2007. Dependency Management in Software Component Deployment. Electr. Notes Theor. Comput. Sci. (ENTCS) Vol. 182, pp. 17-32.
  • Liu, Y. D. and Smith, S. F. 2006. A formal framework for component deployment. OOPSLA, pp. 325-344.