{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:49Z","timestamp":1725484609438},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_25","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T05:26:02Z","timestamp":1180329962000},"page":"477-496","source":"Crossref","is-referenced-by-count":3,"title":["Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions"],"prefix":"10.1007","author":[{"given":"Fran\u00e7oise","family":"Bellegarde","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Chouali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Abrial. The B Book. Cambridge University Press \u2014 ISBN 0521-496195, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"Introducing dynamic constraints in B","author":"J. R. Abrial","year":"1998","unstructured":"J. R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Second Conference on the B method, France, volume 1393 of LNCS, pages 83\u2013128. Springer Verlag, April 1998."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"R. J. Back and R. Kurki-Sunio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symposium on principles of distributed computing, pages 131\u2013142, 1983.","DOI":"10.1145\/800221.806716"},{"key":"25_CR4","unstructured":"F. Bellegarde, S. Chouali, J. Julliand, and O. Kouchnarenko. Comment limiter la sp\u00e9cification de l\u2019\u00e9quit\u00e9 dans les syst\u00e8mes d\u2019\u00e9v\u00e9nements B. In Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciels (AFADL\u201901), pages 205\u2013219, Nancy, France, 2001."},{"key":"25_CR5","unstructured":"D. Bert. Preuve de propri\u00e9t\u00e9s d\u2019\u00e9quit\u00e9 en B: \u00e9tude du protocole du bus SCSI-3. In Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciels (AFADL\u201901), pages 221\u2013241, Nancy, France, 2001."},{"key":"25_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-40911-4_14","volume-title":"Construction of finite labelled transition systems from B abstract systems","author":"D. Bert","year":"2000","unstructured":"D. Bert and F. Cave. Construction of finite labelled transition systems from B abstract systems. In In proc. of IFM\u20192000, volume 1945 of LNCS, pages 235\u2013254. Springer Verlag, November 2000."},{"key":"25_CR7","unstructured":"R. Bharadwaj and J. I. Zucker. Direct model checking of temporal properties (version 2). Technical Report CRL Report 317, Communications Research Laboratory, jan 1996."},{"issue":"2","key":"25_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0167-6423(96)81173-7","volume":"27","author":"M. J. Butler","year":"1996","unstructured":"M. J. Butler. Stepwise re.nement of communicating systems. Science of Computer Programming, 27(2):139\u2013173, 1996.","journal-title":"Science of Computer Programming"},{"key":"25_CR9","series-title":"Lect Notes Comput Sci","first-page":"223","volume-title":"An approach to the design fo distributed systems with B amn","author":"M. J. Butler","year":"1997","unstructured":"M. J. Butler. An approach to the design fo distributed systems with B amn. In J. P Brown and D. Till, editors, 10th International Conference of Z Users (ZUM\u201997), volume LNCS 1212, pages 223\u2013241. Springer-Verlag, April 1997."},{"key":"25_CR10","unstructured":"M. J. Butler and M. Walden. Distributed system development in B. In H. Habrias, editor, First B Conference, pages 155\u2013168, November 1996."},{"issue":"3","key":"25_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1987","unstructured":"E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"K. Etessami and G. Holzmann. Optimizing B\u00fcchi automata. In Proceedings of 11th Int. Conf. on Concurrency Theory (CONCUR), pages 153\u2013167, 2000.","DOI":"10.1007\/3-540-44618-4_13"},{"key":"25_CR13","unstructured":"Comit\u00e9 europ\u00e9en de Normalisation. En27816-3. European standard \u2014 identification cards \u2014 integrated circuit(s) card with contacts-electronic signal and transmission protocols. Technical Report ISO\/CEI 7816-3, 1992."},{"key":"25_CR14","unstructured":"R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. IFIP-WG6.1 Symposium On Protocols Specification, Testing and Verification (PSTV95), pages 2\u201321, Warsaw-Poland, 1995."},{"key":"25_CR15","unstructured":"G. Holzmann. Design and validation of protocols. Prentice hall software series, 1991."},{"key":"25_CR16","unstructured":"J. Julliand, P.A. Masson, and H. Mountassir. V\u00e9rification par model checking modulaire des propri\u00e9t\u00e9s dynamiques introduites en B. In Technique et Science Informatiques, 2001. to appear."},{"key":"25_CR17","series-title":"Lect Notes Comput Sci","first-page":"273","volume-title":"REX WorkshopA Decade of Concurrency","author":"Y. Kesten","year":"1993","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In REX WorkshopA Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 273\u2013346. Springer Verlag, 1993."},{"issue":"3","key":"25_CR18","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions On Programming Languages And Systems, TOPLAS"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings of the 9th ACM Symposium on Principles of Distributed Computing (PODC), pages 377\u2013408, New York, NY, 1990. ACM Press.","DOI":"10.1145\/93385.93442"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag-ISBN 0-387-97664-7, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"7","key":"25_CR21","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Zohar Manna and Amir Pnueli. Models for reactivity. Acta Informatica, 30(7):609\u2013678, 1993.","journal-title":"Acta Informatica"},{"key":"25_CR22","unstructured":"Steria M\u00e9diterran\u00e9e. Le langage B. Manuel de r\u00e9f\u00e9rence version 1.5. S.A.V. Steria, BP 16000, 13791 Aix-en-Provence cedex 3, France."},{"key":"25_CR23","unstructured":"B. Parreaux. V\u00e9rification de syst\u00e8mes d\u2019\u00e9v\u00e9nements B par model-checking PLTL. PhD thesis, U.F.R. des Sciences et Techniques, Universit\u00e9 de Franche-Comt\u00e9, D\u00e9cembre 2000."},{"key":"25_CR24","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. E. Tarjan","year":"1972","unstructured":"R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput, 1:146\u2013160, 1972.","journal-title":"SIAM J. Comput"},{"key":"25_CR25","unstructured":"M. Vardi and P. Wolper. An automata-theoric approach to automatic program verification. In 1 st IEEE Symp. Logic in Computer Science (LICS\u201986), pages 332\u2013344, Cambridge, MA, USA, june 1986."},{"issue":"1","key":"25_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasonning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"25_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Verifying properties of large sets of processes with network invariants","author":"P. Wolper","year":"1990","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Int. Workshopon Automatic Verification Methods for Finite State Systems, LNCS 407, pages 68\u201380, Grenoble, France, june 1989. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:14:25Z","timestamp":1556450065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}