Verification of Cyber-Physical Systems: Exploiting Uncertainty for Scalability

Samenvatting

Networked industrial automation systems, self-driving vehicles, smart energy grids, the Internet of things - we see a proliferation of cyber-physical systems: discrete computer control over continuous physical processes. Many such systems are safety-, performance-, or business-critical. Confidence in their correct operation is required. By proving the conformance of a mathematical model of a system design to a specification, formal verification can provide this confidence. Its applicability however is limited by lacking scalability to large, real-world problems.

I propose to significantly improve the scalability of formal verification methods for critical cyber-physical systems by embracing uncertainty in behavioural models as a natural and desirable aspect and designing verification approaches that exploit the presence of stochastic behaviour.

I focus on models that combine both unquantified and quantified uncertainty. The former represents the absence of any information about which event will occur when (nondeterminism; arising e.g. from the abstract treatment of user inputs). The latter is stochastic behaviour, so the likelihoods of events and their timing are known (e.g. in randomised algorithms). One such model for cyber-physical systems is stochastic hybrid automata, for which I co-developed a high-level modelling framework and a prototypical model checker for safety verification. Yet the underlying approach treats quantified uncertainty as a complication on top of the verification problem for the purely nondeterministic case. It is consequently less scalable despite working with more information.

New techniques that I will develop in this project will exploit this information to guide, restrict and inform the model checking process to achieve superior scalability. They will be implemented as part of a comprehensive, publicly available toolset for quantitative verification. The improvements will be validated on case studies stemming from my own research as well as from cooperations with local and international academic partners.

Kenmerken

Projectnummer

639.021.754

Hoofdaanvrager

Dr. ing. A. Hartmanns

Verbonden aan

Universiteit Twente, Faculteit der Elektrotechniek, Wiskunde en Informatica (EWI), Formal Methods and Tools

Looptijd

01/10/2017 tot 30/09/2020