« zurück

Automated Validation and Verification of Railway Specific Components and Systems

Today’s electronic systems become more and more complex regarding their size and functionality. They are applied in many areas of our personal lives, for example, cellular phones or entertainment electronics. A modern life without them is hard to imagine. Failures of these devices would usually result in minor problems for the users. But complex electronic systems are also used in safety-critical areas like medical equipment, avionics and electronic railway systems. Especially in these sectors the demand for safety is exceptionally high, because human life might depend on the faultless functionality of such devices. This thesis deals with components and systems which are applied in the railway domain. Here, railway domain means that tram and train control systems are considered. One of the basic building blocks of railway control systems is the Counting Head (CH). It is used to determine whether a specified Track Vacancy Detection Section (TVDS) is clear or occupied. Several TVDSs are monitored by so-called electronic interlocking or control systems. Besides the correct function of these systems, the correct function of CHs is crucial. If the CHs fail to work properly, a TVDS would either be falsely indicated as occupied – resulting in a deterioration of availability and reliability – or falsely indicated as clear – possibly introducing a safety hazard. Additionally, the control system which controls the TVDSs and monitors the CHs has to work correctly as well. Otherwise, two trains, for example, might enter two crossing track sections resulting in a critical situation.
Up to this day components and systems in railway applications are often designed and tested in a conventional way, that is, they are simulated with a manually created test bench. Simulation and testing are broadly accepted in industrial environments and have the advantage that designers have a considerable expertise with this kind of work. Nevertheless, simulation and testing are very cost-intensive and time-consuming. For large and complex designs, it is mostly not practicable to reach complete test coverage and important corner cases might be missed. In order to ensure a complete verification there are efforts to introduce formal methods into the railway domain. In contrast to testing and simulation, formal verification means to prove the correctness of these components and systems. Thus, a formal verification flow for components and systems of the railway domain is proposed here.
To verify a system, formal models of the system and its components are needed. Here, these models are implemented using SystemC, a powerful system description language. Then, the system can be proven to respect particular safety-critical aspects. For the tram control system, as presented, such a safety-critical aspect is verified by defining a set of safe system states and proving that the system is always within this set of states. These proofs are accomplished by Bounded Model Checking (BMC), a special form of Model Checking also called Property Checking. Using this strategy, complex systems can be proven to function correctly with respect to safety-critical aspects. But before the system can be considered as completely verified, subsystems and components of the system need to be proven to be correct as well. Thus, formal verification is carried out using the corresponding SystemC models. The formal verification basically consists of two steps: First, a set of properties is created and proven to hold for the component. Second, the set is proven to be functional complete. In this way, single components of a system are completely proven to be correct according to their specification. Note, in previous verification flows the completeness of sets of properties was assured manually, that is, a verification engineer checked the set of properties and decided whether the set was complete or not. Here, the completeness is proven automatically.