People

The course assistants Ramona and Bart offer scheduled office hours to help you with questions:

• Ramona (room 6120), Monday, 10:00 - 11:30
• Bart (room 5483), Wednesday, 10:00 - 11:30

If you have any general questions regarding the course, please post in our google group. This will reach all teachers and your fellow students. This way, there can be an exchange of questions, hints, and discussions among all of us. Please make use of this forum. If you are not yet a member of the group, you have to

• get a google account, and
• request an invitation to the sefm group,
• provide your personnumber and a valid Chalmers or Gothenburg University address when applying for an invitation. This is necessary to identify you as a participant of the course.

All kinds of questions (and answers) on the content of the course are welcome. (But don't post lab solutions!)

Examination

• pass all Lab assignments, and
• pass the regular end-of-course-exam.

Two courses in one

The course is available both for Chalmers students and for GU students.

• TDA293 Software Engineering using Formal Methods at Chalmers. Grades are on the scale U, 3, 4, 5.
• DIT270 Software Engineering using Formal Methods at GU. Grades are on the scale U, G, VG.

Schedule

The workload for an average student is expected to be around 200h, evenly distributed over the 8 week course period that means around 25h/week. From these 25h/week only 6h/week are scheduled and 19h/week are your own responsibility.

The lectures are held in room EA and the exercises in room EB Please check Lectures and Schedule for directions.

Course Content

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigor. The purpose is to construct, with high confidence, systems that behave according to their specification. The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool.

On the model checking side, the advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. Accordingly, we concentrate on the verification of safety properties. The lectures cover the following topics:

• Theoretical foundations of model checking.
• Property languages and their usage.
• Performing automated verification with a software model checking tool.

For the deductive verification side, we use KeY, an integrated tool for the formal specification and verification of Java programs. The tool, which is partly developed at Chalmers and Gothenburg University, supports formal specification in the Java Modeling Language (JML), and translation from JML into logic. An interactive theorem prover is used to formally verify statements about specifications and programs. The lectures cover the following topics:

• Java Modeling Language (JML)
• Formal Semantics of Systems
• Predicate Logic for Specification of Java Programs
• Translating JML into Dynamic Logic
• Verifying Proof Obligations

Familiarity with Java is encouraged.

After successful completion of the course you will:

• be able to express safety properties of (concurrent) programs in a formal way.
• have understood the theoretical foundations of verifying safety properties via model checking.
• Be able to use tools which integrate and automate the model checking of safety properties.
• be able to write formal specifications of object-oriented system units. Understanding the concepts of method contract, class invariant, and behavioural subtyping.
• have understood how the connection between programs and formal specifications can be represented in a program logic. Understand the difference between syntax, semantics, and calculus in connection with logic-based systems.
• be able to verify functional properties of simple Java programs with a verification tool.

Literature

For the first part we use the book Principles of the Spin Model Checker, mostly Chapters 1-5. A more thorough and theoretical treatment of the material can be found in The SPIN Model Checker, but this is not required reading.

For the second part, there is a book on the KeY system called Verification of Object-Oriented Software: The KeY Approach. You can access the online version from a Chalmers account. Chapter 1 in the book gives a general introduction in the philosophy behind KeY. In Chapter 10 gives many useful tips on practical usage.