一种用于验证带寄存器和语音的结构化交互程序的可靠时空霍尔逻辑
编程语言
2008-10-21 v1 计算机科学中的逻辑
摘要
带寄存器和语音的交互系统（简称“rv-系统”）是一种交互计算模型，它通过时空对偶变换封闭寄存器机而得到（“语音”是“寄存器”的时间对偶对应物）。同样地，AGAPIA v0.1（一种针对 rv-系统的结构化编程语言）是经典 while 程序（针对特定数据类型）的时空对偶闭包。典型的 AGAPIA 程序描述了位于不同站点并具有适当响应环境的时间窗口的开放进程。该语言天然支持进程迁移、结构化交互以及在异构机器上的组件部署。本文引入了一种可靠的类霍尔时空逻辑，用于验证 AGAPIA v0.1 程序。作为案例研究，给出了一个流行的分布式终止检测协议的形式化验证证明。
引用
@article{arxiv.0810.3332,
title = {A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices},
author = {Cezara Dragoi and Gheorghe Stefanescu},
journal= {arXiv preprint arXiv:0810.3332},
year = {2008}
}
备注
21 pages, 8 figures, Invited submission for WADT'08 LNCS Proceedings