A type system for resource protocol verification and its correctness proof
A type system for resource protocol verification and its correctness proof
复制标题
一种资源协议验证类型系统及其正确性证明
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
W. Chin
中科院分区：
文献类型：
--
作者：
C. Popeea;W. Chin
我们提出了一种基于依赖打字的形式的新方法，以验证程序中资源的正确使用。我们的方法允许指定复杂的资源，其属性是由不变性和最终状态的注释类型和条件捕获的。协议本身是通过一组预定义的方法指定的，该方法的条件和后条件共同执行了每种资源类型的正确时间用法。我们设计一种简单的语言以及类型系统，该系统显示如何实现资源协议验证。我们对语言进行了正式的操作语义，并提供了正确的证明，该证明证实了良好的程序符合每种资源类型的指定协议。
We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are captured by annotated types and conditions on invariance and final states. The protocol itself is specified through a set of pre-defined methods, whose pre-condition and post-condition together, enforce the correct temporal usage of each resource type. We design a simple language together with a type system that shows how resource protocol verification can be achieved. We formalise an operational semantics for the language and provide a correctness proof which confirms that well-typed programs conform to the specified protocol of each resource type.