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
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.