{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:35:08Z","timestamp":1725496508351},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540644057"},{"type":"electronic","value":"9783540697695"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0053367","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T06:05:53Z","timestamp":1149660353000},"page":"273-292","source":"Crossref","is-referenced-by-count":4,"title":["Specification of an integrated circuit card protocol application using the B method and linear temporal logic"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Julliand","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Legeard","sequence":"additional","affiliation":[]},{"given":"Thierry","family":"Machicoane","sequence":"additional","affiliation":[]},{"given":"Benoit","family":"Parreaux","sequence":"additional","affiliation":[]},{"given":"Bruno","family":"Tatibou\u00cbt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,22]]},"reference":[{"key":"18_CR1","unstructured":"J. R. Abrial-The B Book-Cambridge University Press, 1996-ISBN 0521-496195."},{"key":"18_CR2","unstructured":"J-R. Abrial-Extending B without Changing it (for Developping Distributed Systems) \u2014 1st Conference on the B method-November 1996. Nantes."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"J-R. Abrial, Mussat L-Specification and Design of a transmission protocol by successive refinements using B \u2014 to appear in LNCS. 1997.","DOI":"10.1007\/978-3-642-60858-2_17"},{"key":"18_CR4","unstructured":"J. R. Abrial-Constructions d'Automatismes Industriels avec B \u2014 Congr\u00e9s AFADL \u2014 ONERA-CERT Toulouse-Mai 1997."},{"key":"18_CR5","unstructured":"G. Bernot, S. Coudret, P. Le Gall-Heterogeneous formal specifications-Proc. of the 5th Int. Conf. on Algebraic Methodology and Software Technology-AMAST'96-pp 548\u2013472-LNCS 1101."},{"key":"18_CR6","unstructured":"M. Butler, M. Walden-Distributed System Development in B-1st Conference on the B method-November 1996-Nantes."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis-Memory efficient algorithms for the v\u00e9rification of temporal properties-Formal Methods in System Design I-pp 275\u2013288.","DOI":"10.1007\/BF00121128"},{"key":"18_CR8","unstructured":"European Standard-Identification Cards-Integrated circuit(s) cards with contacts-Electronic Signal and transmission protocols-ISO\/CEI 7816-3-1992."},{"key":"18_CR9","unstructured":"Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control-ISBN 3-540-61929-1-Springer Verlag-1996."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Vardi, P. Wolper-Simple on-the-fly automatic verification of linear temporal logic-Proc. PSTV95 Conference-Warsaw-Poland-1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"18_CR11","unstructured":"P. Godefroid and G. Holzmann-On the verification of temporal properties-Proc. IFIP\/WG6.1 Symp. On Protocols Specification, Testing and Verification-PSTV93-Liege-Belgium-June 1993."},{"key":"18_CR12","unstructured":"G. Holzmann-Design and validation of protocols-Prentice hall software series-1991."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"G. Holzmann, D. Peled and Y. Yannakakis-On the nested depth-first search. Proc. 2nd Spin Workshop-American Mathematical Society-DIMACS\/32-1996.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"18_CR14","unstructured":"G. Holzmann-State compression in SPIN. Proc. 3rd Spin Workshop-Twente University-April 1997."},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"G. Holzmann-The model checker SPIN. IEEE Trans. On Software Engineering-Vol. 23, No 5.","DOI":"10.1109\/32.588521"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"K. Lano-Formal Object-Oriented Development-Springer-Verlag-1995.","DOI":"10.1007\/978-1-4471-3073-4"},{"key":"18_CR17","unstructured":"K. Lano, J. Bicarregui, A. Sanchez-Using B to Design and Verify Controllers for Chemical Processing-1st Conference on the B method-November 1996-Nantes."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli-The Temporal Logic of Reactive and Cocurrent Systems: Specification. ISBN 0-387-97664-7-Springer-Verlag-1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli-Temporal Verification of Reactive Systems: Safety. ISBN 0-387-94459-1-Springer-Verlag-1995.","DOI":"10.1007\/978-1-4612-4222-2_1"},{"key":"18_CR20","unstructured":"Manuel de r\u00e9f\u00e9rence du langage B-Steria M\u00e9diterran\u00e9e-D\u00e9cembre 1996."},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"D. A. Peled-Combining partial order reduction with on-the-fly model checking-Proc. 6th Int. Conf. On Computer Aided Verification-CAV94-Stanford-1994.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"18_CR22","unstructured":"D. Mery-Machines abstraites temporelles-Analyse comparative de B et de TLA+-1st Conference on the B method-November 1996-Nantes."}],"container-title":["Lecture Notes in Computer Science","B\u201998: Recent Advances in the Development and Use of the B Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0053367","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T17:05:51Z","timestamp":1683479151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0053367"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540644057","9783540697695"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0053367","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}