Skip to main content
SpringerLink
Log in

Model-Based Problem Solving for University Timetable Validation and Improvement

  • Conference paper
FM 2015: Formal Methods (FM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9109))

Included in the following conference series:

Abstract

Constraint satisfaction problems can be expressed very elegantly in state-based formal methods such as B. However, can such specifications be directly used for solving real-life problems? We will try and answer this question in the present paper with regard to the university timetabling problem. We report on an ongoing project to build a formal model-based curriculum timetable validation tool where we use a formal specification as the basis to validate timetables from a student’s perspective and to support incremental modification of timetables. In this article we focus on expressing the problem domain, the formalization in B and our approach to execute the formal model in a production system using ProB.

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

Access this chapter

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asín Achá, R., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71–91 (2012)

    Article  Google Scholar 

  2. Abrial, J.-R.: The B-Book. Assigning Programs to Meanings. Cambridge University Press (November 2005)

    Google Scholar 

  3. Banbara, M., Soh, T., Tamura, N., Inoue, K., Schaub, T.: Answer Set Programming as a Modeling Language for Course Timetabling. Theory and Practice of Logic Programming 13(4-5), 783–798 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bendisposto, J., Clark, J., Dobrikov, I., Krner, P., Krings, S., Ladenberger, L., Leuschel, M., Plagge, D.: ProB 2.0 Tutorial. In: Proceedings of the 4th Rodin User and Developer Workshop. TUCS Lecture Notes. TUCS (2013)

    Google Scholar 

  5. Carlsson, M., Ottosson, G.: An Open-Ended Finite Domain Constraint Solver. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  6. Cooper, T.B., Kingston, J.H.: The complexity of timetable construction problems. In: Burke, E.K., Ross, P. (eds.) PATAT 1995. LNCS, vol. 1153, pp. 281–295. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  7. Corne, D., Ross, P., Fang, H.: Evolving Timetables. Practical Handbook of Genetic Algorithms: Applications 1, 219–276 (1995)

    Google Scholar 

  8. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194–207. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Deris, S., Omatu, S., Ohta, H.: Timetable planning using the constraint-based reasoning. Computers & Operations Research 27(9), 819–840 (2000)

    Article  MATH  Google Scholar 

  11. Di Gaspero, L., McCollum, B., Schaerf, A.: The Second International Timetabling Competition (ITC-2007): Curriculum-based Course Timetabling (Track 3). In: Proceedings of the 14th RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, Rome (2007)

    Google Scholar 

  12. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: An extensible ASM execution engine. Fundam. Inform. 77(1-2), 71–103 (2007)

    MATH  Google Scholar 

  14. Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11, 256–290 (2002)

    Article  Google Scholar 

  15. Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. The Journal of Logic Programming 19(20), 503–581 (1994)

    Article  MathSciNet  Google Scholar 

  16. Lach, G., Lübbecke, M.E.: Curriculum based course timetabling: new solutions to Udine benchmark instances. Annals of Operations Research 194(1), 255–272 (2010)

    Article  Google Scholar 

  17. 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 

  18. Lewis, R.: A survey of metaheuristic-based techniques for University Timetabling problems. OR Spectrum 30(1), 167–190 (2008)

    Article  MATH  Google Scholar 

  19. Métayer, C.: AnimB 0.1.1 (2010), http://wiki.event-b.org/index.php/AnimB

  20. Müller, T., Rudová, H.: Real-life Curriculum-based Timetabling. PATAT (June 2012)

    Google Scholar 

  21. Müller, T., Rudová, H.: Real-life curriculum-based timetabling with elective courses and course sections. Annals of Operations Research, 1–18 (June 2014)

    Google Scholar 

  22. Plagge, D., Leuschel, M.: Validating B, Z and TLA  +  using proB and kodkod. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372–386. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Post, G., Di Gaspero, L., Kingston, J.H., McCollum, B.: The Third International Timetabling Competition. Annals of Operations Research (February 2013)

    Google Scholar 

  24. 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 

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

    Article  Google Scholar 

  26. Shapiro, S.C.: The Jobs Puzzle: A Challenge for Logical Expressibility and Automated Reasoning. In: AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (2011)

    Google Scholar 

  27. Torlak, E., Chang, F.S., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326–341. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA +  specifications. In: Pierre, L., Kropf, T. (eds.) Proceedings CHARME’99, pp. 54–66. Springer, Heidelberg (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Heinrich Heine University, Düsseldorf, Germany

    David Schneider, Michael Leuschel & Tobias Witt

Authors
  1. David Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tobias Witt
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Schneider .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Nikolaj Bjørner

  2. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

    Frank de Boer

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Schneider, D., Leuschel, M., Witt, T. (2015). Model-Based Problem Solving for University Timetable Validation and Improvement. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19249-9_30

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19248-2

  • Online ISBN: 978-3-319-19249-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation