Seminar Formal Methods 2009/2010 (2IF95)


Last update: 02-September-2009
Take your laptop with you to the first meeting!

Goal of this course

The aim of this course is to get you acquainted with the everyday practice of doing research in the Formal Methods area. Together, you will read scientific papers, give presentations about them, formulate research questions, try to solve them, and write down your results in a new paper intended to be submitted to a workshop or conference. Moreover, since the Formal Methods group distinguishes itself from other groups by placing an emphasis on mathematical correctness, it is likely that part of the work done in this seminar consists of designing formal definitions, formulating theorems about those definitions, and finally proving these theorems. The usual technical details about the course can be found on OWInfo. This website is intended for communicating things that come up during the course (like the overall planning).

This years research topic

Like the previous year, we have prepared a research topic to be studied during the course. Nevertheless, if you would like to study a topic of your own, feel free to propose such a topic during the first weeks of the seminar. Furthermore, if in the first meeting the group turns out to be too large, or too diverse, to focus on a single research subject, we will try to accommodate for this by preparing a second topic.

The Silent Step in Timed Process Algebra

The theoretical research question is an open question in the field of process algebra, that has been studied before by prof. Jos Baeten and other members of the FM group as well as the OAS group.

In timed process algebra, it turns out to be impossible to remove certain internal behavior from specifications of even the simplest communication protocols. This is due to the use of a very strong notion of equivalence, known as timed branching bisimulation, that allows the observation of the exact time at which an internal choice is made.

The aim of this seminar, is to find the strongest notion of equivalence that allows us to reduce specifications of simple communication protocols to simple representations of these protocols without unnecessary internal transitions. A successful notion of equivalence should furthermore be a congruence for the usual process algebraic operations.

We plan to approach this problem by studying literature, and consecutively try to reduce Fisher's protocol and the PAR protocol with axioms that we design for the purpose.

Literature

[1] A.S. Klusener. The Silent Step in Time In: W.R.Cleaveland (Eds.): CONCUR '92, Lecture Notes in Computer Science Vol. 630, pp 421-435, Springer Verlag (1992)
[2] J.C.M. Baeten, C.A. Middelburg, M.A. Reniers. A New Equivalence for Processes with Timing Technical Report CSR 02-10, Eindhoven University of Technology (2002)
[3] M.A. Reniers and M. van Weerdenburg. Action Abstraction in Timed Process Algebra: The Case for an Untimed Silent Step In: International Symposion on the Fundamentals of Software Engineering (FSEN), Lecture Notes in Computer Science, Vol. 4767, pp 287-301, Springer Verlag (2007)
[4] J.C.M. Baeten, J.A. Bergstra, and M.A. Reniers. Discrete Time Process Algebra with Silent Step In: Plotkin, Sterling and Tofte (Eds.): Proof, Language and Interaction, Essays in Honour of Robin Milner. p 535-569, The MIT Press (2000)

Planning, Preparation and Deliverables

Although research is often difficult to plan precisely, there is still some kind of structure to it. The planning below is what we think is going to happen in the foreseeable future.

The tentative research program

Week 36 --- Introduction to the Seminar
No deliverables
Week 37 --- The Silent Step in Time
One student/group prepares a lecture of fortyfive minutes
The other students/groups hand in a question about the paper at the start of the lecture
In the 2nd hour we give feedback on the lecture and discuss the questions that were handed in
Week 38 --- A New Equivalence for Processes with Timing
Same format as week 2
Week 39 --- Action Abstraction in Timed Process Algebra
Same format as week 2
Week 40 --- Re-evaluating Fisher's and the PAR protocol
Same format as week 2
Week 41 --- Discussion on different models of time, and observability therein
Week 42 --- Phrasing the research problem
Everyone summarizes for him/herself what has come up during the last weeks
During the lecture we get a clear picture of the problem we are going to work on
Furthermore, we make a planning for the remaining weeks
Week 43 --- Puzzling & Frustration
Week 44 --- EXAM WEEK.
Week 45 --- EXAM WEEK.
Week 46 --- More Puzzling & Frustration
Week 47 --- Eureka!
Week 48 --- (Tentative program due to IPA Herfstdagen)
Week 49 --- Disappointment at finding a mistake
Week 50 --- Starting from scratch
Week 51 --- Finally solving the problem
Week 52 --- CHRISTMAS BREAK
Week 53 --- NEW-YEAR BREAK
Week 1 --- Thinking you found a mistake
Week 2 --- Submitting our paper to a conference or workshop