{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:54:13Z","timestamp":1742928853261,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_8","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"110-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Checking the Conformance of a Promela Design to its Formal Specification in Event-B"],"prefix":"10.1007","author":[{"given":"Dieu-Huong","family":"Vu","sequence":"first","affiliation":[]},{"given":"Yuki","family":"Chiba","sequence":"additional","affiliation":[]},{"given":"Kenro","family":"Yatake","sequence":"additional","affiliation":[]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Aoki, T.: Model checking multi-task software on real-time operating systems. In: The 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing, pp. 551\u2013555 (2008)","DOI":"10.1109\/ISORC.2008.46"},{"key":"8_CR3","series-title":"Representation and Mind Series","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)"},{"key":"8_CR4","unstructured":"Bert, D., Potet, M.L., Stouls, N.: Genesyst: a tool to reason about behavioralaspects of B event specifications. Application to security properties (2010)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/10722468_18","volume-title":"SPIN Model Checking and Software Verification","author":"P Broadfoot","year":"2000","unstructured":"Broadfoot, P., Roscoe, B.: Tutorial on FDR and its applications. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, p. 322. Springer, Heidelberg (2000)"},{"issue":"1","key":"8_CR6","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1002\/stvr.1482","volume":"24","author":"Y Choi","year":"2014","unstructured":"Choi, Y.: Model checking trampoline OS: a case study on safety analysis for automotive software. Softw. Test. Verif. Reliab. 24(1), 38\u201360 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"5","key":"8_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411\u2013420. ACM, New York (1999)","DOI":"10.1145\/302405.302672"},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations I.: Untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-10373-5_25","volume-title":"Formal Methods and Software Engineering","author":"PJ Matos","year":"2009","unstructured":"Matos, P.J., Fischer, B., Marques-Silva, J.: A Lazy Unbounded Model Checker for Event-B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 485\u2013503. Springer, Heidelberg (2009)"},{"key":"8_CR13","series-title":"PHI Series in computer science","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall, Upper Saddle River (1989)"},{"key":"8_CR14","unstructured":"Muller, A.: VDM the Vienna development method (2009)"},{"key":"8_CR15","unstructured":"Muller, T.: Formal methods, model-cheking and Rodin plugin development to link Event-B and Spin (2009)"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-1-4471-4534-9_6","volume-title":"Mathematics in Computing","author":"G O\u2019Regan","year":"2013","unstructured":"O\u2019Regan, G.: Z formal specification language. In: O\u2019Regan, G. (ed.) Mathematics in Computing, pp. 109\u2013122. Springer, London (2013)"},{"key":"8_CR17","unstructured":"OSEK\/VDX Group: OSEK\/VDX operating system specification 2.2.3. http:\/\/portal.osek-vdx.org\/"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/j.entcs.2009.12.024","volume":"259","author":"S Reeves","year":"2009","unstructured":"Reeves, S., Streader, D.: Guarded operations, refinement and simulation. Electron. Notes Theor. Comput. Sci. 259, 177\u2013191 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"In der Rieden, T., Knapp, S.: An approach to the pervasive formal specification and verification of an automotive system. In: Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, pp. 115\u2013124 (2005)","DOI":"10.1145\/1081180.1081195"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Vu, D.H., Aoki, T.: Faithfully formalizing OSEK\/VDX operating system specification. In: Proceedings of the 3rd Symposium on Information and Communication Technology, pp. 13\u201320 (2012)","DOI":"10.1145\/2350716.2350721"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-32943-2_15","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"K Yatake","year":"2012","unstructured":"Yatake, K., Aoki, T.: Model checking of OSEK\/VDX OS design model based on environment modeling. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 183\u2013197. Springer, Heidelberg (2012)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T23:45:49Z","timestamp":1676936749000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_8","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}