Séminaires
Séminaire du 14 Octobre 2005
Lieu
Programme
14h00-15h00: Thomas Vergnaud (ENST) : « AADL, un langage pour la modélisation et la génération automatique d'applications »
Abstract: AADL (Architecture Analysis & Design Language) fait partie de la famille des langages de description d'architecture. Il permet la description précise et concrète d'architectures pour les systèmes embarqués temps-réel. Pour cela, AADL définit un ensemble de composants à la sémantique bien définie, permettant de modéliser à la fois les aspects logiciels et matériels d'une architecture. AADL permet d'exprimer les différentes contraintes inhérentes à ces systèmes. L'approche très concrète d'AADL permet de l'utiliser comme langage fédérateur pour la description de systèmes. L'architecture décrite peut être analysée en terme de performances et de respect des contraintes. AADL peut ainsi servir de représentation intermédiaire entre des modélisations formelles plus abstraites et la réalisation de l'application en elle-même. Le passage d'une description AADL à la réalisation concrète d'une application exécutable peut se faire de plusieurs façons, selon les objectifs visés pour l'utilisation d'AADL (simple information de déploiement ou description complète des composants applicatifs). Nous exposons ici nos travaux autour d'AADL, focalisés sur la génération automatique d'applications réparties à partir de leur description en AADL. Nous présentons aussi la suite d'outils Ocarina, qui sert de support à nos travaux de génération.
15h00-15h30 : Sami Evangelista (CNAM) : « Model Checking High Level Petri Net Specifications with Helena »
Abstract: this talk presents the high level Petri nets analyzer Helena. Helena can be used for the on-the-fly verification of state properties, i.e., properties that must hold in all the reachable states of the system, and deadlock freeness. Some features of Helena make it particularly efficient in terms of memory and states management. The Delta-markings method provides very good compression ratios and gives remarkable results when dealing with large state vectors of programs. Structural abstractions techniques, such as transitions agglomerations or the stubborn set method, are used to tackle the state explosion problem. Benchmarks are presented which compare our tool to the well known model checker Maria. Helena is developed in portable Ada and is freely available under the conditions of the GNU General Public License. It can be downloaded at the following address : http://helena.cnam.fr.