CSR: Small: Verifying Simulink-Stateflow models

绝大多数商用嵌入式系统都是使用MathWork的Simulink和Stateflow等基于模拟的工具进行设计的。虽然模拟在计算上是高效的，但它们并不完整-它们不能天真地用于设计具有可证明保证的系统。该项目旨在建立工具和技术来验证这些模型。为此，该项目克服了两个关键的技术障碍。首先，众所周知，Simulink-Stateflow(SLSF)模型没有任何明确的含义。构建块的数学描述可以不同于数值生成的模拟行为。通过用(可能是概率的)混合自动机定义SLSF模型的语义来解决这个问题。其次，可以通过现有技术自动验证的Simulink模型类(转换为混合自动机)具有相当的限制性。在这个项目中，第二个问题是通过将SLSF模型抽象为具有简单动力学的混合自动机，对抽象模型进行模型检查，然后根据模型检查器生成的反例来提炼抽象。这种反例制导的抽象求精框架提供了半决策过程来自动分析Simulink-Stateflow模型。该项目开发的软件工具将SLSF模型转换为概率混合自动机，通过抽象、模型检查和求精对形式自动机模型进行分析，然后将有效的反例转换回Simulink，为用户提供诊断信息。此外，该项目基于现有混合系统文献中的示例并借鉴工业应用，建立了基准SLSF模型及其对应的混合自动机模型的存储库。该储存库将被公开传播，并将用于评估我们的工具。将开发一门关于混合系统验证的新课程，向伊利诺伊州工程专业的本科生和研究生介绍嵌入式系统设计中形式化方法的使用。本文概述的研究任务的成功完成可能会更广泛地影响出现在自动驾驶汽车和混合模拟-数字电路等应用领域的概率混合系统的设计和验证。

The vast majority of commercial embedded systems are designed with simulation-based tools such as MathWork's Simulink and Stateflow. While simulations are computationally efficient, they are not complete---they cannot be naively used to design systems with provable guarantees. This project aims to build tools and techniques to verify such models. To this end, the project overcomes two key technical hurdles. First, it has been well known that Simulink-Stateflow (SLSF) models do not have any well-defined meaning. The mathematical description of a building block can be different from the simulated behavior that is generated numerically. This problem is addressed by defining semantics of SLSF models in terms of (possibly probabilistic) hybrid automata. Secondly, the class of Simulink models (translated to hybrid automata) that can be verified automatically by currently available techniques is rather restrictive. This second problem is addressed in this project by abstracting SLSF models into hybrid automata with simple dynamics, model checking the abstract models, and then refining the abstractions based on counterexamples generated by the model checker. Such a counterexample guided abstraction refinement framework provides semi-decision procedures to automatically analyze Simulink-Stateflow models. The developed software tools developed in this project translate SLSF models into probabilistic hybrid automata, analyze the formal automata model by abstracting, model checking, and refining, and then translate valid counterexamples back into Simulink to provide the user diagnostic information. Furthermore, the project builds a repository of benchmark SLSF models and their corresponding hybrid automaton models, based on examples from existing hybrid systems literature and drawing on industrial applications. The repository will be publicly disseminated and will be used to evaluate our tool. A new course will be developed on the verification of hybrid systems that introduces undergraduate and graduate students in engineering at Illinois to the use of formal methods in embedded system design. Successful completion of the research tasks outlined here is likely to more broadly influence the design and verification of probabilistic hybrid systems that arise in application domains such as autonomous vehicles and mixed analog-digital circuits.