LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Pi, Lei (2010)
Languages: English
Types: Article
Subjects: Langages de description d'achitecture, AADL Transformation de modèle, Spécification formelle, Model-checking, Méta-modélisation, 000
L'évolution de la complexité des systèmes embarqués critiques conduit actuellement à exploiter d'une part des langages de modélisation les plus proches possible des spécifications du métier du concepteur, et d'autre part des outils de vérification de modèle (model checker) permettant d'assurer la correction du système par rapport à des exigences de sûreté, de respect de contraintes temps-réel. C'est dans ce contexte qu'a été initié notamment le projet TOPCASED (http ://www.topcased.org) visant à proposer un atelier de développement de systèmes critiques temps-réel basé sur la vérification formelle et les langages dédiés. Les méthodes et outils issus de ces travaux visent une intégration des activités de vérification formelle au sein du processus et de la plate-forme de développement. AADL (the SAE Architecture Analysis and Design Language) est un langage de description d'architecture qui permet de décrire autant les aspects matériels que les composants logiciels d'un système. Pour factoriser les transformations entre les langages de modélisation AADL et les dialectes des outils de vérification, le langage intermédiaire FIACRE (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués) a été développé. Il permet de représenter les aspects comportementaux et temporisés de systèmes, en particulier de systèmes embarqués et de systèmes distribués, pour leur vérification ou simulation. Dans ce contexte, j'ai étudié la sémantique de noyaux du modèle d'exécution d'AADL ainsi que leur expression dans différents formalismes, comme TASM, BIP, ACSR et FIACRE. Ils ont fait apparaître le besoin d'unifier ces formalismes. J'ai travaillé sur une nouvelle définition de la sémantique du langage FIACRE et proposé d'enrichir FIACRE par un opérateur de suspension/reprise et un mécanisme d'allocation de ressource dont nous avons illustré l'utilité sur différents exemples. Cependant, la richesse d'expressivité induite n'autorisait plus l'utilisation des RdPT pour la vérification des descriptions FIACRE ainsi étendues. Nous avons alors proposé une traduction du langage FIACRE étendu vers une classe de RdPT nouvellement introduite dans l'environnement Tina : les réseaux de Petri temporels à chronomètres. The evolution of the complexity of critical embedded systems currently leads to use on the one hand modeling languages closest to the specifications of the designer’s job, and on the other hand verification tools (model checker) to ensure the correction of the system with respect to the correctness requirements and the real-time constraints. It is in this context that the project TOPCASED has been launched to propose a framework to develop critical realtime systems based on formal verification and dedicated languages. The methods and tools from this work are an integration of formal verification in the process and platform development. AADL (the SAE Architecture Analysis and Design Language) est un langage de description d’architecture qui permet de décrire autant les aspects matériels que les composants logiciels d’un système. In order to make easer the connection of model checkers to those languages, the pivot FIACRE language (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués) has been developed. It is powerful enough to support the expression of the semantics of real time. In this context, I studied the semantic of the AADL execution model and its expression in different formalisms, like TASM, BIP, ACSR and FIACRE. They revealed the need to unify these formalisms. I worked on a new definition of the semantics of the language FIACRE. Then I propose to enrich FIACRE by a suspend/resume operator and a mechanism for resource allocation of which usefullness is illustrated on several examples. However, the induced expressive power no longer permits the use of TPN for the verification of extended FIACRE models. Thus, I propose a translation of the extended FIACRE language into a class of TPN newly introduced in the environment Tina: Petri nets with stopwatches.

Share - Bookmark

Cite this article