用于关键系统早期分析的双引擎
计算机科学中的逻辑
2014-08-05 v1
摘要
本文提出了一种基于 Alloy 语言对关键系统进行建模、仿真和属性检查的框架，Alloy 是一种带有内置传递闭包算子的声明式一阶关系逻辑。本文介绍了一种新的双分析引擎，能够同时提供反例和证明。反例通过 SMT 求解器完全自动地发现，其对数值表达式的支持优于现有的 Alloy Analyzer。然而，由于 Alloy 语言是不可判定的，证明并不总能自动找到。我们的引擎提供了一种经济的方法：首先尝试使用基于 SMT 的全自动分析来证明属性，仅在首次尝试失败时才切换到交互式定理证明器。本文还报告了将该框架应用于微软 COM 标准和标记 - 清扫垃圾回收算法的情况。
引用
@article{arxiv.1408.0707,
title = {A Dual-Engine for Early Analysis of Critical Systems},
author = {Aboubakr Achraf El Ghazi and Ulrich Geilmann and Mattias Ulbrich and Mana Taghdiri},
journal= {arXiv preprint arXiv:1408.0707},
year = {2014}
}
备注
Workshop on Dependable Software for Critical Infrastructures (DSCI), Berlin 2011