{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T03:50:54Z","timestamp":1769313054004,"version":"3.49.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,8,15]],"date-time":"2015-08-15T00:00:00Z","timestamp":1439596800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s10009-015-0395-9","type":"journal-article","created":{"date-parts":[[2015,8,14]],"date-time":"2015-08-14T08:25:10Z","timestamp":1439540710000},"page":"187-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Validation of the ABZ landing gear system using ProB"],"prefix":"10.1007","volume":"19","author":[{"given":"Lukas","family":"Ladenberger","sequence":"first","affiliation":[]},{"given":"Dominik","family":"Hansen","sequence":"additional","affiliation":[]},{"given":"Harald","family":"Wiegard","sequence":"additional","affiliation":[]},{"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,15]]},"reference":[{"key":"395_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-book: Assigning programs to meanings. Cambridge University Press, New York (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"395_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"395_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) Proceedings ICFEM\u201906, LNCS 4260, pp. 588\u2013605. Springer-Verlag (2006)","DOI":"10.1007\/11901433_32"},{"key":"395_CR4","unstructured":"Bendisposto, J.: Directed and Distributed Model Checking of B-Specifications. Dissertation, University of D\u00fcsseldorf (2015)"},{"key":"395_CR5","doi-asserted-by":"crossref","unstructured":"Bert, D., Potet, M.-L., Stouls, N.: Genesyst: A tool to reason about behavioral aspects of B event specifications. application to security properties. In ZB 2005, pages 299\u2013318 (2005)","DOI":"10.1007\/11415787_18"},{"key":"395_CR6","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: ABZ Case Study. Communications in Computer Information Science, vol. 433. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"395_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E.: Abstract State Machines. Springer, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"395_CR8","doi-asserted-by":"crossref","unstructured":"Bouton, T., de\u00a0Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: Verit: an open, trustable and efficient smt-solver. In: Schmidt, R.A. (eds.) Proc. Conference on Automated Deduction (CADE), Lecture Notes in Computer Science, pp. 151\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"395_CR9","unstructured":"Cansell, D., M\u00e9ry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besan\u00e7on, France, January 17\u201319, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4355 pp. 140\u2013154. Springer (2007)"},{"key":"395_CR10","unstructured":"Dahlstr\u00f6m, E., Dengler, P., Grasso, A., Liley, C., McCormack, C., Schepers, D., Watt, J.: Scalable vector graphics (svg) 1.1. World Wide Web Consortium Recommendation, vol. 16 (2011)"},{"key":"395_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS, LNCS 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"395_CR12","doi-asserted-by":"crossref","unstructured":"Deharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Smt solvers for rodin. In: Proceedings ABZ\u20192012, LNCS. Springer (to appear)","DOI":"10.1007\/978-3-642-30885-7_14"},{"key":"395_CR13","doi-asserted-by":"crossref","unstructured":"Gmehlich, R., Grau, K., Hallerstede, S., Leuschel, M., L\u00f6sch, F., Plagge, D.: On fitting a formal method into practice. In: Qin, S., Qiu, Z. (eds.) Proceedings ICFEM\u20192011, Lecture Notes in Computer Science, vol. 6991, pp. 195\u2013210. Springer (2011)","DOI":"10.1007\/978-3-642-24559-6_15"},{"key":"395_CR14","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.scico.2013.03.008","volume":"82","author":"S Hallerstede","year":"2014","unstructured":"Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2\u201321 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"4\u20135","key":"395_CR15","first-page":"767","volume":"11","author":"S Hallerstede","year":"2011","unstructured":"Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4\u20135), 767\u2013782 (2011)","journal-title":"TPLP"},{"key":"395_CR16","doi-asserted-by":"crossref","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ Landing Gear System using ProB. In: ABZ 2014: The Landing Gear Case Study, pp. 66\u201379. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_5"},{"key":"395_CR17","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Abrial, J.: Event-b decomposition for parallel programs. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22\u201325, 2010. Proceedings, Lecture Notes in Computer Science, vol. 5977, pp. 319\u2013333. Springer (2010)","DOI":"10.1007\/978-3-642-11811-1_24"},{"key":"395_CR18","unstructured":"Koenig, D., Glover, A., King, P., Laforge, G., Skeet, J.: Groovy in action, vol. 91. Manning (2007)"},{"key":"395_CR19","unstructured":"Krings, S., Bendisposto, J., Leuschel, M.: Turning failure into proof: evaluating the prob disprover. In: Proceedings of the 1st International Workshop about Sets and Tools (2014)"},{"key":"395_CR20","unstructured":"Ladenberger, L.: BMotion Studio for ProB Project Website. http:\/\/stups.hhu.de\/ProB\/w\/BMotion_Studio , (May 2015)"},{"key":"395_CR21","doi-asserted-by":"crossref","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-Motion Studio. In: Proceedings FMICS\u20192009, LNCS 5825, pp. 202\u2013204. Verlag (2009)","DOI":"10.1007\/978-3-642-04570-7_17"},{"key":"395_CR22","doi-asserted-by":"crossref","unstructured":"Ladenberger, L., Dobrikov, I., Leuschel, M.: An approach for creating domain specific visualisations of csp models. In: Giannakopoulou, D., Salan, G. (eds.) HOFM 2014, LNCS (2014)","DOI":"10.1007\/978-3-319-15201-1_2"},{"key":"395_CR23","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W.J. (eds.) Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbr\u00fccken, Germany, October 3\u20136, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3725, pp. 162\u2013175. Springer (2005)","DOI":"10.1007\/11560548_14"},{"issue":"2","key":"395_CR24","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.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"395_CR25","unstructured":"Ligot, O., Bendisposto, J., Leuschel, M.: Debugging event-b models using the prob disprover plug-in. Proceedings AFADL 7 (2007)"},{"key":"395_CR26","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"11","author":"D Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9\u201321 (2010)","journal-title":"STTT"},{"key":"395_CR27","unstructured":"Roscoe, A.W., Hoare, C.A.R., Bird R.: The Theory and Practice of Concurrency. Prentice-Hall PTR, Upper Saddle River (1997)"},{"key":"395_CR28","unstructured":"Rubel, D., Wren, J., Clayberg, E.: The Eclipse Graphical Editing Framework (GEF). Addison-Wesley Professional (2011)"},{"key":"395_CR29","doi-asserted-by":"crossref","unstructured":"Butler, M., Savicks, Vitaly, Colley, J.: Co-simulation environment for rodin: landing gear case study. Communications in Computer Information Science, vol. 433. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_11"},{"key":"395_CR30","doi-asserted-by":"crossref","unstructured":"Silva, R., Butler, M.: Shared event composition\/decomposition in event-b. In: Aichernig, B.K., de\u00a0Boer, F.S., Bonsangue, M.M. (eds.) FMCO, Lecture Notes in Computer Science, vol. 6957, pp. 122\u2013141. Springer (2010)","DOI":"10.1007\/978-3-642-25271-6_7"},{"issue":"5","key":"395_CR31","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1002\/spe.1002","volume":"41","author":"R Silva","year":"2011","unstructured":"Silva, R., Pascal, C., Hoang, T\u00a0.S., Butler, M\u00a0.J.: Decomposition tool for event-b. Softw., Pract. Exp. 41(5), 199\u2013208 (2011)","journal-title":"Softw., Pract. Exp."},{"key":"395_CR32","doi-asserted-by":"crossref","unstructured":"Su, W., Abrial, J.-R.: Aircraft landing gear system: Approaches with event-b to the modeling of an industrial system. In: ABZ 2014: The Landing Gear Case Study, pp. 19\u201335. Springer (2014)","DOI":"10.1007\/978-3-319-07512-9_2"},{"key":"395_CR33","unstructured":"W3C CSS Working Group. Cascading Style Sheets (CSS) Snapshot 2010. http:\/\/www.w3.org\/TR\/css-2010\/ (2011)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0395-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0395-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0395-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0395-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T10:41:08Z","timestamp":1567075268000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0395-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,15]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["395"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0395-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,15]]}}}