Isabelle 中 Simulink 层次结构框图的类型推断
软件工程
2017-02-28 v2
摘要
Simulink 是嵌入式系统设计的事实工业标准。在先前的工作中，我们在 Isabelle 中开发了针对 Simulink 模型的组合分析框架——反应式系统精算微积分（RCRS），用于检查组件的兼容性和可替换性。然而，该项工作未考虑标准类型检查。本文提出了一种使用 Isabelle 定理证明器对层次结构框图进行类型推断的方法。Simulink 图被转换为 Isabelle 理论。随后利用 Isabelle 强大的类型推断机制，基于基本块的类型推断该图的类型。目标之一是尽可能形式化地处理更多的图。特别是，我们希望能够处理甚至可能存在类型歧义的图，前提是它们被 Simulink 接受。该方法在我们的工具集中得以实现，该工具集将 Simulink 图转换为 Isabelle 理论并进行简化。我们在多个案例研究中评估了我们的技术，最引人注目的是由 Toyota 提供的汽车燃油控制系统基准。
引用
@article{arxiv.1612.05494,
title = {Type Inference of Simulink Hierarchical Block Diagrams in Isabelle},
author = {Viorel Preoteasa and Iulia Dragomir and Stavros Tripakis},
journal= {arXiv preprint arXiv:1612.05494},
year = {2017}
}