We apologize for a recent technical issue with our email system, which temporarily affected account activations. Accounts have now been activated. Authors may proceed with paper submissions. PhDFocusTM
CFP last date
20 December 2024
Reseach Article

Model Checking BRS based AADL Specification

by Nadira Benlahrache, Faiza Belala, Taha A. Cherfia
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 52 - Number 21
Year of Publication: 2012
Authors: Nadira Benlahrache, Faiza Belala, Taha A. Cherfia
10.5120/8338-1955

Nadira Benlahrache, Faiza Belala, Taha A. Cherfia . Model Checking BRS based AADL Specification. International Journal of Computer Applications. 52, 21 ( August 2012), 43-52. DOI=10.5120/8338-1955

@article{ 10.5120/8338-1955,
author = { Nadira Benlahrache, Faiza Belala, Taha A. Cherfia },
title = { Model Checking BRS based AADL Specification },
journal = { International Journal of Computer Applications },
issue_date = { August 2012 },
volume = { 52 },
number = { 21 },
month = { August },
year = { 2012 },
issn = { 0975-8887 },
pages = { 43-52 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume52/number21/8338-1955/ },
doi = { 10.5120/8338-1955 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T20:52:53.591479+05:30
%A Nadira Benlahrache
%A Faiza Belala
%A Taha A. Cherfia
%T Model Checking BRS based AADL Specification
%J International Journal of Computer Applications
%@ 0975-8887
%V 52
%N 21
%P 43-52
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

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.

References
  1. 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.
  2. 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.
  3. 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.
  4. SAE. International Avionics Systems Division (ASD). 2004. Avionics Architecture Description Language Standard. Available: http://www. sae. org.
  5. SEI. 2004. OSATE: An extensible Source AADL Tool Environment. SEI AADL Team technical Report.
  6. 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.
  7. Jensen, O. H. and Milner, R. 2004. Bigraphs and mobiles processes (revised). Technical Report 580, University of Cambridge, ISSN: 1476-2986.
  8. 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.
  9. Perrone, G. and Hildebrandt, T. 2012. A Model Checker for Bigraphs. In proceedings of the 27th ACM Sym. in Applied Computing ACM-SAC'12.
  10. 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.
  11. Milner, R. 2008. Bigraphs: a space for interaction. Available on web site: http://www. cl. cam. ac. uk.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. Bures, T. , Hnetynka, P. and Plasil, F. 2006. SOFA 2. 0: Balancing Advanced Features in a Hierarchical Component Model. SERA, pp. 40-48.
  17. Belguidoum, M. and Dagnat, F. 2007. Dependency Management in Software Component Deployment. Electr. Notes Theor. Comput. Sci. (ENTCS) Vol. 182, pp. 17-32.
  18. Liu, Y. D. and Smith, S. F. 2006. A formal framework for component deployment. OOPSLA, pp. 325-344.
Index Terms

Computer Science
Information Sciences

Keywords

Architecture language bigraphs BRS installation reconfiguration