CSR: Small: Verifying Simulink-Stateflow models

CSR：小型：验证 Simulink-Stateflow 模型

• 批准号: 1016791
• 负责人: Sayan Mitra
• 金额: $ 50万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1016791&HistoricalAwards=false
• 关键词: CSR; Small; Verifying; Simulink; Stateflow

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.

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