Type inference and strong static type checking for Promela
Type inference and strong static type checking for Promela
复制标题
Promela 的类型推断和强静态类型检查
DOI：
10.1016/j.scico.2010.05.010
复制
发表时间：
2010
影响因子：
1.3
通讯作者：
Donaldson A
中科院分区：
文献类型：
--
作者：
Donaldson A
Spin模型检查器及其规范语言Promela在工业界和学术界广泛用于检查分布式算法和协议的逻辑属性。Spin的模型检查涉及通过抽象的Promela规范对系统进行推理，因此该技术严重依赖于该规范的可靠性。Promela包含一组丰富的数据类型，包括第一类通道，但语言语法限制了通道类型的声明，因此通常不可能直接从其声明中推导出通道的完整类型。我们提出的设计和实现蚀刻，增强型检查器的Promela，它使用基于约束的类型推断执行强类型检查的Promela规范，允许静态检测的错误，自旋不会检测到，直到模拟/验证时间，或自旋可能完全错过。我们讨论的理论和实际问题与设计一个类型系统和类型检查现有的语言，并正式我们的方法使用Promela类演算。为了处理基本类型之间的子类型，我们提出了一个扩展的标准统一算法来解决系统的平等和子类型的约束，有界替换的基础上。
The Spin model checker and its specification language Promela have been used extensively in industry and academia to check the logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of channel types so that it is not generally possible to deduce the complete type of a channel directly from its declaration. We present the design and implementation of Etch, an enhanced type checker for Promela, which uses constraint-based type inference to perform strong type checking of Promela specifications, allowing static detection of errors that Spin would not detect until simulation/verification time, or that Spin may miss completely. We discuss theoretical and practical problems associated with designing a type system and type checker for an existing language, and formalise our approach using a Promela-like calculus. To handle subtyping between base types, we present an extension to a standard unification algorithm to solve a system of equality and subtyping constraints, based on bounded substitutions.
登录
查看更多内容
子类型不等式
DOI：
10.1109/lics.1992.185543
发表时间：
1992
期刊：
[1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
J. Tiuryn
通讯作者：
J. Tiuryn
动态交互的类型
DOI：
--
发表时间：
1993
期刊：
--
影响因子：
--
作者：
Kohei Honda
通讯作者：
Kohei Honda
DOI：
10.1007/3-540-46425-5_18
发表时间：
2000
期刊：
--
影响因子：
--
作者：
Laurent Mauborgne
通讯作者：
Laurent Mauborgne
隐式类型高阶语言中的类型错误切片
影响因子：
1.3
作者：
C. Haack;J. Wells
通讯作者：
J. Wells
具有子类型的类型推断框架
DOI：
10.1145/289423.289448
发表时间：
1998
期刊：
--
影响因子：
--
作者：
F. Pottier
通讯作者：
F. Pottier