SHF: Small: Verifying Open Concurrent Real Time Systems

嵌入式设备的广泛流行，以及它们的网络化集合，使得确保它们的可靠性成为社会的当务之急。然而，这种嵌入式系统的正式验证是具有挑战性的，因为它们是并发的“混合”系统，即耦合的数字程序和物理实体与模拟环境交互，同时满足实时约束。在这个问题的重要性和科学深度的吸引下，对这种混合系统的正确性分析在过去的几十年里受到了广泛的关注。在定义用于设计此类系统的语言和模型、理解此类系统自动验证的理论界限以及开发用于模拟和验证正式混合模型的工具方面，已经取得了相当大的进展。然而，主要挑战依然存在。目前的形式化方法允许对具有简单连续动力学的单个封闭混合系统进行自动化分析。这与实际情况相反，混合系统往往具有复杂的连续动态，并且通常由多个并发交互的模块组成。这项工作解决了这些挑战，以便能够对开放、并发和混合的系统进行自动化分析。具体来说，将进行下列研究任务：(a)发展技术，用简单动力学的混合系统紧密逼近具有复杂连续动力学的混合系统；(b)制订混合系统组成的决策程序；(c)为存在近似抽象的混合系统发展假设-保证推理；(d)将提出的方法应用于气垫船分布式控制环境HoTDeC中部署的软件和算法的分析。

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.