| Reference : Formalisation de contextes et d'exigences pour la validation formelle de logiciels em... |
| Scientific journals : Article | |||
| Engineering, computing & technology : Computer science | |||
| http://hdl.handle.net/10993/25174 | |||
| Formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqués | |
| French | |
| Dhaussy, Philippe [> >] | |
| Boniol, Frédéric [> >] | |
| Roger, Jean-Charles [> >] | |
| Raji, Amine [> >] | |
Le Traon, Yves  [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)] | |
| Baudry, Beno It [> >] | |
| 2012 | |
| TSI. Technique et science informatiques | |
| Lavoisier | |
| 31 | |
| 6 | |
| 797--825 | |
| Yes | |
| International | |
| [fr] Contextes de preuve ; exigences formelles ; modèles de contexte ; observateurs ; automates temporisés ; vérification | |
| [fr] Un défi bien connu dans le domaine des méthodes formelles est d'améliorer leur intégration dans
les processus de développement industriel. Dans le contexte des systèmes embarqués, l’utilisation des techniques de vérification formelle nécessitent tout d'abord de modéliser le système à valider, puis de formaliser les propriétés devant être satisfaites sur le modèle et enfin de décrire le comportement de l'environnement du modèle. Ce dernier point que nous nommons « contexte de preuve » est souvent négligé. Il peut être, cependant, d'une grande importance afin de réduire la complexité de la preuve. Dans notre contribution, nous cherchons à proposer à l’utilisateur une aide pour la formalisation de ce contexte en lien avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un langage (DSL), nommée CDL (Context Description Language), pour la description des acteurs de l’environnement, basée sur des diagrammes d’activités et de séquence et des patrons de définition des propriétés à vérifier. Les propriétés sont modélisées et reliées à des régions d’exécution spécifiques du contexte. Nous illustrons notre contribution sur un exemple et décrivons des résultats sur plusieurs applications industrielles embarquées. | |
| http://hdl.handle.net/10993/25174 |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
