Dagstuhl Seminar 13372
Integration of Tools for Rigorous Software Construction and Analysis
( Sep 08 – Sep 13, 2013 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/13372
Organizers
- Uwe Glässer (Simon Fraser University - Burnaby, CA)
- Stefan Hallerstede (Aarhus University, DK)
- Michael Leuschel (Heinrich-Heine-Universität Düsseldorf, DE)
- Elvinia Riccobene (University of Milan, IT)
Contact
- Susanne Bach-Bernhard (for administrative matters)
Schedule
The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods and tools that are distinguished by their mathematical rigor and have proved to be industrially viable. A main goal of the seminar is to contribute to the integration of accurate state- and machine-based system development methods, clarifying their commonalities and differences to better understand how to combine related approaches for accomplishing the various modeling tasks of reliable high-quality hardware/software systems, such as experimental validation or mathematical verification.
We believe that it is vital to bring together the tool developer communities of the various state-based formal methods. Indeed, each community has valuable tools and technologies which would be beneficial also for the other approaches. Thus, it will be hugely beneficial to share various techniques and tools such as simulators, model checkers and theorem provers that have been developed for the individual state-based formal methods. A Dagstuhl seminar will provide the ideal setting for this, initiating fruitful exchanges and hopefully having a long-lasting impact.
The main questions and issues are grouped into the individual study groups below. Each study group will be addressed during a day or half-day during the workshop and will be driven by case studies which we will distribute several months before the event.
- Study Group 1: Survey of the Current State of the Art
- Study Group 2: Short-term Integration (low-hanging fruits)
- Study Group 3: Methodologies and Techniques for Tools Integration
- Study Group 4: Industrial, Commercial and Academic Exploitation
- Study Group 5: Prospects, Challenges for Future Tools
- Study Group 6: Prospects, Challenges and Vision for Future State-Based Formal Methods
Motivation
Dagstuhl Seminar 06191 had been a success in establishing the "ABZ" joint conference for the different state-based modelling communities (e.g., ASM, B, VDM, Z, TLA+) with venues in London (2008), Orford, CA (2010), Pisa (2012) and Toulouse (2014). It was a first step toward bringing these communities closer together. However, the conference, although being a place where the researchers meet, does not produce in itself a significant number of collaborations across the communities. The organisers of this seminar consider such collaborations vital in order to achieve a larger impact academically and industrially.
Aims of the seminar
The seminar aims to:
- Inspire exchange and joint use of formal modelling tool technologies
- Establish long-term cross-community collaboration
- Work towards a common vision on formal modelling
Points 2 and 3 are particularly important for future tool developments, a common methodical foundation, and more economic use of the necessary and available resources.
Preparation
At first the organisers intended to give the participants of the seminar case studies in advance that the participants could work on prior to the seminar to showcase their methods and tools. However, a downside of this common organisational practice is that most attendees arrive at the seminar with well-prepared, polished formal models and presentations. This would have resulted in conference-style presentations, not leaving much room for cross-community group work on problems with mixed-method approaches. Thus, no substantial gain above and beyond what the "ABZ" conferences already accomplish would have been achieved. Hence, the organisers decided to take the risk not to ask for advance preparation but have all the work done collaboratively during the seminar. This was thought to create a more open atmosphere and leave room for discussion. The organisers chose candidates for case studies to be carried out during the seminar and asked the participants to explore solutions with diverse methods in small, often mixed, groups formed dynamically based on interests. A tentative schedule for the week was published prior to the seminar. It was adapted by the organisers every night, taking into account the actual progress by the work groups and feedback received in plenum discussions held every day in the late afternoon or evening.
Execution
On Sunday evening the organisers held a three hour meeting to prepare day 1 of the seminar. It was decided that, in general, evenings should be left for the participants to socialise. The case study for day 1 needed to be well-chosen to engage the participants in the seminar. It was required that
- a single problem should be treated to minimise presentation overhead necessary for explaining the model
- the problem to be solved should not be trivial but solvable within 3 hours
- the problem should not leave too much room for interpretation so that the models, methods and tools used are more readily comparable
- the problem to be solved should come with a sketch of a solution so that focus would be on the modelling activity itself and not on finding the smartest solution.
The decision was made to use the problem of "Derivation of a termination detection algorithm for distributed computations'' (EWD840) by E. W. Dijkstra.
On day 1, all but one group succeeded in producing a formal model. (That group produced their model on day 2 in the after-lunch session.) At the end of day 1, the organisers felt that not enough discussion across community boundaries was taking place. This would have to be addressed in the following days. The planning for day 2, payed specific attention to this aspect. In the evening of day 1, a two-hour planning meeting among the organisers was held. It was decided that a good way of getting the different communities involved in discussions would be to reshuffle the groups of day 1 somewhat. To carry out a comparison between the methods and tools, each group would have some members that produced the original model and some "envoys" of a group that had modelled the problem in a different notation. (This turned out to work well. By lunchtime on day 2, live discussions across the community boundaries had effectively started.) On suggestion of the participants, an originally planned plenum discussion on tool integration was carried out in three groups dealing with methodology, abstract syntax and low-level integration. (The actual number of groups was decided together with all participants in the beginning of the corresponding session. Even though it may have appeared frustrating at times for some participants, the organisers thought involving all participants in some of the decision making would also improve everyone's commitment.) The organisers also started incorporating talks. This was also considered useful for breaking the routine of the seminar.
In the evening of day 2, a one hour meeting among the organisers was held to plan day 3. It was thought that the participants could be involved closer by forming new groups that should each address a problem using two different approaches and tools. The comparison would then be possible while modelling. The modelling problem chosen was the FM'99 ATM modelling challenge. Two more talks followed on day 3 and some planning for integration meetings that should be held in smaller groups on day 4. The latter were considered to be fruitful by many with a lot of common interests being announced. In the afternoon of day 3, a shorter hike provided a welcome break, as the weather did not invite for larger excursions.
On day 3 in the evening, a 30 minute meeting of the organisers was held. The plan for day 4 was mostly to tie up the open threads from the preceding days. A short wrap up of the case studies followed by presentations giving a comparison between two methods. In the evening, a first discussion of post-seminar work was held, discussing the Dagstuhl report and a joint book on "comprehensive modelling and modelling tools". In the evening of day 4, a 30 minute meeting by the organisers was held. It was decided that the morning of day 5 should be spent discussing the joint book. Uwe Glässer presented an alternative case for use in the book to start a discussion about the writing approach that should be taken. (On day 5, it was decided to keep the ATM study but improve its description.)
Outcomes and Outlook
The main outcomes of the seminar are (a) various new collaborations across community boundaries to achieve a possible integrated use of different methods and tools, and (b) concrete plans for a book on "comprehensive modelling", a step towards a common vision of the research field. An agreement has been reached with Springer Verlag to publish the post proceedings of the seminar in the State-Of-The-Art series of Lecture Notes in Computer Science. This should improve visibility of the effort started at the seminar.
The organisers seek to get funding, e.g., by way of a network of excellence, to continue the integration work and keep up the momentum achieved during the seminar. The aim will be to develop a common vision and a more coordinated research agenda where, in particular, resources for tool development could be used more efficiently in future.
Creative Commons BY 3.0 Unported license
Uwe Glässer, Stefan Hallerstede, Michael Leuschel, and Elvinia Riccobene
- Paolo Arcaini (University of Milan, IT) [dblp]
- Jens Bendisposto (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
- Egon Börger (University of Pisa, IT) [dblp]
- Marcel Dausend (Universität Ulm, DE) [dblp]
- David Déharbe (Federal University of Rio Grande do Norte, BR) [dblp]
- Albert Fleischmann (Metasonic AG - Pfaffenhofen, DE) [dblp]
- Marc Frappier (University of Sherbrooke, CA) [dblp]
- Leo Freitas (University of Newcastle, GB) [dblp]
- Angelo Gargantini (University of Bergamo, IT) [dblp]
- Vincenzo Gervasi (University of Pisa, IT) [dblp]
- Uwe Glässer (Simon Fraser University - Burnaby, CA) [dblp]
- Stefan Hallerstede (Aarhus University, DK) [dblp]
- Dominik Hansen (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
- Ian Hayes (The University of Queensland - Brisbane, AU) [dblp]
- Cliff B. Jones (University of Newcastle, GB) [dblp]
- Markus Alexander Kuppe (Universität Hamburg, DE)
- Peter Gorm Larsen (Aarhus University, DK) [dblp]
- Thierry Lecomte (CLEARSY - Aix-en-Provence, FR) [dblp]
- Michael Leuschel (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
- Fernando Mejia (Alstom Transport - Saint-Quen, FR) [dblp]
- Stephan Merz (LORIA - Nancy, FR) [dblp]
- Andreas Prinz (University of Agder - Grimstad, NO) [dblp]
- Alexander Raschke (Universität Ulm, DE) [dblp]
- Elvinia Riccobene (University of Milan, IT) [dblp]
- Gerhard Schellhorn (Universität Augsburg, DE) [dblp]
- Klaus-Dieter Schewe (Software Competence Center - Hagenberg, AT) [dblp]
- Colin F. Snook (University of Southampton, GB) [dblp]
- Hernán Vanzetto (INRIA Lorraine - Nancy, FR) [dblp]
- Laurent Voisin (SYSTEREL Aix en Provence, FR) [dblp]
- Qing Wang (Australian National University, AU) [dblp]
- Kirsten Winter (The University of Queensland - Brisbane, AU) [dblp]
- Hamed Yaghoubi Shahir (Simon Fraser University - Burnaby, CA) [dblp]
Related Seminars
- Dagstuhl Seminar 06191: Rigorous Methods for Software Construction and Analysis (2006-05-07 - 2006-05-12) (Details)
Classification
- modelling / simulation
- semantics / formal methods
- verification / logic
Keywords
- state-based formal methods (ASM
- B
- TLA+)
- tools (model checking
- theorem proving
- animation
- simulation
- model-based testing
- specification and design)
