Reliability of CPS

Nowadays, as traditional control systems are replaced by ever more powerful networks of microprocessors, cyber-physical systems(CPS) are becoming an integral part of modern society. Medical devices and automotive systems are two areas that have greatly benefited from such developments. Correct functioning of such systems is of paramount importance since a malfunction can lead to a serious injury or a loss of life. However, as recent problems with the reliability of advanced automotive control systems demonstrate, while correct functioning of such systems is of paramount importance, it is increasingly difficult to guarantee this.

One way to ensure correctness of a complex cyber-physical system is to thoroughly test and/or verify its correctness. While testing can increase confidence in a component, it can not guarantee correctness. Verification, on the other hand, can guarantee correctness. However, thorough verification, for example, of a car with advanced engine controls and numerous networked microprocessors is simply not feasible. In general, this infeasibility may be due to the inherent intractability of verification of hybrid systems or due to the unavailability of the source level description of a component because of proprietary and other reasons. In addition, even if the component has been verified for correctness, usually this verification is performed on a model of the component which may not be accurate. Furthermore, the run time environment may not satisfy the assumptions that were made in the verification of the component.