Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z

ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z pp 167–182Cite as

Using B and ProB for Data Validation Projects

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9675))

Abstract

Constraint satisfaction and data validation problems can be expressed very elegantly in state-based formal methods such as B. However, is B suited for developing larger applications and are there existing tools that scale for these projects? In this paper, we present our experiences on two real-world data validation projects from different domains which are based on the B language and use ProB as the central validation tool. The first project is the validation of university timetables, and the second project is the validation of railway topologies. Based on these two projects, we present a general structure of a data validation project in B and outline common challenges along with various solutions. We also discuss possible evolutions of the B language to make it (even) more suitable for such projects.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://www.data-validation.fr.

  2. 2.

    In addition, the types of the arguments have to be provided for \(\mathrm{prj_{1}}\) and \(\mathrm{prj_{2}}\); e.g., \(\mathrm{prj_{2}}((COURSE \times SEMESTER) \times WEEKDAY, {\mathbb {Z}})(v)\).

  3. 3.

    ProB can compute in 0.18 s, despite there being 15!=1,307,674,368,000 permutations.

  4. 4.

    In many models, the variant actually corresponds exactly to the number of iterations.

  5. 5.

    https://www3.hhu.de/stups/prob/index.php/ProB_Java_API.

References

  1. Abelson, H., Sussman, G.J.: Structure and Interpretation of Computer Programs, 2nd edn. MIT Press, Cambridge (1996)

    MATH  Google Scholar 

  2. Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221–236. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  3. Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  4. 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–129. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  5. 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–354. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. In: Proceedings of DS-Event-B 2012, Kyoto. CoRR, abs/1210.7039 (2012)

    Google Scholar 

  7. Clements, P., Northrop, L.M.: Software Product Lines: Practices and Patterns. Addison-Wesley Longman Publishing Co. Inc, Boston (2001)

    Google Scholar 

  8. Corne, D., Ross, P., Fang, H.-L.: Evolving timetables. In: Practical Handbook of Genetic Algorithms: Applications, vol. 1, pp. 219–276 (1995)

    Google Scholar 

  9. Deris, S., Omatu, S., Ohta, H.: Timetable planning using the constraint-based reasoning. Comput. Oper. Res. 27(9), 819–840 (2000)

    Article  MATH  Google Scholar 

  10. Gotlieb, C.C.: The construction of class-teacher time-tables. In: IFIP Congress, pp. 73–77 (1962). http://dblp.uni-trier.de/rec/bib/conf/ifip/Gotlieb62, http://dblp.org

  11. Hayes, I.J., Jones, C.B., Nicholls, J.E.: Understanding the differences between VDM and Z. ACM SIGSOFT Softw. Eng. Notes 19(3), 75–81 (1994)

    Article  Google Scholar 

  12. Herman, D., Wand, M.: A theory of hygienic macros. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 48–62. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)

    Google Scholar 

  14. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. 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–446 (2014)

    Google Scholar 

  17. 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–874. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Leuschel, M., Cansell, D., Butler, M.: Validating and animating higher-order recursive functions in B. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 78–92. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. 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–723. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. 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–116. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  21. Milicevic, A., Efrati, I., Jackson, D.: \(\alpha \)Rby—An embedding of Alloy in Ruby. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 56–71. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  22. Rudová, H., Murray, K.: University course timetabling with soft constraints. In: Burke, E.K., De Causmaecker, P. (eds.) PATAT 2002. LNCS, vol. 2740, pp. 310–328. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  23. Schimmelpfeng, K., Helber, S.: Application of a real-world university-course timetabling model solved by integer programming. OR Spectr. 29(4), 783–803 (2006)

    Article  MATH  Google Scholar 

  24. Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487–495. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

Download references

Acknowledgements

We would like to thank Luis-Fernando Mejia from Alstom for pushing (and funding) B and ProB into new directions. We have also grateful to ClearSy and Systerel for exercising ProB, allowing us to discover new aspects of the B language. We are grateful to Thales for funding a collaborative research project and to the Thales team, in particular Nader Nayeri, for all their help and insights. Finally we would like to thank Frank Meier, Tobias Witt, Philip Höfges and the planning teams at the Faculty of Arts and Humanities and the Faculty of Business Administration and Economics at Heinrich Heine University for their contributions to the curriculum validation project.

Author information

Authors and Affiliations

  1. Institut Für Informatik, Heinrich-Heine-Universität Düsseldorf, Universitätsstr. 1, 40225, Düsseldorf, Germany

    Dominik Hansen, David Schneider & Michael Leuschel

Authors
  1. Dominik Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Leuschel .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Software Competence Center, Hagenberg, Austria

    Klaus-Dieter Schewe

  3. Software Competence Center, Hagenberg, Austria

    Atif Mashkoor

  4. Software Competence Center, Hagenberg, Austria

    Miklos Biro

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Hansen, D., Schneider, D., Leuschel, M. (2016). Using B and ProB for Data Validation Projects. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33600-8_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33599-5

  • Online ISBN: 978-3-319-33600-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation