CSP-OZ: a combination of object-Z and CSP
作者： Clemens Fischer
DOI: 10.1007/978-0-387-35261-9_29
关键词:
摘要: In this paper we define a combination of Object-Z and CSP called CSP-OZ. The basic idea is to CSP-semantics for every class. Special care taken capture the characteristics input output parameters properly preserve expected refinement rules.
core.ac.uk
springer.com
sci-hub.st 参考文章(22)
J. M. Spivey, The Z notation: a reference manual Prentice Hall International (UK) Ltd.. ,(1992)
A. W. Roscoe, J. C. P. Woodcock, L. Wulf, Non-Interference Through Determinism european symposium on research in computer security. pp. 33- 53 ,(1994) , 10.1007/3-540-58618-0_55
Bill Roscoe, An alternative order for the failures model ,(1988)
Tony Hoare, Communicating Sequential Processes ,(1985)
Clemens Fischer, Combining Object-Z and CSP. FBT. pp. 119- 128 ,(1997)
J. Derrick, E. A. Boiten, H. Bowman, M. W. A. Steen, Supporting ODP - Translating LOTOS to Z Springer, Boston, MA. pp. 399- 406 ,(1997) , 10.1007/978-0-387-35082-0_29
H. Tej, B. Wolff, A Corrected Failure Divergence Model for CSP in Isabelle/HOL formal methods. pp. 318- 337 ,(1997) , 10.1007/3-540-63533-5_17
Ben Strulo, How Firing Conditions Help Inheritance ZUM '95 Proceedings of the 9th International Conference of Z Usres on The Z Formal Specification Notation. pp. 264- 275 ,(1995) , 10.1007/3-540-60271-2_125
Eerke Boiten, Howard Bowman, John Derrick, Maarten Steen, Viewpoint Consistency in Z and LOTOS: A Case Study formal methods. pp. 644- 664 ,(1997) , 10.1007/3-540-63533-5_34
Rom Langerak, A Testing Theory for LOTOS using Deadlock Detection Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX. pp. 87- 98 ,(1989)