{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:12Z","timestamp":1740098952565,"version":"3.37.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_15","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T07:34:48Z","timestamp":1508139288000},"page":"250-265","source":"Crossref","is-referenced-by-count":1,"title":["Construction of Abstract State Graphs for Understanding Event-B Models"],"prefix":"10.1007","author":[{"given":"Daichi","family":"Morita","sequence":"first","affiliation":[]},{"given":"Fuyuki","family":"Ishikawa","sequence":"additional","affiliation":[]},{"given":"Shinichi","family":"Honiden","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","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)"},{"issue":"6","key":"15_CR2","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. (STTT) 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"15_CR3","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, Chap. 26, pp. 825\u2013885. IOS Press (2009)"},{"key":"15_CR4","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-78800-3_24"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Dulac, N., Viguier, T., Leveson, N.G., Storey, M.D.: On the use of visualization in formal requirements specification. In: Proceedings of the IEEE Joint International Conference on Requirements Engineering, pp. 71\u201380 (2002)","DOI":"10.1109\/ICRE.2002.1048507"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1980), pp. 163\u2013173. ACM, New York (1980)","DOI":"10.1145\/567446.567462"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). doi:\n10.1007\/3-540-63166-6_10"},{"key":"15_CR9","unstructured":"Ham, F.V., van de Wetering, H., Van Wijk, J.J.: Visualization of state transition graphs. In: Proceedings of the IEEE Symposium on Information Visualization 2001 (INFOVIS 2001), p. 59. IEEE Computer Society, Washington, DC (2001)"},{"issue":"6","key":"15_CR10","doi-asserted-by":"crossref","first-page":"909","DOI":"10.1007\/s00165-016-0376-0","volume":"28","author":"TS Hoang","year":"2016","unstructured":"Hoang, T.S., Schneider, S., Treharne, H., Williams, D.M.: Foundations for using linear temporal logic in Event-B refinement. Form. Aspects Comput. 28(6), 909\u2013935 (2016)","journal-title":"Form. Aspects Comput."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-25423-4_10","volume-title":"Formal Methods and Software Engineering","author":"L Ladenberger","year":"2015","unstructured":"Ladenberger, L., Leuschel, M.: Mastering the visualization of larger state spaces with projection diagrams. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 153\u2013169. Springer, Cham (2015). doi:\n10.1007\/978-3-319-25423-4_10"},{"issue":"2","key":"15_CR12","doi-asserted-by":"crossref","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. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/11415787_2","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"M Leuschel","year":"2005","unstructured":"Leuschel, M., Turner, E.: Visualising larger state spaces in PRO\n          B. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6\u201323. Springer, Heidelberg (2005). doi:\n10.1007\/11415787_2"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1985), pp. 97\u2013107. ACM, New York (1985)","DOI":"10.1145\/318593.318622"},{"issue":"1","key":"15_CR15","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"12","author":"D Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12(1), 9\u201321 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR16","unstructured":"Snook, C., Butler, M.: UML-B and Event-B: an integration of languages and tools. In: Proceedings of the IASTED International Conference on Software Engineering (SE 2008), pp. 336\u2013341. ACTA Press, Anaheim (2008)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T07:38:55Z","timestamp":1508139535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}