Engineering Software for Resilient Cyber-Physical Systems

Designing, implementing, and verifying resilient cyber-physical systems is challenging. Resilience is the ability to provide the required capability when facing adversity. Resilient cyber-physical systems should avoid, withstand, recover from, and evolve and adapt to cope with adversity stemming from computation, networking, or physical environment. From the engineering point of view, the usefulness of such systems is hindered by their lack of ability to adapt and overcome unknown stimuli, ever-changing and conflicting objectives, and deprecated internal components. Software as a tool for self-management is a key instrument for dealing with uncertainty. Yet, engineering software for resilient cyber-physical systems is hard since the effects of operating under the unknown might emerge during the execution, requesting decision-making at runtime rather than design time. Decision-making at runtime should guarantee the satisfaction of system goals, work efficiently to be effectively used in practice, and guarantee the expected quality.With this in mind, this thesis contributes towards the engineering of software for resilient cyber-physical systems by (i) combining control theory and artificial intelligence for efficient adaptation, (ii) using formal methods for ensuring correctness of control-theoretic software adaptation, and (iii) promoting a language for scenario-based testing autonomous systems. We found that the hybrid approach, combining control theory and artificial intelligence, improves the efficiency of the adaptation mechanism. The results shed light on the interplay between control theory and artificial intelligence as fundaments for engineering resilient cyber-physical systems. Yet, incorporating machine learning and control theory introduces non-deterministic autonomic behavior, posing a challenge for the assurance provision for such tools. On the one hand, we found that the use of formal methods helps to build confidence in software-based controllers. On the other hand, large and complex systems place barriers to the usage of formal methods. Thus, we explore the use of testing and specifically scenario-based testing for validating large and complex cyber-physical systems that are required to operate in complex and unpredictable environments, like autonomous vehicles. In a nutshell, this thesis argues in favor of introducing control theory and artificial intelligence in designing and implementing software-based controllers. Also, we exploit formal methods and testing as instruments for verifying and validating cyber-physical systems