使用Promela和Spin对Go中的消息传递并发性进行有界验证
Bounded verification of message-passing concurrency in Go using Promela and Spin
摘要：
本文描述了Go程序设计语言的消息传递片段的静态验证框架。我们的框架提取模型，过度近似的程序的消息传递行为。这些模型或行为类型在Promela中编码，因此可以通过Spin有效验证。我们通过验证包含在编译时未知的通信相关参数的程序来改进以前的工作，即，生成参数化线程数或创建具有参数化容量的通道的程序。这些程序是通过一个有界的验证方法与用户提供的界限进行检查。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
