Abstract
We summarise our experiences in teaching two formal methods courses at Pontificia Universidad Javeriana. The first course is a JML-based software engineering course. The second course is a model-driven software engineering course realised in the B method for software development. We explain how formal methods are promoted in Pontificia Universidad Javeriana, how we motivate students to embrace formal methods techniques, and how they are promoted through the presentation of motivating examples.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Rodin deliverable D7, Event-B mathematical Language. In: Information Society Technologies, ch. V (2005)
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundam. Inf. 77(1-2), 1–28 (2007)
Abrial, J.R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Informatica 77(1,2), 1–24 (2007)
Bouquet, F., Dadeau, F., Julien, J.: JML2B: Checking JML specifications with B machines. In: The 7th International B Conference, pp. 285–288 (2007)
Breunesse, C., Catano, N., Huisman, M., Jacobs, B.: Formal methods for Smart Cards: An experience report. Science of Computer Programming 55(1–3), 53–80 (2005)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)
Catano, N., Barraza, F., García, D., Ortega, P., Rueda, C.: A case study in JML-assisted software development. In: Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008). ENTCS, July 2009, vol. 240, pp. 5–21 (2009)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML reference manual (2008), http://www.eecs.ucf.edu/~leavens/-JML/jmlrefman/jmlrefman_toc.html
Link, J.: Unit Testing in Java. Morgan Kaufmann, San Francisco (2003)
Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)
Meyer, B.: Object Oriented Software Construction. Prentice Hall PTR, Englewood Cliffs (1997)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI (November 2006)
Robinson, A., Voronkov, A.: Handbook of Automated Reasoning. MIT Press, Cambridge (2001)
Schneider, S.: The B-Method: An Introduction. Palgrave, Oxford (2001)
Spivey, J.M.: An introduction to Z and formal specifications. Software Engineering Journal 4(1), 40–50 (1989)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Inc., Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Catano, N., Rueda, C. (2009). Teaching Formal Methods for the Unconquered Territory. In: Gibbons, J., Oliveira, J.N. (eds) Teaching Formal Methods. TFM 2009. Lecture Notes in Computer Science, vol 5846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04912-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-04912-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04911-8
Online ISBN: 978-3-642-04912-5
eBook Packages: Computer ScienceComputer Science (R0)