Motifs Formels D'Architectures Pour La Surete de Fonctionnement

Ce livre propose des mthodes assistant la modlisation et l'valuation de l'architecture de sret de fonctionnement des systmes embarqus complexes. Ces mthodes sont bases sur des motifs gnraux d'architectures de systmes correspondant des lments de sret. Le principe est celui des "patrons de conception" dvelopps en gnie logiciel. Ces patrons peuvent tre formaliss l'aide de langages formels comme AltaRica. Dans notre cas, les motifs correspondent des abstractions d'architectures concrtes et donc requirent une modlisation plus dclarative. Les proprits tudies tant en gnral dynamiques, nous avons choisi d'utiliser une logique temporelle pour les exprimer. Les motifs sont donc constitus d'une partie en AltaRica et d'une partie de proprits. Ce type de modlisation mixte possde plusieurs intrts, notamment lors de la conception en phase amont d'architectures de systmes o il est possible de manipuler la fois des parties clairement dfinies d'un systme et des spcifications. Elle a galement pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage.