{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T04:28:51Z","timestamp":1770352131789,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319335995","type":"print"},{"value":"9783319336008","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_10","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T08:15:15Z","timestamp":1462868115000},"page":"167-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Using B and ProB for Data Validation Projects"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Hansen","sequence":"first","affiliation":[]},{"given":"David","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"10_CR1","volume-title":"Structure and Interpretation of Computer Programs","author":"H Abelson","year":"1996","unstructured":"Abelson, H., Sussman, G.J.: Structure and Interpretation of Computer Programs, 2nd edn. MIT Press, Cambridge (1996)","edition":"2"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-319-05032-4_17","volume-title":"Software Engineering and Formal Methods","author":"R Abo","year":"2014","unstructured":"Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221\u2013236. Springer, Heidelberg (2014)"},{"key":"10_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-662-43652-3_10","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"RB Ayed","year":"2014","unstructured":"Ayed, R.B., Collart-Dutilleul, S., Bon, P., Idani, A., Ledru, Y.: B formal validation of ERTMS\/ETCS railway operating rules. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 124\u2013129. Springer, Heidelberg (2014)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: roissy VAL. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334\u2013354. Springer, Heidelberg (2005)"},{"key":"10_CR6","unstructured":"Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. In: Proceedings of DS-Event-B 2012, Kyoto. CoRR, abs\/1210.7039 (2012)"},{"key":"10_CR7","volume-title":"Software Product Lines: Practices and Patterns","author":"P Clements","year":"2001","unstructured":"Clements, P., Northrop, L.M.: Software Product Lines: Practices and Patterns. Addison-Wesley Longman Publishing Co. Inc, Boston (2001)"},{"key":"10_CR8","unstructured":"Corne, D., Ross, P., Fang, H.-L.: Evolving timetables. In: Practical Handbook of Genetic Algorithms: Applications, vol. 1, pp. 219\u2013276 (1995)"},{"issue":"9","key":"10_CR9","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1016\/S0305-0548(99)00051-9","volume":"27","author":"S Deris","year":"2000","unstructured":"Deris, S., Omatu, S., Ohta, H.: Timetable planning using the constraint-based reasoning. Comput. Oper. Res. 27(9), 819\u2013840 (2000)","journal-title":"Comput. Oper. Res."},{"key":"10_CR10","unstructured":"Gotlieb, C.C.: The construction of class-teacher time-tables. In: IFIP Congress, pp. 73\u201377 (1962). http:\/\/dblp.uni-trier.de\/rec\/bib\/conf\/ifip\/Gotlieb62 , http:\/\/dblp.org"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/182824.182843","volume":"19","author":"IJ Hayes","year":"1994","unstructured":"Hayes, I.J., Jones, C.B., Nicholls, J.E.: Understanding the differences between VDM and Z. ACM SIGSOFT Softw. Eng. Notes 19(3), 75\u201381 (1994)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78739-6_4","volume-title":"Programming Languages and Systems","author":"D Herman","year":"2008","unstructured":"Herman, D., Wand, M.: A theory of hygienic macros. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 48\u201362. Springer, Heidelberg (2008)"},{"key":"10_CR13","volume-title":"Software Abstractions: Logic, Language, and Analysis.","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"10_CR14","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"10_CR15","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. In: Proceedings of DS-Event-B 2012, Kyoto. CoRR, abs\/1210.6815 (2012)"},{"key":"10_CR16","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/9781119002727.ch14","volume-title":"Formal Methods Applied to Complex Systems","author":"Michael Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animationto data validation: the ProB constraint solver 10 years on. In: Formal Methods Applied to Complex Systems, pp. 427\u2013446 (2014)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-11447-2_6","volume-title":"Rigorous Methods for Software Construction and Analysis","author":"M Leuschel","year":"2009","unstructured":"Leuschel, M., Cansell, D., Butler, M.: Validating and animating higher-order recursive functions in B. In: Abrial, J.-R., Gl\u00e4sser, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 78\u201392. Springer, Heidelberg (2009)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/978-3-642-05089-3_45","volume-title":"FM 2009: Formal Methods","author":"M Leuschel","year":"2009","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 708\u2013723. Springer, Heidelberg (2009)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-662-43652-3_8","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Schneider, D.: Towards B as a high-level constraint modelling language. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 101\u2013116. Springer, Heidelberg (2014)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-662-43652-3_5","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Milicevic","year":"2014","unstructured":"Milicevic, A., Efrati, I., Jackson, D.: $$\\alpha $$ \u03b1 Rby\u2014An embedding of Alloy in Ruby. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 56\u201371. Springer, Heidelberg (2014)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-540-45157-0_21","volume-title":"Practice and Theory of Automated Timetabling IV","author":"H Rudov\u00e1","year":"2003","unstructured":"Rudov\u00e1, H., Murray, K.: University course timetabling with soft constraints. In: Burke, E.K., De Causmaecker, P. (eds.) PATAT 2002. LNCS, vol. 2740, pp. 310\u2013328. Springer, Heidelberg (2003)"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1007\/s00291-006-0074-z","volume":"29","author":"K Schimmelpfeng","year":"2006","unstructured":"Schimmelpfeng, K., Helber, S.: Application of a real-world university-course timetabling model solved by integer programming. OR Spectr. 29(4), 783\u2013803 (2006)","journal-title":"OR Spectr."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-19249-9_30","volume-title":"FM 2015: Formal Methods","author":"D Schneider","year":"2015","unstructured":"Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487\u2013495. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33600-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,16]],"date-time":"2024-06-16T08:58:32Z","timestamp":1718528312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"11 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}