论文标题
使用Promela和Spin的GO中消息通讯并发的有限验证
Bounded verification of message-passing concurrency in Go using Promela and Spin
论文作者
论文摘要
本文介绍了GO编程语言的消息片段的静态验证框架。我们的框架提取模型，使程序的通话行为过高。这些模型或行为类型是在Promela中编码的，因此可以通过自旋进行有效验证。我们通过验证包含与通信相关的参数的程序进行改进的工作，这些程序在编译时未知的参数，即产生参数数的线程数或创建具有参数化容量的通道的程序。通过用户提供的界限，通过有限的验证方法检查了这些程序。
This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or behavioural types, are encoded in Promela, hence can be efficiently verified with Spin. We improve on previous works by verifying programs that include communication-related parameters that are unknown at compile-time, i.e., programs that spawn a parameterised number of threads or that create channels with a parameterised capacity. These programs are checked via a bounded verification approach with bounds provided by the user.
