Paper Info
Title
Model Checking Data-Dependent Real-Time Properties of the European Train Control System
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 [1] integrates Communicating Sequential Processes (CSP) [2], Object-Z (OZ) [3], and Duration Calculus (DC) [4] 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) [5] 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.
Year
DOI
Venue
2006
10.1109/FMCAD.2006.21
FMCAD
Keywords
Field
DocType
software system,real-time requirement,data handling,data aspect,duration calculus,infinite data domain,convenient language,real-time safety property,formal language,european train control system,emergency message handling,model checking data-dependent real-time,control flow,three dimensions,embedded systems,communicating sequential processes,real time,software systems,formal languages,compositional semantics,model checking
Model checking,Programming language,Data domain,Computer science,Control flow,Communicating sequential processes,European Train Control System,Theoretical computer science,Real-time computing,Software system,Group method of data handling,Duration calculus
Conference
ISBN
Citations 
PageRank 
0-7695-2707-8
18
0.86
References 
Authors
3
2
Name
Order
Citations
PageRank
Johannes Faber1765.46
Roland Meyer220315.99