{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:27:38Z","timestamp":1725492458205},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440437"},{"type":"electronic","value":"9783540456940"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45694-5_1","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T03:44:18Z","timestamp":1191555858000},"page":"1-23","source":"Crossref","is-referenced-by-count":4,"title":["Refinement and Verification Applied to an In-Flight Data Acquisition Unit*"],"prefix":"10.1007","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Natalia","family":"Ioustinova","sequence":"additional","affiliation":[]},{"given":"Ernst","family":"Kesseler","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Yaroslav S.","family":"Usenko","sequence":"additional","affiliation":[]},{"given":"Yuri A.","family":"Yushtein","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Th. Arts and I. A. van Langevelde. Correct performance of transaction capabilities. In Proceedings 2nd Conference on Applications of Concurrency to System Design (ICACSD\u20192001), Newcastle upon Tyne, UK, pp. 35\u201342. IEEE Computer Society Press, 2001.","DOI":"10.1109\/CSD.2001.981762"},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"\u03bcCRL: a toolset for analysing algebraic specifications","author":"S. C. C. Blom","year":"2001","unstructured":"S. C. C. Blom, W. J. Fokkink, J. F. Groote, I. A. van Langevelde, B. Lisser, and J. C. van de Pol. \u03bcCRL: a toolset for analysing algebraic specifications. In G. Berry, H. Comon, and A. Finkel, eds, Proceedings 13th Conference on Computer Aided Verification (CAV\u201901), Paris, France, LNCS 2102, pp. 250\u2013254. Springer-Verlag, July 2001."},{"key":"1_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/3-540-45263-X_25","volume-title":"The verification of coordination","author":"P. F. G. Dechering","year":"2000","unstructured":"P. F. G. Dechering and I. A. van Langevelde. The verification of coordination. In A. Porto and G.-C. Roman, Proceedings 4th Conference on Coordination Languages and Models (COORDINATION\u20192000), Limmasol, Cyprus, LNCS 1906, pp. 335\u2013340. Springer-Verlag, 2000."},{"key":"1_CR5","unstructured":"J. A. J. A. Dominicus, A. A. ten Have, M. C. Buitelaar, P. R. Hoek, and F. J. Carati. Functional requirements for an on-board loads and usage monitoring system for the WHL Lynx SH-14D helicopter. Report CR 97568, National Aerospace Laboratory, November 1997."},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"CADP\u2014 a protocol validation and verification toolbox","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP\u2014 a protocol validation and verification toolbox. In R. Alur and T. A. Henzinger, eds, Proceedings 8th Conference on Computer-Aided Verification (CAV\u201996), New Brunswick, New Jersey, LNCS 1102, pp. 437\u2013440. Springer-Verlag, 1996."},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R. J. Glabbeek van","year":"1996","unstructured":"R. J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555\u2013600, 1996.","journal-title":"Journal of the ACM"},{"key":"1_CR8","unstructured":"J. F. Groote, J. Pang, and A. G. Wouters. A balancing act: Analyzing a distributed lift system. In S. Gnesi and U. Ultes-Nitsche, eds, Proceedings 6th Workshop on Formal Methods for Industrial Critical Systems (FMICS\u20192001), Paris, France, pp. 1\u201312, 2001."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"J. F. Groote and A. Ponse. The syntax and semantics of \u03bcCRL. In A. Ponse, C. Verhoef, and S. F. M. van Vlijmen, editors, Algebra of Communicating Processes 1994, pages 26\u201362. Workshop in Computing Series, Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4471-2120-6_2"},{"issue":"5","key":"1_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"J. Hooman and J. C. van de Pol. Formal verification of replication on a distributed data space architecture. In Proceedings 17th Symposium on Applied Computing (SAC\u20192002)-Coordination Models, Languages and Applications, Madrid, Spain, pp. 351\u2013358. ACM Press, 2002.","DOI":"10.1145\/508791.508859"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyzer. In Proceedings 22nd Conference on Software Engineering (ICSE\u20192000), Limerick, Ireland, pp. 730\u2013733. ACM Press, 2000.","DOI":"10.1145\/337180.337616"},{"key":"1_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BFb0053367","volume-title":"Specification of an integrated circuit card protocol application using the B method and linear temporal logic","author":"J. Julliand","year":"1998","unstructured":"J. Julliand, B. Legeard, T. Machicoane, B. Parreaux, and B. Tatibou\u00ebt. Specification of an integrated circuit card protocol application using the B method and linear temporal logic. In D. Bert, ed., Proceedings 2nd B Conference (B\u201998)\u2014 Recent Advances in the Development and Use of the B Method, Montpellier, France, pp. 273\u2013292, LNCS 1393. Springer-Verlag, 1998."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"K. Lano and H. Haughton. Specification in B: An Introduction Using the B Toolkit. World Scientific, 1996.","DOI":"10.1142\/p006"},{"key":"1_CR15","unstructured":"R. Mateescu and M. Sighireanu. Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Technical Report 3899, INRIA, March 2000. To appear in Science of Computer Programming."},{"key":"1_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/3-540-45648-1_8","volume-title":"An approach to combining B and Alloy","author":"L. Mikhailov","year":"2002","unstructured":"L. Mikhailov and M. Butler. An approach to combining B and Alloy. In D. Bert, J. P. Bowen, M. C. Henson, and K. Robinson, eds, Proceedings 2nd Conference of B and Z Users (ZB\u20192002)\u2014 Formal Specification and Development in Z and B, Grenoble, France, pp. 140\u2013161, LNCS 2272. Springer-Verlag, 2002."},{"key":"1_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-46000-4_26","volume-title":"Formal specification of JavaSpaces architecture using \u03bcCRL","author":"J. C. de Pol van","year":"2002","unstructured":"J. C. van de Pol and M. Valero Espada. Formal specification of JavaSpaces architecture using \u03bcCRL. In F. Arbab and C. L. Talcott, eds, Proceedings 5th Conference on Coordination Languages and Models (COORDINATION\u20192002), York, UK, LNCS 2315, pp. 274\u2013290. Springer-Verlag, 2002."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"E. Sekerinski and K. Sere (eds). Program Development by Refinement. Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0585-5"},{"key":"1_CR19","unstructured":"A. L. Vergroesen, P. R. Hoek, F. J. Carati, J. A. J. A. Dominicus, A. A. ten Have, and D. Sch\u00fctz. An automatic in-flight data acquisition system for the RNLN Lynx helicopter. In Proceedings 19th International Symposium on Aircraft Integrated Monitoring Systems (AIMS\u201998), Garmisch Partenkirchen, Germany, May 1998."},{"key":"1_CR20","unstructured":"A. G. Wouters. Manual for the \u03bcCRL tool set (version 2.8.2). Report SEN-R0130, CWI, December 2001."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2002 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45694-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,23]],"date-time":"2019-02-23T18:25:52Z","timestamp":1550946352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45694-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440437","9783540456940"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45694-5_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}