Formal Methods in Software Engineering (Version 0.2)
This course is an introduction to Model-Based Analysis and Testing techniques. We will experiment with real tools as well as learn the underlying theory. Therefore, some of the lectures will be hands-on labs and rather informal, while others will be more conventional lectures, dry and without any sense of humor.
- Lectures / Labs:
- Wednesdays 16:15, Liivi 2-611.
- Fridays 14:15, Liivi 2-611.
- Instructors:
- Vesal Vojdani (vesal@ut.ee)
- Kalmer Apinis (might still make it)
List of Topics
The following techniques and tools could be covered. You may still vote in moodle about which topics should be covered. The underlying theory will be introduced in a demand-driven fashion. Since the theory is a lot of fun in and of itself, we have to space things out to keep you motivated to hear all this practical stuff:
- Design-by-Contract (Contracts for Java)
- Verification of Object-Oriented Programs (KeY)
- Model Checking (SPIN)
- Software Model Checking (Java PathFinder)
- Symbolic Execution for Test Generation (Symbolic PathFinder)
- Model-Based Test Generation (ModelJUnit)
- Static Analysis of Concurrent Systems (Goblint)
More broadly, the essence of this course is best expressed by a famous quotation from the father of Social Psychology, Kurt Lewin: "There is nothing more practical than a good theory."
Acknowledgements
The preparation of this course was partially supported by the EU ARTEMIS Joint Undertaking under grant agreement n° 269335 (MBAT: Combined Model-based Analysis and Testing of Embedded Systems) and the German Research Foundation (DFG).
