Motifs Formels D'Architectures Pour La Surete de Fonctionnement

Ce livre propose des méthodes assistant la modélisation et l'évaluation de l'architecture de sűreté de fonctionnement des systčmes embarqués complexes. Ces méthodes sont basées sur des motifs généraux d'architectures de systčmes correspondant ŕ des éléments de sűreté. Le principe est celui des "patrons de conception" développés en génie logiciel. Ces patrons peuvent ętre formalisés ŕ l'aide de langages formels comme AltaRica. Dans notre cas, les motifs correspondent ŕ des abstractions d'architectures concrčtes et donc requičrent une modélisation plus déclarative. Les propriétés étudiées étant en général dynamiques, nous avons choisi d'utiliser une logique temporelle pour les exprimer. Les motifs sont donc constitués d'une partie en AltaRica et d'une partie de propriétés. Ce type de modélisation mixte possčde plusieurs intéręts, notamment lors de la conception en phase amont d'architectures de systčmes oů il est possible de manipuler ŕ la fois des parties clairement définies d'un systčme et des spécifications. Elle a également pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage.