Abstract

The reduction in size and cost of hardware together with the accelerating innovation and advancement in sensor and computational technologies have opened the door for cyber physical systems into all types of applications. While most early systems involved varying degrees of human involvement, the various success stories are encouraging designers to develop cyber physical systems for autonomous control.
The trustworthiness of a cyber-physical system is essential for it to be qualified for utilization in most real-life deployments. This is especially critical for systems that deal with precious human lives. which can be engaged directly as in biomedical systems or indirectly as in automotive systems. Although use-cases for biomedical and automotive systems are considered, the proposed generalized framework can be used to analyze the safety of various cyber-physical systems.
These safety-critical systems can be investigated using both experimental testing and model-based verification. Accurate models have the potential to permit investigating the system behavior under abnormal scenarios. Also, appropriate modeling can speed-up the development process by evaluating candidate designs at an early stage of the design cycle.
Model-based verification can be conducted using the less-exhaustive simulation testing or the resources-greedy model checking. As a trade-off, statistical model checking bears a feasible approach where statistical guarantees can be examined with a specific level of confidence. This research addresses the problem of utilizing accurate system-level models to analyze and design safety-critical cyber-physical systems.
The behavioral descriptions of cyber physical systems are modelled by constructing equivalent formal models. These system-level models are used to conduct statistical model checking to verify properties written using metric interval temporal logic and to provide statistical guarantees on the system safety. This approach is applied on biomedical and automotive systems to verify their safety with consideration for some distortions resulting from unintentional or intentional sources. The proposed verification approach enlightens the development process by providing feedback that can help elect the designs. Moreover, new robust and safe control techniques are proposed to enhance the safety of a closed-loop glucose controller system. Also, a systematic approach is proposed for safety analysis of cyber physical systems. This approach processes systems described using SysML diagrams and applies a new proposed automatic algorithm to construct equivalent formal models. This research work is a step towards bridging the gap between system-level models and formal models so that analysis can be conducted efficiently to enhance the safety and robustness of cyber-physical systems.