FM 2008

Tutorials

The FM 2008 tutorial program aims to provide conference participants with the opportunity to learn new techniques and gain insights in a wide range of areas of formal methods. This year we have six tutorials, given by renowned experts in their fields.

A reduced fee will be offered to tutorial presenters. If the number of participants is less than 6, the accepted tutorial may be cancelled.

Inquiries should be directed to the Tutorial Chair, Marina Waldn (bo Akademi University).

Important Dates

Final tutorial notes:14 May 2008


Tutorial Schedule (26–27 May 2008)
 

Monday 26th

Computational Systems Biology (full day) (T1)
Ion Petre and Ralph-Johan Back

Teaching formal methods to students in high school and introductory university courses (full day) (T2)
Ralph-Johan Back

Event-B and the Rodin Platform (full day) (T3)
Jean-Raymond Abrial

Tuesday 27th

Why formal verification remains on the fringes of commercial development (full day) (T4)
Arvind

Morning session only

Formal Methods and Signal Processing (half day) (T5)
Raymond Boute

Afternoon session only

Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking (half day) (T6)
Ganesh Gopalakrishnan and Yu Yang

Formal modelling and analysis of real-time systems using UPPAAL (half day) (T7)
Paul Pettersson and Wang Yi (cancelled)

 

Computational Systems Biology (full day)
Ion Petre and Ralph-Johan Back
Åbo Akademi University, Turku, Finland

Biology is witnessing nowadays a transformation towards a more quantitative science, based on major technological breakthroughs in the past decade. In this transformation, biology is incorporating mathematical modeling techniques and computational approaches towards numerical simulations, model analysis, and predictions. Systems biology is perhaps the best example in this respect. A major effort here goes into understanding the biological functioning of the whole based on the well-understood function of its parts. The aim is to formalize and analyze the ever-changing inter-connections between components (often on different time and space scales), their influence on one another, regulatory patterns, alternative pathways, etc. This is a typical example of a branch of biology where formal reasoning rather than empirical observations is the main driving force.
 
The importance of biology as a new application area for applied mathematics and computer science has been recognized in our community. There are already significant contributions in this field from well-established computer science research groups (from the formal methods community see D.Harel, L.Cardelli, G.Plotkin, and others), as well as a number of international conferences and journals dedicated to the topic, having computer science as the main target community.

The main difficulties for a computer scientist entering this field are on one hand, the lack of a proper (if minimal) biological background and on the other hand, the lack of training in the mathematical and computational techniques most often used in this field. Through this one-day (6 hours) tutorial, we aim to give an introduction to computational systems biology, starting with a crash course on molecular biology for computer scientist, continuing with continuous and discrete modeling techniques, as well as formal methods-based modeling approaches. We also plan to give a computer tutorial on Copasi (Complex Pathway Simulator), a useful tool for modeling and simulating sysbio projects. Finally, we plan to give an overview of a well-rounded off sysbio project (on the heat shock response) that we have been working on in our groups for a couple of years now. We believe that this combination of basic notions and techniques, computer tutorial, and a well-defined complex research project should give our audience a valuable insight into the beauty and the challenges of systems biology. We also hope to give them an insight into the potential of their already existing computer science tools and techniques in this new application area.

 

Teaching formal methods to students in high school and introductory university courses (full day)
Ralph-Johan Back
Abo Akademi University, Turku, Finland

Formal methods are a standard ingredient in CS and SE university curriculum. However, the emphasis on using mathematical methods in building software systems is not always received very well by students, as the methods taught are often seen as overly complex and difficult to apply in practice. We have been working on this problem in our research lab, Learning and Reasoning (Abo Akademi and University of Turku) for a number of years now, and have developed new methods for teaching formal methods to novices that seem to work very well in practice. Novices are here students in high school and first year university students who encounter formal methods for the first time.

The course will focus on two main topics:

  • how to teach the systematic construction of mathematical proofs and derivations in high school and introductory university courses, and
  • how to teach the construction of correct programs for first year CS and SE students in university.

On the first topic, we describe how to use structured derivations for presenting mathematical proofs and derivations. Structured derivations are a further development of Dijkstra’s calculational proof style. The main extension is the use of nested derivations, which makes it possible to express arbitrary logical derivations in a rather natural fashion. We have adapted the structured derivation proof style to the mathematics curriculum in Finnish high schools, and carried out extensive case studies on the use of structured derivations in mathematics teaching. The experiences have been very good, showing that the use of structured derivations improves the performance of students in mathematics quite markedly. Structured derivations also provide a good formalism for computer supported and web based mathematics teaching, because the syntax of mathematical proofs is more explicit and therefore easier to construct, read and analyze.

The second topic is concerned with how to build programs that are correct by construction. The traditional approach is to either use a posteriori verification, where we first construct the program, identify the necessary pre- and postconditions and loop invariants, and then verify that the program is correct. Alternatively, we can use Dijkstra’s constructive approach, and build the program code and the proof hand in hand. In invariant based programming, we take Dijkstra’s approach to the extreme, by constructing pre- and postcondition as well as possible loop invariants before any code is written at all. The program is then verified in the usual way by proving the verification conditions (using structured derivations). Invariant based programming is supported by a new visual formalism, nested invariant diagrams. This approach, when supported by an appropriate work flow, seems to work quite well in practice, and allows the programmer to quickly identify errors in his program while he is constructing it, and in the end deliver a program that has been proved mathematically correct. We have taught invariant based programming to first year CS students with very good results. The students have learned how to construct correct programs in practice, and have expressed quite a strong appreciation of the method. We have also taught the approach to experienced programmers (some with prior knowledge of formal methods, some without), with similar good results.

