Motifs formels d'architectures de systèmes pour la sûreté de fonctionnement

This thesis aimed at providing methods to assist modelling and assessing qualitatively embedded complex systems safety architectures. These architectures are often based on generic systems architectures models corresponding to safety mechanisms such as redundancies, detections, etc. While taking as a starting point the principles of the design pattern approach used in the software community, we proposed a modeling of these mechanisms and attributes allowing their re-use during safety assessments. These analyses require to reason on the behavior of systems in the presence of failures which can be modelled using formal languages like AltaRica. In our case, patterns are corresponding to concrete architectures' abstractions and so require a more declarative modelling, using properties. Those properties being generally dynamic, we chose a temporal logic to model them. Safety patterns are therefore made of an AltaRica part and a property part. We believe this kind of mixed modelling to be of great interest, especially in the preliminary system architecture design phase where it is necessary to deal with detailed parts of systems as well as specifications. It should also ease the allocation of requirements and prototyping. A notation mixing operational and declarative views has been defined.Cette thèse propose des méthodes assistant la modélisation et l'évaluation qualitative de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces architectures sont souvent construites à partir de motifs généraux d'architectures de systèmes correspondant à des mécanismes de sûreté récurrents comme des redondances, des détections, etc. En s'inspirant des principes des "patrons de conception" développés en génie logiciel, nous avons proposé une modélisation de ces mécanismes et des attributs permettant leur réutilisation lors des analyses de sûreté de fonctionnement. Ces analyses nécessitent de raisonner sur le comportement des systèmes en présence de pannes qui peut être modélisé à 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 AltaRica et d'une partie 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 d'un système conçues de manière détaillée et des spécifications. Elle a également pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage. Nous avons donc défini une notation mixant ces aspects opérationnels et déclaratifs