Lab Rationale

The lab sheet has been designed following the spirit of the paper:

Teaching Formal Methods for Software Engineering – Ten Principles Antonio Cerone, Markus Roggenbach, Bernd-Holger Schlingloff, Gerardo Schneider, and Siraj Ahmed Shaikh https://www.informaticadidactica.de/uploads/Artikel/Schlinghoff2015/Schlinghoff2015.pdf

It strives to realise a number of the principles stated in this paper, including

• Principle 6: Formal Methods need lab classes – create a stable platform

• Principle 7: Formal Methods are best taught by examples – choose from a domain familiar to the target group

• Principle 10: Formal Methods are fun – shout it out loud!

Didactically, the lab shall provide the students with the experience that they are capable of successfully addressing a problem with a formal methods tool. Differentiation between students in terms of marks is not an objective. A student who engages with the lab ought to be able to complete tasks 1, 2 and 3. Only task 4 is slightly challenging and might not be accessible to everyone.

Economically, the lab should be “self-running” in the sense that students can follow the lab sheet without requiring much extra tutoring.

The lab has been successfully tried in a 2nd year, undergraduate module on Software Engineering. This unit comprised of

• two lectures (1 hr each): introducing Ladder Logic verification
• one 2 hr lab: hands-on experience
• two lectures (1 hr each): placing Ladder Logic verification into the field of formal methods

The idea behind this teaching approach is: let’s first experience a formal method, and only then see what else is there in the field.