Industry is presently investigating the possibility to use commodity multicore processors connected by standard network components in safety critical systems like cars. In this scenario one clearly wants to be able to argue that a passenger on the rear seat trying to hack the car's entertainment system cannot shoot down the electronic chassis control and the engine control, although large portions of the hardware are shared. Any such argument - be it informal, a paper and pencil proof, or formally verified by a CAV system - has to consider the layers of the architecture of the car's computer system; it has to show that each layer provides a simulation between two adjacent computational models in the systems architecture and that these simulated models stay intact for all configurations and input sequences of the entire system. These models turn out to be far from obvious with very subtle and nontrivial modifications compared to classical textbook computer science.
展开▼
