_M_O_O_G_/2I1283
Formal Methods in Software Engineering
Techniques for precisely and unambiguously describing program behaviour and properties of programs are needed in many situations ranging from building software for which the cost of failure is unacceptably high to outsourcing situations, when code-farms in other time-zones are following remotely developed specifications and keeping the customer in the loop is hard or too expensive.
For precise specifications, graphical models like plain UML are not enough; it is hard to reason about a program's behaviour without making assumptions that need not hold true. To build systems that with high confidence behave in accordance with their specifications, we need formal methods -- methods for analysis, design and implementation with mathematical underpinnings.
The course deals with formal specification using formal modelling languages such as JML (Java Modelling Language) and OCL (Object Constaint Language), design by contract, and tools, checkers, IDE:s and programming languages that support such concepts.
Having successfully completeted the course, a student should have confidence in using formal languages for specifying programs or parts of programs and have the necessary knowledge to use and learn tools for using formal specification techniques in real-world projects.
Formal specification languages, writing precise requirements, formulating invariants, and using tools to support these processes.
Experience in OO modelling and some programming.
AGILE, DYPL, TEME, IOOR, CISS.
Written exam (2 credits), small project work (3 credits).
Not yet decided.