 |
 |
Journal articles
Towards a verified transformation from AADL to the formal component-based language FIACRE
Abstract : During the last decade, aadl is an emerging architecture description languages addressing the modeling of embedded systems. Several research projects have shown that aadl concepts are well suited to the design of embedded systems. Moreover, aadl has a precise execution model which has proved to be one key feature for effective early analysis. In this paper, we are concerned with the foundational aspects of the verification support for aadl. More precisely, we propose a verification toolchain for aadl models through its transformation to the Fiacre language which is the pivot verification language of the TOPCASED project: high level models can be transformed to Fiacre models and then model-checked. Then, we investigate how to prove the correctness of the transformation from AADL into Fiacre and present related elementary ingredients: the semantics of aadl and Fiacre subsets expressed in a common framework, namely timed transition systems. We also briefly discuss experimental validation of the work.
https://hal.archives-ouvertes.fr/hal-01278902
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Thursday, February 25, 2016 - 10:14:23 AM
Last modification on : Thursday, June 11, 2020 - 4:49:42 AM
Long-term archiving on: : Thursday, May 26, 2016 - 11:06:00 AM
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Thursday, February 25, 2016 - 10:14:23 AM
Last modification on : Thursday, June 11, 2020 - 4:49:42 AM
Long-term archiving on: : Thursday, May 26, 2016 - 11:06:00 AM
File
Bodeveix_14914.pdf
Files produced by the author(s)