通过变换验证反应式系统的时序性质
计算机科学中的逻辑
2015-12-15 v1 编程语言
摘要
我们展示程序变换技术如何用于验证反应式系统的安全性和活性性质。特别地，我们展示程序变换技术 distillation 如何用于将用函数式语言指定的反应式系统变换为简化形式，随后可分析该形式以验证系统的时序性质。旨在建模互斥的示例系统使用这些技术针对安全性（互斥）和活性（无饥饿）进行分析，其包含的错误被正确识别。
引用
@article{arxiv.1512.03860,
title = {Verifying Temporal Properties of Reactive Systems by Transformation},
author = {Geoff Hamilton},
journal= {arXiv preprint arXiv:1512.03860},
year = {2015}
}
备注
In Proceedings VPT 2015, arXiv:1512.02215. This work was supported, in part, by Science Foundation Ireland grant 10/CE/I1855 to Lero - the Irish Software Engineering Research Centre (www.lero.ie), and by the School of Computing, Dublin City University