摘要: In this paper we discuss a simple integration of timed CSP and Object-Z. Following existing work, the components in such an are written as either Object-Z classes, or processes, combined together using parallel composition. Here approach general, describe how semantics can be used integrated notation. We briefly verification analysis for descriptions, before providing more in-depth discussion refinement approach. both individual components, well two-event model which distinguishes between start end events. The latter allows operation duration to specified show integrates into traditional state-based simulation rules.
springer.com
core.ac.uk
sci-hub.st 参考文章(22)
Carsten Sühl, RT-Z: An Integration of Z and timed CSP IFM’99. pp. 29- 48 ,(1999) , 10.1007/978-1-4471-0851-1_3
Clemens Fischer, How to Combine Z with Process Algebra ZUM '98 Proceedings of the 11th International Conference of Z Users on The Z Formal Specification Notation. pp. 5- 23 ,(1998) , 10.1007/978-3-540-49676-2_2
Roger Duke, Gordon Rose, Formal Object Oriented Specification Using Object-Z ,(2000)
Clemens Fischer, Heike Wehrheim, Model-Checking CSP-OZ Specifications with FDR IFM’99. pp. 315- 334 ,(1999) , 10.1007/978-1-4471-0851-1_17
Graeme Smith, The Object-Z specification language ,(1999)
Steve Schneider, Concurrent and Real-time Systems: The CSP Approach ,(1999)
S. D. Brookes, A. W. Roscoe, An Improved Failures Model for Communicating Processes international conference on concurrency theory. pp. 281- 305 ,(1984) , 10.1007/3-540-15670-4_14
Graeme Smith, A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems formal methods. ,vol. 1313, pp. 62- 81 ,(1997) , 10.1007/3-540-63533-5_4
G. Smith, J. Derrick, Refinement and verification of concurrent systems specified in Object-Z and CSP international conference on formal engineering methods. pp. 293- 302 ,(1997) , 10.1109/ICFEM.1997.630436
Luca Aceto, Action Refinement in Process Algebras ,(1992)