Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Les systèmes cyber-physiques sont des systèmes habituellement complexes et souvent critiques, dans le sens où leur défaillance peut avoir des impacts négatifs significatifs sur des vies humaines. Lors de leur développement, il convient donc de mettre l’accent sur les phases de validation et vérification (V & V) afin de prouver que le système satisfait sa spécification et les exigences de l’utilisateur et que les cas d’erreur pouvant conduire à des accidents ne se produiront pas. Dans la mesure où ils sont souvent très volumineux et complexes, le développement repose habituellement sur des procédés dits de séparation des préoccupations. Cela consiste à modéliser le système de manière hétérogène, avec différents modèles qui doivent ensuite être combinés pour rendre contre du système dans son ensemble. Ces séparations des préoccupations peuvent être de différentes natures : horizontale, ce qui revient à séparer le système de manière structurelle en sous-systèmes ; verticales, ce qui revient à séparer le développement d’une partie du système en plusieurs étapes allant de la spécification abstraite à l’implémentation concrète ; et enfin transversale, ce qui consiste à regrouper ensemble les différents aspects du système qui participent de la même thématique (fonction, performance, sécurité, sûreté…). Usuellement, les différentes parties du système sont modélisées avec des langages métier dédiés tandis que les activités de V & V sont effectuées soit par tests et relectures, soit par l’approche que nous utilisons : les méthodes formelles. Dans tous ces cas, les activités de V & V doivent prendre en compte ces séparations afin de fournir une confiance dans le système complet se basant sur la confiance en ses constituants. En d’autres termes, afin de prouver la conformité du système global, il faut lui définir une sémantique comportementale qui doit prendre en compte les sémantiques ad-hoc des constituants du système. Pour définir cette sémantique, il faut parvenir à regrouper toutes ces sémantiques ...