Subproject 6: Automotive

In Verisoft's subproject 6 the verification of an automotive system is attempted. The system consists of typical components deployed and run on-board of vehicles: a time-triggered bus system (similar to FlexRay), a time-triggered operating system (similar to OSEKTime). On top of these system components, an automotic emergency call application is realized.

Verification of FlexRay

FlexRay is a standard for a high-end real time bus for automotive applications. It is being developed and pushed forward by an industry consortium consisting of leading automotive manufacturers and suppliers. FlexRay speficies a time-triggered communication bus. The central component of FlexRay is its communication protocol, which provides the following two core features:
  • a message exchange service with deterministic, periodic message transport and
  • a synchronization service that synchronizes the clocks of all nodes, which are connected to the bus.

The FlexRay work package deals with the implementation and verification of FlexRay bus interfaces. It shall be proven that these interface, if connected to the communication bus, comply to the FlexRay communication protocol and thus implements its features.

A gate-level implementation of the interface has already been completed as well as mathemical proofs of its correctness. These proofs are currently being formalized in the theorem prover Isabelle.

Verification of the OSEKtime Operating System with FTCom

The OSEKtime OS is a standard for a time-triggered operating system designed as a run-time environment for highly dependable real-time software in automotive electronic control units. It consists of a real-time preemptive dispatcher and a fault-tolerant communication layer as described. Since one of OSEKtime's main design goals is predictability, scheduling is statically defined at compile time.

FTCom is a fault-tolerant communication layer provided by OSEKtime. It is responsible for the interaction between communication controller hardware and application software. FTCom offers a number of services to the application layer and acts as an interface to the bus controller (in our case the bus interface mentioned eaerlier). The services provided to the applications are:

  • Global message handling allowing the application processes to communicate with each other. This service makes the physical deployment of communication partners transparent, as FTCom handles both local and global inter-process data exchange.
  • Time service and external clock synchronization for the purpose of local clock correction

In the course of the operating system verification OLOS, a newly developed, restricted implementation of the OSEKtime standard was developed. The acronym OLOS stands for "OSEKtime Like Operating System". OLOS does not provide for fault tolerance. However, OLOS has been designed with extensibility in mind, for example, with respect to fault-tolerant variants.

The formal verification of OLOS has been started. This also includes the verificaiton of the communication layer and the device drivers for the bus interfaces.

Verification of an Application

The emergency call application specified by the project partner BMW Group sends out an emergency call if an accident occurs. For this purpose, it reads the state of the crash sensor. If the crash sensor signals an accident, the application reads the vehicle coordinates sent by the navigation system and sends them out by using the mobile phone application. Thus, the emergency call application interoperates with tree other applications (crash sensor, navigation system, and mobile phone), which are distributed over a FlexRay network of ECUs.

The applications were modeled as automata within the CASE tool AutoFocus. For that purpose, a special task model was developed (AFTM, AutoFocus Task Model). Then their ML implementation was integrated with the remaining components of the automotive subproject. AFTM allows to modularize the verification task. For the verification of the application three steps are required:

  • Verification of the task model for the concerete application in AutoFocus (with a model checker)
  • Proof of the correct translation of the task model into the programming language C0 (translation validation)
  • Proof that the execution semantics of AFTM and OSEKtime are equivalent.
AFTM also allows the synthesis of a schedule for the deployment of task to processes that run under OSEKtime.

AutoFocus is a tool for modelling distributed systems. A system consists of a set of components, which are connected via channels, and communicate by exchanging messages. AutoFocus was developed at Technische Universität München, Fakultät für Informatik, Chair IV: Software & Systems Engineering

 
Revision 14 Dec 2006