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.