He, Lulu
[Author]
;
université Paris-Saclay
[Contributor];
Dague, Philippe
[Contributor];
Ye, Lina
[Contributor]
Formal verification at design stage of diagnosis related properties for discrete event and real-time systems ; Vérification formelle au stade de la conception de propriétés liées au diagnostic des systèmes à événements discrets et temps réel
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Formal verification at design stage of diagnosis related properties for discrete event and real-time systems ; Vérification formelle au stade de la conception de propriétés liées au diagnostic des systèmes à événements discrets et temps réel
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Le diagnostic de pannes est une tâche cruciale et difficile dans le contrôle automatique des systèmes complexes, dont l’efficacité dépend d’une propriété du système appelée diagnosticabilité. La diagnosticabilité décrit la propriété du système permettant de déterminer dès la phase de conception si un défaut donné se produisant en ligne sera identifiable avec certitude sur la base des observations disponibles, ce qui est une alternative aux tests qui ne peuvent que montrer la présence de défaillances sans garantir leur absence. Le problème de diagnosticabilité des systèmes à événements discrets a reçu une attention considérable dans la littérature, mais peu nombreux sont les travaux qui prennent en compte des contraintes de temps explicites lors de cette analyse. Or de telles contraintes sont naturellement présentes dans les systèmes réels et ne peuvent être négligées compte tenu de leur impact sur cette propriété. Nous avons proposé dans notre travail de master une nouvelle approche à base de SMT (Satisfiability Modulo Theories) pour vérifier la diagnosticabilité en temps borné sur les automates temporisés. Afin d’améliorer l’efficacité de notre méthode (le problème est PSPACE-complet), nous en proposons à présent une extension incrémentale fondée sur l’utilisation de sur- et sous-approximations paramétrées dans une généralisation de la méthode CEGAR (raffinement d’abstraction guidé par un contre-exemple). Nous montrons l’amélioration apportée au travers de résultats expérimentaux. Néanmoins, la diagnosticabilité est une propriété assez forte, qui nécessite généralement un nombre élevé de capteurs. Par conséquent, il n’est pas rare que le développement d’un système diagnosticable soit trop coûteux. Afin de garantir dès la conception un certain niveau de sûreté de fonctionnement de manière économique et efficace, nous proposons deux approches. La première consiste à concevoir des systèmes à événements discrets diagnosticables en utilisant des blocs de retard. En effet, que se passe-t-il si un système se révèle comme non ...