SHF: Small: Verifying Open Concurrent Real Time Systems

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

The widespread prevalence of embedded devices, and networked collections of them, makes ensuring their reliability a social imperative. However, formal verification of such embedded systems is challenging as they are concurrent ``hybrid'' systems, i.e., coupled digital programs and physical entities that interact with an analog environment while meeting real-time constraints. Lured by the importance and scientific depth of the problem, the analysis of such hybrid systems for correctness has received widespread attention in the last couple of decades. Considerable progress has been made in defining languages and models for designing such systems, understanding the theoretical bounds to automated verification of such systems, and developing tools to simulate and verify formal hybrid models. However, key challenges remain. Current state of the art in formal methods allows for the automated analysis of single, closed hybrid systems with simple continuous dynamics. This is in contrast to the fact that, in practice, hybrid systems tend to have complex continuous dynamics, and usually consist of multiple modules interacting concurrently. This work addresses these challenges so as to enable the automated analysis of systems that are open, concurrent, and hybrid. Specifically, the following research tasks will be carried out: (a) Develop techniques to tightly approximate hybrid systems with complex continuous dynamics by hybrid systems with simple dynamics; (b) Develop decision procedures for the composition of hybrid systems; (c) Develop assume-guarantee reasoning for hybrid systems in the presence of approximate abstractions; (d) Apply the proposed methods to analyze software and algorithms deployed in HoTDeC, an environment for distributed control of hovercrafts.