Abstract :
The behavior of embedded hardware and software systems is determined by at least three dimensions: control flow, data aspects, and real-time requirements. To specify the different dimensions of a system with the best-suited techniques, the formal language CSP-OZ-DC (Hoenicke and Maier, 2005) integrates communicating sequential processes (CSP) (Hoare, 1985), Object-Z (OZ) (Smith, 2000), and duration calculus (DC) (Zhou and Hansen, 2004) into a declarative formalism equipped with a unified and compositional semantics. In this paper, we provide evidence that CSP-OZ-DC is a convenient language for modeling systems of industrial relevance. To this end, we examine the emergency message handling in the European train control system (ETCS) as a case study with uninterpreted constants and infinite data domains. We automatically verify that our model ensures real-time safety properties, which crucially depend on the system´s data handling. Related work on ETCS case studies focuses on stochastic examinations of the communication reliability (Hermanns et al., 2005; Zimmermann and Hommel, 2005). The components´ data aspects are neglected, though
Keywords :
communicating sequential processes; embedded systems; formal languages; locomotives; program verification; CSP-OZ-DC formal language; European train control system; Object-Z; communicating sequential processes; compositional semantics; data-dependent real-time properties; declarative formalism; duration calculus; embedded systems; emergency message handling; infinite data domains; model checking; model verification; real-time safety properties; unified semantics; uninterpreted constants; Automatic control; Calculus; Communication system control; Control system synthesis; Control systems; Electrical equipment industry; Formal languages; Hardware; Real time systems; Software systems;
