{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:20:56Z","timestamp":1742912456461,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_25","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"421-436","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Proving Event Ordering Properties for Information Systems"],"prefix":"10.1007","author":[{"given":"Marc","family":"Frappier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge, UK, 1996."},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"Second International B Conference","author":"J.-R. Abrial","year":"1998","unstructured":"Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In Second International B Conference, D. Bert, ed., LNCS 1393, Springer-Verlag, 83\u2013128, April 1998."},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T. and Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25\u201359, 1987.","journal-title":"Computer Networks and ISDN Systems"},{"key":"25_CR4","unstructured":"Butler, M. J., Wald\u00e9n, M.: Distributed System Development in B. In First B Conference, H. Habrias, ed., November 1996."},{"issue":"4","key":"25_CR5","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, 12(4):182\u2013198, 2000.","journal-title":"Formal Aspects of Computing"},{"key":"25_CR6","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume":"2","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In Formal Methods for Open Object-Based Distributed Systems (FMOODS\u201997), volume 2, 423\u2013438, Chapman & Hall, 1997.","journal-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS\u201997)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Frappier, M., St-Denis, R.: Combining JSD and Cleanroom for Object-Oriented Scenario Specification. In Object-Oriented Behavioral Specifications, H. Kilov, B. Rumpe, I. Simmonds, eds., Kluwer Academic Publishers, 1999.","DOI":"10.1007\/978-1-4615-5229-1_5"},{"key":"25_CR8","volume-title":"Technical Report","author":"M. Frappier","year":"2002","unstructured":"Frappier, M., St-Denis, R.: Specifying Information Systems through Structured Input-Output Traces, Technical Report, D\u00e9partement de math\u00e9matiques et d\u2019informatique, Universit\u00e9 de Sherbrooke, Sherbrooke (Qu\u00e9bec), Canada J1K 2R1, 2002."},{"key":"25_CR9","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":"25_CR10","volume-title":"ASE: 15th IEEE Conference on Automated Software Engineering","author":"R. Laleau","year":"2000","unstructured":"Laleau, R. Mammar, A.: An Overview of a Method and its Support Tool for Generating B Specifications from UML Notations. In ASE: 15th IEEE Conference on Automated Software Engineering, Grenoble, France, IEEE Computer Society Press, September 2000."},{"key":"25_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1007\/3-540-48119-2_48","volume-title":"Formal Methods (FM\u201999)","author":"E. Meyer","year":"1999","unstructured":"Meyer, E., Souqui\u00e8res, J.: A Systematic approach to Transform OMT Diagrams to a B specification. In Formal Methods (FM\u201999), J.M. Wing, J. Woodcook, J. Davies, eds., LNCS 1708 vol. 1, Springer-Verlag, 875\u2013895, September 1999."},{"key":"25_CR12","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989."},{"key":"25_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-47884-1_8","volume-title":"3rd International Conference on Integrated Formal Methods (IFM\u201902)","author":"E. Sekerinski","year":"2002","unstructured":"Sekerinski, E., Zurob, R.: Translating Statecharts to B, In 3rd International Conference on Integrated Formal Methods (IFM\u201902), M. Butler, L. Petre, K. Sere, eds, LNCS 2335, Springer-Verlag, 128\u2013144, Turku, Finland, May 2002."},{"key":"25_CR14","unstructured":"Butler, M., and Snook, C.: Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. In UML 2000 Workshop, Dynamic Behaviour in UML Models: Semantic Questions. York, UK, 2\u20136 October, 2000."},{"key":"25_CR15","unstructured":"Snook, C., Walden, M.: Use of U2B for Specifying B Action Systems. In International workshop on Refinement of Critical Systems: Methods, Tools and Experience (RCS\u201902), Grenoble, France, January 2002."},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1023\/A:1011269103179","volume":"18","author":"G. Smith","year":"2001","unstructured":"Smith, G., Derrick, J.: Specification, Refinement and Verification of Concurrent Systems An Integration of Object-Z and CSP. Formal Methods in System Design, 18:249\u2013284, 2001.","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T13:30:00Z","timestamp":1675085400000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}