Verification of Real-Time Systems: Application to the Transportation Domain

The need of conceiving reliable real-time systems is crucial for the software engineering. This paper is dedicated to the specification and the verification of land transportation systems taken as an application domain. We present a case study in the area of transportation. The system consists of several automated vehicles called CyCab, that have to communicate with a station. The components are modeled with timed automata and some properties are expressed in the timed logic TCTL to be checked by the model checking tool Kronos. These systems, which are both distributed and embedded, require to express non functional-properties, for example a response time constrained.