{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:30:51Z","timestamp":1759991451571},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540347507"},{"type":"electronic","value":"9783540347521"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11768173_6","type":"book-chapter","created":{"date-parts":[[2006,6,21]],"date-time":"2006-06-21T12:02:49Z","timestamp":1150891369000},"page":"85-100","source":"Crossref","is-referenced-by-count":3,"title":["Constructing Property-Oriented Models for Verification"],"prefix":"10.1007","author":[{"given":"Jifeng","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Sherif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M. Butler","year":"2000","unstructured":"Butler, M.: csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of computing\u00a012, 182\u2013196 (2000)","journal-title":"Formal Aspects of computing"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","volume":"138","author":"J. Davies","year":"1995","unstructured":"Davies, J., Schneider, S.: A brief history of Timed CSP. Theoretical Computer Science\u00a0138, 243\u2013271 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"6_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-30482-1_39","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2004","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Wang, Y.: Timed Patterns: TCOZ to Timed Automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 483\u2013498. Springer, Heidelberg (2004)"},{"key":"6_CR5","series-title":"Cornerstones of Computing Series","volume-title":"Formal Object Oriented Specification Using Object-Z","author":"R. Duke","year":"2000","unstructured":"Duke, R., Rose, G.: Formal Object Oriented Specification Using Object-Z. Cornerstones of Computing Series. Macmillan, Basingstoke (2000)"},{"key":"6_CR6","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997)","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol.\u00a02, pp. 423\u2013438. Chapman & Hall, Boca Raton (1997)"},{"key":"6_CR7","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"6_CR8","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"6_CR9","unstructured":"Li, L., He, J.: Towards a Denotational Semantics of Timed RSL using Duration Calculus. Technical Report 161, UNU\/IIST (April 1999)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1166","DOI":"10.1007\/3-540-48118-4_12","volume-title":"FM\u201999 - Formal Methods","author":"B. Mahony","year":"1999","unstructured":"Mahony, B., Dong, J.S.: Sensors and Actuators in TCOZ. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, p. 1166. Springer, Heidelberg (1999)"},{"issue":"2","key":"6_CR11","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1109\/32.841115","volume":"26","author":"B. Mahony","year":"2000","unstructured":"Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering\u00a026(2), 150\u2013177 (2000)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/s001650200004","volume":"13","author":"B. Mahony","year":"2002","unstructured":"Mahony, B., Dong, J.S.: Deep Semantic Links of TCSP and Object-Z: TCOZ Approach. Formal Aspects of Computing\u00a013(2), 142\u2013160 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR13","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-45236-2_19","volume-title":"FME 2003: Formal Methods","author":"S.C. Qin","year":"2003","unstructured":"Qin, S.C., Dong, J.S., Chin, W.N.: A Semantics Foundation for TCOZ in Unifying Theories of Programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 321\u2013340. Springer, Heidelberg (2003)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45614-7_26","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A. Sampaio","year":"2002","unstructured":"Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 451\u2013470. Springer, Heidelberg (2002)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/BFb0032011","volume-title":"Real-Time: Theory in Practice","author":"S. Schneider","year":"1992","unstructured":"Schneider, S., Davies, J., Jackson, D.M., Reed, G.M., Reed, J.N., Roscoe, A.W.: Timed CSP: Theory and practice. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 640\u2013675. Springer, Heidelberg (1992)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-36103-0_62","volume-title":"Formal Methods and Software Engineering","author":"A. Sherif","year":"2002","unstructured":"Sherif, A., He, J.: Towards a Timed Model for Circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 613\u2013624. Springer, Heidelberg (2002)"},{"key":"6_CR18","volume-title":"Advances in Formal Methods","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. In: Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1109\/ICFEM.1997.630436","volume-title":"International Conference on Formal Engineering Methods","author":"G. Smith","year":"1997","unstructured":"Smith, G., Derrick, J.: Refinement and verification of concurrent systems specified in Object-Z and CSP. In: International Conference on Formal Engineering Methods, pp. 293\u2013302. IEEE Computer Society, Los Alamitos (1997)"},{"key":"6_CR20","series-title":"Prentice Hall International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"6_CR21","unstructured":"Woodcock, J., Cavalcanti, A.: Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Wofson Building, Parks Road, Oxford OX1 3QD, UK (July 2001)"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1109\/APSEC.2001.991490","volume-title":"The 8th Asia-Pacific Software Engineering Conference (APSEC 2001)","author":"J. Woodcock","year":"2001","unstructured":"Woodcock, J., Cavalcanti, A.: The steam boiler in a unified theory of Z and CSP. In: He, J., Li, Y., Lowe, G. (eds.) The 8th Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 291\u2013298. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J. Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11768173_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:50Z","timestamp":1619507570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11768173_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540347507","9783540347521"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11768173_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}