使用 Promela 与 Spin 对 Go 中的消息传递并发进行有界验证
编程语言
2020-04-06 v1 软件工程
摘要
本文描述了一种针对 Go 编程语言中消息传递片段的静态验证框架。我们的框架提取了对程序消息传递行为进行过近似的模型。这些模型，或称行为类型，被编码于 Promela 中，因此可以用 Spin 高效验证。我们通过验证包含编译期未知通信相关参数的程序改进了先前的工作，即生成参数化数量线程或创建参数化容量通道的程序。这些程序通过用户提供界的有界验证方法进行检查。
引用
@article{arxiv.2004.01323,
title = {Bounded verification of message-passing concurrency in Go using Promela and Spin},
author = {Nicolas Dilley and Julien Lange},
journal= {arXiv preprint arXiv:2004.01323},
year = {2020}
}
备注
In Proceedings PLACES 2020, arXiv:2004.01062