IPA Course Formal Methods 2008

23 - 27 June 2008
Technische Universiteit Eindhoven

IPA organises courses on each of its major research fields, Algorithms and Complexity, Formal Methods and Software Technology. These three IPA Courses intend to give an overview of (part of) the research of IPA in this specific field. They are organised in a cycle of two years, and form a mandatory element in the education plan of IPA PhD-students (every student should attend at least two out of the three IPA courses).

The Formal Methods Course, which is hosted by IPA at the Technische Universiteit Eindhoven focusses on five main areas of Formal Methods research. One course day will be dedicated to each of these areas, in which lectures are combined with hands-on tool training. More information on the course program will become available through this page. The program for this edition of the course was composed by Jaco van de Pol (UT).

Dates and Locations

The overall schedule of the course is as follows, course days will last from approximately 10.00 to 17.00 hours.

Monday 23 June room HG 6.01 Introduction Jaco van de Pol (UT)
Timed Automata & UPPAAL Frits Vaandrager (RU)
Tuesday 24 June room HG 6.01 Model Checking with SPIN Theo C. Ruys (UT)
Wednesday 25 June room HG 6.01 Theorem Proving & PVS Erik Poll (RU)
Thursday 26 June room HG 6.01 Behavioural Analysis using mCRL2 Aad Mathijssen et al. (TU/e)
Friday 27 June room HG 6.01 Graph Transformations & GROOVE Arend Rensink (UT)

A more precise time table will be made available as soon as possible. Unlike the Herfstdagen and Lentedagen, overnight accomodation is not "built in" for this course. The schedule is set up in such a way that it is feasible for many students to travel back and forth to Eindhoven during the week. In cases where this is not feasible, we will provide basic overnight accomodation. You can specify your accomodation needs on the registration form.

The venue for the course is the main building ("hoofdgebouw") of the Technische Universiteit Eindhoven, marked "HG" on the campus map. The TU/e campus is only a few minutes walk from Eindhoven Central Station. After arriving at the station, take the stairs down from the platform and turn to your right. Exit the station on the north side (buss station) to the main road. Enter the diagonal walk way to your right. At the end you will come to a crossing with a main road, guarded by traffic lights. The entrance to the campus is across the main road. Follow this footpath along the circular building till the end. You are now on a square with the main building in front of you and a green glass building to your right. Enter the main building through the main (south side) entrance, and take the elevator to the floor indicated by the first digit of the room numbers above, i.e floor 6. Room 6.01, a.k.a. the "WIN zaal" is the first room to your left when you leave the elevator.

Course Material

Course material will be handed out during the course. Where possible, this material will be made available for downloading via this page.

Costs

The courses are directed towards IPA PhD. students, giving them an overview of IPA's research. For them participation is free (including overnight accommodation if necessary). Other IPA-members can attend if there is capacity left, and the same holds for members of associated research schools. For these categories we will charge costs for the course material, lunches, etc (and we will not provide overnight accomodation). Costs for these participants will be specified here as soon as possible.

Registration

You can register for the course using the online registration form (when you require overnight accommodation, you can specify your needs in the Remarks box). The deadline for registration is Monday 16 June


CONTENT DETAILS


Introduction to Formal Methods

Jaco van de Pol (UT)

Monday June 23

Formal methods are rigorous mathematical techniques, to specify and analyse computer systems. Different aspects of computer systems are considered, for instance structure, behaviour, timing, dependability, etc. Also, formal methods can be applied in different phases of the development cycle, such as requirements, design, coding, or testing. An overview will be given of various methods, and their applicability to different system aspects during the system development cycle. At the same time, this is an introduction of the other lectures that follow in this Formal Methods course.

Schedule

10.00 - 11.00 Lecture

11.00 - 11.15 Break

Timed Automata & UPPAAL

Frits Vaandrager (RU)

Monday June 23

This tutorial will present the tool UPPAAL (see www.uppaal.com) focusing on the application of this tool to solve verification problems. UPPAAL is a tool for modelling, simulating and verifying real-time systems. The modelling language is based on timed automata allowing system behaviour to be described as a networks of timed automata extended with data variables which may be manipulated by a rich C-like programming language. The verification engine of UPPAAL supports both safety, liveness and bounded liveness properties. In the tutorial we will review the notion of zones and their efficient representation and manipulation for the analysis of timed automata models using difference bounded matrices.

The tutorial will also include a demo of the tool and lab sessions during which the participants tackle various verification questions using Uppaal.

Schedule

11.15 Tutorial on Uppaal

12.15 Lunch

13.15 Lab session:

14.30 Coffee

14.45 Biphase mark case study

15.15 Lab session:

16.30 End

Model checking with SPIN

Theo C. Ruys (UT)

Tuesday June 24

