ITR/SY: Formal Design and Analysis of Hybrid Systems

嵌入式系统，如汽车、医疗和航空电子系统中的控制器，由一系列相互作用的软件模块组成，这些模块对模拟环境做出反应并进行控制。控制理论等工程学科专注于连续动态，并为设计鲁棒控制律以确保动态系统的最佳性能提供基础。软件工程等计算学科专注于离散程序，并提供实现复杂控制和分析工具的结构化方法，以验证分布式软件。对于具有多种操作模式的联网嵌入式设备，离散和连续方面的复杂性的组合导致尚未很好理解的基本问题，这使得可靠的嵌入式系统的编程成为一项特别具有挑战性的任务。 设计嵌入式设备的系统方法需要结合控制理论和现代软件工程的工具，而新兴的混合系统理论--具有紧密集成的离散和连续动态的系统，有可能提供基础。尽管混合动力系统作为一个模型的巨大吸引力，国家的最先进的分析和设计技术的混合动力系统的适用性已被限制在小尺寸的例子，由于复杂性。本ITR研究旨在开发自动抽象和层次分解的基础和工具，作为简化和可扩展性的一种手段。 为了促进嵌入式软件的高层次设计，建模概念，如层次结构，模块化，重用，组合性和面向对象，探索开发层次混合系统的理论与伴随的组合演算的细化。这将是行为接口和不同抽象级别组件描述的基础。 为了严格指定和评估设计方案和正确性要求，自动化技术，如模型检查是非常有效的。为了应用这些技术的混合系统的形式化分析，本研究正在开发自动化的计划，用于构建混合模型的抽象。正在追求的技术方向包括利用层次结构的模型检查算法，使用谓词抽象提取有限状态近似的算法，反例引导的抽象细化，基于属性保持的连续微分方程的互模拟减少，以及假设保证推理。这项研究的结果被集成在软件工具的建模和分析的混合动力系统。开发嵌入式系统的安全性和可靠性有更高的保证的技术的好处进行了评估，在多个，自主的，移动的机器人的实验测试平台。

Embedded systems, such as controllers in automotive, medical, and avionic systems, consist of a collection of interacting software modules reacting to and controlling an analog environment. Engineering disciplines such as control theory focus on continuous dynamics, and offer foundations for designing robust control laws for ensuring optimal performance of dynamical systems. Computing disciplines such as software engineering focus on discrete programs, and offer structured ways of implementing complex control and analysis tools for validating distributed software. For networked embedded devices with multiple modes of operation, the combination of the complexity in both discrete and continuous aspects leads to fundamental problems that are not yet well understood, and this makes the programming of reliable embedded systems a particularly challenging task. A systematic approach to designing embedded devices requires combining tools from control theory and modern software engineering, and the emerging theory of hybrid systems---systems with tightly integrated discrete and continuous dynamics, has the potential to provide the foundation. Despite the great appeal of hybrid systems as a model, the applicability of the state-of-the-art analysis and design techniques for hybrid systems has been limited to examples of small size due to complexity. This ITR research aims to develop foundations and tools for automatic abstraction and hierarchical decomposition as a means of simplification and scalability. To facilitate high-level design of embedded software, modeling concepts such as hierarchy, modularity, reuse, compositionality, and object-orientation, are explored to develop a theory of hierarchical hybrid systems with an accompanying a compositional calculus of refinement. This will be the basis for behavioral interfaces and descriptions of components at different levels of abstractions. For rigorously specifying and evaluating design alternatives and correctness requirements, automated techniques such as model checking are very effective. To apply these techniques for formal analysis of hybrid systems, this research is developing automated schemes for constructing abstractions of hybrid models. The technical directions being pursued include model checking algorithms that exploit hierarchy, algorithms for extracting finite-state approximations using predicate abstraction, counter-example guided refinement of abstractions, property-preserving bisimulation-based reductions of continuous differential equations, and assume-guarantee reasoning. The results of this research are being integrated in software tools for modeling and analysis of hybrid systems. The benefits of the techniques for developing embedded systems with higher assurance for safety and reliability are evaluated in an experimental testbed of multiple, autonomous, mobile robots.