«

»

Contribution à la formalisation de contextes et déxigences pour la validation formelle de logiciels embarqués

by Philippe Dhaussy, Pierre-Yves Pillain, Stephen Creff, Amine Raji, Yves Le Traon, Benoit Baudry “
Abstract:
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é CDL (Context Description Language), pour la description des acteurs de l’environnement, basé 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.
Reference:
Contribution à la formalisation de contextes et déxigences pour la validation formelle de logiciels embarqués (Philippe Dhaussy, Pierre-Yves Pillain, Stephen Creff, Amine Raji, Yves Le Traon, Benoit Baudry “), In Approches Formelles dans l’Assistance de Développement Logiciel, 2010.
Bibtex Entry:
@inproceedings{Dhaussy2010,
	Abstract = {  
  Un d{'e}fi bien connu dans le domaine des m{'e}thodes formelles est d'am{'e}liorer leur int{'e}gration dans les processus de d{'e}veloppement industriel. Dans le contexte des syst{`e}mes embarqu{'e}s, l'utilisation des techniques de v{'e}rification formelle n{'e}cessitent tout d'abord de mod{'e}liser le syst{`e}me {`a} valider, puis de formaliser les propri{'e}t{'e}s devant {"e}tre satisfaites sur le mod{`e}le et enfin de d{'e}crire le comportement de l'environnement du mod{`e}le. Ce dernier point que nous nommons « contexte de preuve » est souvent n{'e}glig{'e}. Il peut {^e}tre, cependant, d'une grande importance afin de r{'e}duire la complexit{'e} de la preuve. Dans notre contribution, nous cherchons {`a} proposer {`a} l'utilisateur une aide pour la formalisation de ce contexte en lien avec la formalisation des propri{'e}t{'e}s. Dans ce but, nous proposons et exp{'e}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{'e}s et de s{'e}quence et des patrons de d{'e}finition des propri{'e}t{'e}s {`a} v{'e}rifier. Les propri{'e}t{'e}s sont mod{'e}lis{'e}es et reli{'e}es {`a} des r{'e}gions d'ex{'e}cution sp{'e}cifiques du contexte. Nous illustrons notre contribution sur un exemple et d{'e}crivons des r{'e}sultats sur plusieurs applications industrielles embarqu{'e}es.
 },
	Address = {Poitiers, France},
	Author = {Philippe Dhaussy and Pierre-Yves Pillain and Stephen Creff and Amine Raji and Yves Le Traon and Benoit Baudry "},
	Booktitle = {Approches Formelles dans l'Assistance de D{'e}veloppement Logiciel},
	Month = {June},
	Title = {Contribution {`a} la formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqu{'e}s},
	Url = {http://www.irisa.fr/triskell/publis/2010/Dhaussy2010.pdf},
	X-International-Audience = {no},
	X-Language = {FR},
	X-Proceedings = {yes},
	Year = {2010},
	x-abbrv = {AFADL},
	keywords={MDE,analysis},}