Full version (PDF)

Programme

Material

 

Event-B and the Rodin Platform (full day)
Jean-Raymond Abrial

This tutorial is an introduction to the construction of complex systems using Event-B and the Rodin Platform.

Event-B is a mathematical formalism (based on first-order logic and set theory) used to develop formal models of discrete transition systems. These models are elaborated before effectively building these systems which are thus intended to be correct by construction.

Discrete transition system is the unifying paradigm which can be used in many different areas: sequential, distributed, concurrent, parallel. It also covers larger systems where one takes into account not only the future software but also its (fragile) environment.

Models are made of constants and variables related by possibly complex invariants. Their dynamics is defined by means of transitions (called events) made of guards (the enabling conditions) and actions (supposed to modify variables in parallel).

Models are developed by means of successive refinements steps: from quite simple and abstract to very concrete. When a model becomes too complicated, it can be decomposed into smaller ones communicating in a systematic fashion.

Proofs and model-checking are performed at each step of the development. They insure that each model is coherent and that it indeed refines its abstraction (if any).

The Rodin Platform is the tool set which has been developed (as funded by the European Project Rodin) to ensure a mechanical aid to the user of this approach. This platform is open source and implemented on Eclipse. It works on Windows, Linux and Mac-OS. It contains a database suppoert which contains the developed models. This database is surrounded by various plugins: provers, model-checkers, animators, UML transformers, etc. New plugins can be added.

The intent of the tutorial is to explain all this in greater details by means of various practical examples and tool demonstrations.

Full version (PDF)

Slide: Introduction (PDF)
Slide: A Mechanical Press Controller (PDF)
Slide: The Bounded Re-transmission Protocol (PDF)
Slide: Reference Card (PDF)
Slide: Summary of Mathematical Notation (PDF)

 

Formal Methods and Signal Processing (half day)
Raymond Boute
INTEC–Ghent University

Motivation  Signal Processing (SP) is an ideal discipline to combine with Formal Methods (FM). Benefits are mutual: using FM techniques in SP, and using SP as a foothold for broadening FM into a general engineering discipline.
   SP is ideal as a target area because it is one of the traditionally more mathematics-intensive disciplines and mathematical modeling is routine engineering practice (a role model for software engineering!). Still, defective formulations have been noted by SP professionals [references in full version], where FM can provide fully defect-free conventions ``letting the symbols do the work''. Moreover, SP has broadened from analog models to including multidimensional information and algorithms implemented in software, where modeling is weak and FM can also help. Conversely, Parnas's observations from nearly two decades ago are even more relevant today: CS students often end up doing engineering jobs where a strong signals and systems background is necessary. Combination with FM provides significant synergy.

Overview  A unifying formalism (Functional Mathematics) is presented that avoids all defects of the traditional conventions while still maintaining the familiar “look and feel” of the formulas. It supports the same calculational style of reasoning in differential/integral calculus, formal logic, theories of signals and systems, algorithms and software. The two main components are:
   (i) an algebra of generic functionals, originally designed for structuring signals and systems, but equally useful in formal logic and modeling software;
   (ii) a functional predicate calculus that allows engineers to calculate as fluently with quantifiers as they have learned to do with derivatives and integrals, and hence opens the door to modeling programs mathematically.
   Throughout, examples show the unification between “continuous” SP models for signals and systems and “discrete” FM models for computers and software.

Full version (PDF)

 

Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking (half day)
Ganesh Gopalakrishnan and Yu Yang
School of Computing, University of Utah, Salt Lake City, UT 84112, U.S.A.

Conventional testing methods are inadequate for debugging multithreaded C programs because many “unexpected” thread interactions can only be manifested through very low probability event sequences that are easily missed during test creation. As a result, bugs can escape into the field, and often manifest years after code deployment. While the approach of building formal models in modeling languages such as Promela followed by model checking using tools such as SPIN has been shown to be effective for verification, the burden of model extraction makes this approach inapplicable in general software development. Runtime model checking – first implemented in the Verisoft tool – can help solve this problem by running the actual code under the control of a scheduling mechanism, and detecting violations of assertions (typically deadlocks and other safety properties).

It is well recognized that when interleaving thread actions, one must prevent the interleaving of independent actions to avoid state explosion. Static partial order reduction methods achieve this objective by a priori (through static criteria) determining persistent sets (which are a subset of actions enabled at any given state) and only interleaving actions within persistent sets. This method is ineffective in the face of information that is difficult to compute statically. For instance, given the actions of two threads a[e1] and a[e2] that are simultaneously enabled, unless one can determine whether e1==e2, it is not possible to tell whether the actions commute. The dynamic partial order reduction (DPOR) approach of Flanagan and Godefroid avoids this difficulty by taking advantage of the known values of expressions and pointer references (in the above example checking whether e1==e2 at runtime) to dramatically cut down the number of interleavings examined. It has been shown to be very effective in detecting safety violations and deadlocks by systematically exploring all relevant interleavings of the multithreaded programs under specific inputs (meaning, specific external input drivers).

Full version (PDF)

Material

 

Why formal verification remains on the fringes of commercial development (full day)
Arvind
CSAIL, MIT

There are dozens of papers and theses on successful verification of cache-coherence protocols and out-of-order processors. Yet this formal verification has little impact on the design of actual chips embodying these functionalities. Formal verification does not seem to reduce the need for ad hoc verification and testing of designs before fabrication. We will give reasons for this persistent “gap” and offer a possible solution.

Full version (PDF)