This course day surveys model checking of linear temporal logic (LTL). Model checking is a prominent formal verification technique for assessing functional properties of software and communication systems. Model checking requires a model of the system under consideration and a desired property (often formulated in LTL) and then systematically checks whether or not the given model satisfies this property. Typical properties such as deadlock freedom, invariants, and request-response can be checked. Model checking is an automated technique to check the absence of errors (i.e., property violations) and alternatively can be considered as an intelligent and effective debugging technique to find bugs.

The course provides some basic theoretical background of (LTL) model checking and introduces the well-known model checker SPIN together with its modeling language Promela.

Schedule

10.00 - 11.00 Lecture 1: Model Checking and LTL

11.00 - 11.15 Break

11.15 - 11.45 Exercises 1: LTL

11.45 - 12.15 Lecture 2: Introduction to SPIN

12.15 - 13.15 Lunch

13.15 - 14.00 Lecture 3: Using SPIN

14.00 - 14.30 Exercises 2: Hands-on with SPIN

14:30 - 14.45 Break

14:45 - 15.30 Exercises 2 (continued)

15.30 - 15.45 Break

15.45 - 16.15 Lecture 4: Advanced SPIN

Theorem Proving & PVS

Erik Poll (RU)

Wednesday June 25

This course day gives an introduction to interactive theorem proving using the theorem prover PVS. We introduce the PVS specification language, illustrate how it can be used to model concepts and problems from computer science, and show how the associated theorem prover can then be used to reason about these models.

Most of the day will be taken up with practical exercises on using PVS, first on some toy logical problems and then on more interesting computer science problems. If there is time, we will end the day by showing some serious applications of theorem proving, for Java program verification.

Schedule

10.00 - 11.00 Lecture 1: Introduction to PVS

11.00 - 11.15 Break

11.15 - 12.00 Exercises 1

12.00 - 12.15 Discussion of exercises 1

12.15 - 13.15 Lunch

13.15 - 13.45 Lecture 2: Case study - state machines in PVS

13.45 - 14.15 Exercises 2

14.15 - 14.30 Break

14.30 - 15.15 Exercises 2

15.15 - 15.30 Discussion of excercises 2

15.30 - 15.45 Break

15.45 - 16.15 Wrap-up: Example applications of PVS

Behavioural Analysis using mCRL2

Aad Mathijssen, Bas Ploeger, Tim Willemse, Frank Stappers (TU/e)

Thursday June 26

In a typical distributed system, a number of components are running simultaneously in parallel. By working together, these components provide the functionalities that are required from the complete system. Although the behaviour of a single component can usually be specified and analysed relatively easily, the behaviour of the system as a whole is often too complex to be specified or analysed thoroughly. This is primarily due to (and inherent to) the parallelism between the system's components. An exhaustive analysis of all of the system's states and execution paths thus becomes a formidable task - even for a system with a relatively small number of components.

In this part of the course, we introduce and explain process algebra, which is a formalism that is well suited for the specification of system behaviour. This is done within the context of the mCRL2 specification language and toolset. With the toolset, users can specify the behaviour of a distributed system and analyse it using automated techniques.

Teaching materials

Slides for the day.

Schedule

10:00 - 10:30 Basic Process algebra

10:20 - 10:45 Parallellism and abstraction

10:45 - 11:00 Processes with data

11:00 - 11:15 Break

11:15 - 11:35 Linear processes

11:35 - 12:00 Temporal logic

12:00 - 12:15 Verification

12:15 - 13:15 Lunch

13:15 - 13:45 Toolset overview and demo

13:45 - 14:15 Hands-on experience

14:15 - 14:30 Break

14:30 - 15:30 Hands-on experience

15:30 - 15:45 Break

15:45 - 16:00 Wrap-up

16:00 - 16:15 Industrial case studies

Graph Transformation & GROOVE

Arend Rensink (UT)

Friday June 27

During this day, the participants will get an introduction into graph transformation and become acquainted with a particular tool, GROOVE, for executing graph transformation systems en generating the resulting state spaces.

Graph transformation is a formalism which specifies changes in arbitrary graph-shaped models by encoding, in rules, local changes to be made to the graphs, in terms of deletions and additions. Moreover, the application conditions for such rules can also be directly encoded. This makes the formalism particularly suitable for describing the dynamics of, for instance, object-oriented programs (where the graphs represent the heap and stack structure).

GROOVE is a tool developed at the University of Twente which implements a particular brand of graph transformation. It has as a distinguishing feature that it systematically and efficiently generates the state space resulting from the repeated application of rules to a given start graph, while at the same time collapsing the graphs modulo isomorphism. There is a CTL model checking back-end included.

Schedule

10:00 11:00 Introduction

11:00 12:00 Exercises

12:00 13:00 Lunch

13:00 13:30 Foundations

13:30 14:00 Extension: Attributes

14:00 15:00 Exercises

15:00 15:30 Extension: Quantification

15:30 16:30 Exercises

16:30 - 16:45 Wrap-up