PhD Oral Exam - Abdel-Latif Alshalalfah, Electrical and Computer Engineering

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

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 these safety-critical systems can be investigated using both experimental testing and model-based verification, accurate models have the potential to permit risk-free mimicking of the system behavior even in the most extreme 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.

In this work, 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 provide statistical guarantees on the system safety. This approach is applied on biomedical and automotive systems to verify their safety under faults and security attacks. The proposed verification approach enlightens the development process by providing feedback that can help elect the designs. In this work, new robust and safe control techniques are proposed to enhance the safety of a closed-loop glucose controller system. Also, in this research 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.