De Almeida Pereira, Dalay Israel
[VerfasserIn]
;
Centrale Lille Institut
[MitwirkendeR];
Collart-Dutilleul, Simon
[MitwirkendeR]
Analyse et spécification formelle des systèmes d’enclenchement ferroviaire basés sur les relais ; Analysis and formal specification of relay-based railway interlocking systems
Titel:
Analyse et spécification formelle des systèmes d’enclenchement ferroviaire basés sur les relais ; Analysis and formal specification of relay-based railway interlocking systems
Beteiligte:
De Almeida Pereira, Dalay Israel
[VerfasserIn]
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Les Systèmes d'Enclenchement Ferroviaire (SEF) basés sur des relais sont des systèmes critiques, ils doivent être spécifiés et leur sécurité doit être prouvée afin de garantir l'absence de dangers lors de leurs exécutions. Toutefois, il s'agit d'une tâche difficile, car les SEF à relais ne sont généralement modélisés que de manière structurelle, de sorte que leur analyse comportementale est effectuée manuellement sur la base des connaissances des experts sur le système. Cependant, l'existence d'une description formelle du comportement des SEF est impérative pour pouvoir effectuer des preuves de sécurité. En outre, comme les SEF informatisés ont tendance à être moins chers, plus faciles à entretenir et à faire évoluer, le secteur ferroviaire a intérêt à ce qu'il existe une méthodologie pour transformer des SEF à relais existants en SEF informatisés.Les méthodologies formelles de spécification sont fondées sur des bases mathématiques solides qui permettent de prouver la sécurité des systèmes. En outre, de nombreux langages de spécification formelle prennent en charge non seulement la vérification, mais aussi la mise en œuvre de ces systèmes par un processus de développement formalisé. Ainsi, les méthodes formelles peuvent être la clé pour prouver la sécurité des SEF et les mettre en œuvre en utilisant des technologies informatiques.Cette thèse aborde deux propositions principales. Premièrement, elle présente une analyse des informations des diagrammes à relais et de la formalisation de la structure et du comportement des SEF basés sur des expressions mathématiques afin de créer un certain niveau de formalisation des systèmes. Le modèle résultant peut être étendu et adapté afin de se conformer à différents contextes ferroviaires et il peut aussi être utilisé afin de soutenir la spécification de ces systèmes dans différents langages de spécification formels. Ensuite, cette thèse présente comment le modèle formel des SEF peut être adapté afin de spécifier formellement ces systèmes selon la méthode B, un langage de ...