分层块图翻译确定性的机械证明
计算机科学中的逻辑
2018-04-13 v2
摘要
分层块图（HBDs）是包括Simulink在内的嵌入式系统设计工具的核心。存在许多从HBDs到具有形式语义、适于形式验证的语言的翻译。然而，据我们所知，这些翻译均未被证明正确。我们在本文中提出首个机械证明的HBD翻译算法。该算法将HBDs翻译成具有三种基本组合操作（串行、并行和反馈）的项代数。为了捕获产生不同项、实现不同权衡的各种翻译策略，该算法是非确定的。尽管如此，我们证明其语义确定性：对于每个输入HBD，算法可生成的所有可能项在语义上等价。我们应用该结果表明，先前引入的三种Simulink翻译策略如何可形式化为该算法的确定性化，并推导出这些策略产生语义等价的结果（先前工作中遗留的开放问题）。所有结果均在Isabelle定理证明器中形式化并证明。
引用
@article{arxiv.1611.01337,
title = {Mechanically Proving Determinacy of Hierarchical Block Diagram Translations},
author = {Viorel Preoteasa and Iulia Dragomir and Stavros Tripakis},
journal= {arXiv preprint arXiv:1611.01337},
year = {2018}
}