Refinement and verification of concurrent systems specified in Object-Z and CSP
Refinement and verification of concurrent systems specified in Object-Z and CSP
复制标题
Object-Z 和 CSP 中指定的并发系统的细化和验证
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
J. Derrick
中科院分区：
文献类型：
--
作者：
Graeme Smith;J. Derrick
通常，使用多种正式规范语言可以促进大型或复杂系统的形式开发。这种语言组合特别适合并发或分布式系统的规范，在这些系统中，过程和状态的建模都是必要的。本文提出了一种使用对象-Z和CSP（交流顺序过程）组合编写的规格进行细化和验证的方法。这两种语言的常见语义基础可以根据CSP的精致来使用一种统一的完善方法。为了使基于状态的技术用于规范的对象-Z组件，我们开发了基于状态的改进关系，这些相对于CSP改进而言是合理且完整的。另外，提出了一种用于静态和动态特性的验证方法。该方法允许我们通过使用CSP运算符的定律以及Object-Z的逻辑来验证CSP系统规范的属性。
The formal development of large or complex systems can often be facilitated by the use of more than one formal specification language. Such a combination of languages is particularly suited to the specification of concurrent or distributed systems, where both the modelling of processes and state is necessary. This paper presents an approach to refinement and verification of specifications written using a combination of Object-Z and CSP (communicating sequential processes). A common semantic basis for the two languages enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used for the Object-Z components of a specification, we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the CSP operators together with the logic for Object-Z.