Validation of Railway Security Automatisms Based on Petri Networks
Marc Antoni · 2014
This chapter shows that it is indeed possible to apply a formal validation method to industrial automatisms. It focuses on the case of railway automatisms. The method is based on several design actions: taking the specific railway context to be highly important, identifying security properties and operating postulates; making a distinction between the functional software and the basic software; specifying the functions in the form of automata written in AEFD language (Deterministic Finite Automaton). This language makes it possible to write Petri networks and interpret in a deterministic way which is accessible to those involved in signaling. The application of formal methods to signal boxes requires that we render the safety properties and the operation postulates totally explicit. Therefore, it is necessary to take the railway context on board, to observe and formalize the safety and the logical and physical properties of its critical computerized systems.