The IPA Lentedagen are an annual multi-day event, dedicated to a specific theme of current interest to the research community of IPA. This year's Lentedagen are dedicated to the integration of formal methods.

Formal methods (languages, tools, and techniques for the analysis and design of systems, with a sound, mathematical basis) come in many different flavors. One reason why this abundance of approaches persists is that there is still no single method that does it all: analyzing a complex or large system can require the application of different formal methods, modeling different relevant aspects of the system in isolation. For instance, algebraic data types for its data, process algebras or temporal logics for its behavior, duration calculus or timed automata for its timing. In the efforts to address this problem, two directions can be distinguished: one is to try to increase the scope of individual methods, extending them to cover more aspects within a single formal method. The other is to try to couple methods to benefit from their combined coverage. In this year's Lentedagen we focus on the second direction, the coupling of formal methods.

Methods (or "notations") can be coupled with different degrees of tightness, in their Ten Commandments Revisited, Bowen and Hinchey distinguish three levels:

• Viewpoints in this loose coupling, different notations present different system views, with each notation emphasizing a particular system aspect.
• Method integration in a closer coupling, several notations (both formal and informal or semiformal) combine with manual or automatic translation between notations. The idea is to provide an underlying semantics for the less formal notations, to enable well- understood graphical (or other) presentations, and to offer the benefits of formal verification.
• Integrated methods in a tight coupling, multiple notations combine within a single framework to give a uniform semantics to each notation.

Program

Wednesday May 7

11.00-12.00 Registration

12.00-13.30 Lunch

Introduction

13.30-14.15: Arend Rensink (UT): Small tools and interoperability Abstract Slides Paper

Method integration: Checking models I

14.15-15.00 Marcel Verhoef (Chess): Co-simulation of distributed embedded real-time control systems -- Coupling VDM++ to 20-sim Abstract Slides Paper

15.00-15.45 Sander Vermolen (TUD): Automatically discharging VDM proof obligations using HOL Abstract Slides

15.45-16.15 Break

Integrated methods: Modeling and analysis with mCRL2

16.15-17.00 Jan Friso Groote (TU/e): The mCRL2 philosophy Slides

17.00-17.45 Yaroslav Usenko (LaQuSo): Linearization of processes Abstract Slides

17.45-18.30 Tim Willemse (TU/e): Parametrized boolean equation systems Slides

18.30-19.00 Drinks

19.00-20.30 Dinner

Thursday May 8

Invited lecture

09.00-10.30 Hubert Garavel (INRIA Rhone-Alpes): Integrating formal methods within a process calculi framework Paper

10.30-11.00 Break

Method integration: Intermediate formats

11.00-11.45 Ramon Schiffelers (TU/e): The Common Interchange Format Slides

Method integration: Model checking I

11.45-12.30 Michael Weber (UT): NIPS -- A black-box approach to model checking tools Abstract Slides Paper

12.30-14.30 Lunch & zoo

Method integration: Checking models II

14.30-15.15 Suzana Andova (TU/e): Dynamic consistency in process algebra -- From Paradigm to ACP Abstract Slides

15.15-16.00 Jozef Hooman (ESI/RU): Towards checking Stateflow models with mCRL Abstract Slides

16.00-16.30 Break

Invited lecture

16.30-18.00 Einar Broch Johnsen (University of Oslo): Combining semantics with analysis in the Maude framework Abstract

Integrated methods: Credo

18.00-18.45 MohammadMahdi Jaghouri (CWI): Modelchecking & testing for schedulability of concurrent objects Abstract Slides Paper

19.00-20.30 Dinner

20.30- ..... Social event

Friday May 9

Method integration: Dependability analysis

09.00-09.45 Pepijn Crouzen (Universität des Saarlandes): Dynamic fault tree analysis using input/output interactive Markov chains Abstract Slides Paper 1 Paper 2

Method integration: Model checking II

09.45-10.30 Theo C. Ruys (UT): An object-oriented, layered approach to validation tools Abstract Slides Paper

10.30-11.00 Break

11.00-11.45 Arend Rensink (UT): Model checking dynamic states in Groove Abstract Slides

Viewpoints and method integration: Industrial case studies

11.45-12.30 Mark Voorhoeve & Venkatesh Kannan (TU/e): Document handling -- three modeling approaches Abstract Slides

12.30-13.15 Niels Braspenning (ASML): Integrating formal methods and industry - a real-life case study Abstract

13.15-14.30 Lunch & departure

Costs

(Costs are based on single room)

Please note that Ph.D. students who are not in IPA will be charged as associated members if they belong to a research school that is associated with IPA (such as ASCI, SIKS, OZSL, and DISC) and as an other participant otherwise.

To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated "first come, first serve". All Ph.D. students (IPA and non-IPA) have to share a room. Others may also be asked to share if we run out of rooms. Registration for the event is still open, we will accept participants until we run out of space at the hotel!

Please remit the amount due, to our bank account with the ABN/AMRO. Account number: 60.27.60.690, in the name of V.A.J. Borghuis e/o S.M.H.J. Joosten, Den Dolech 2, 5600 AM Eindhoven. Please mention participation "IPA Lentedagen 2008".

Registration

Registration is for the Lentedagen is open, please register using the online Registration Form under the link. Registration closes on Monday April 21.

How to get to 't Paviljoen