http://www.dagstuhl.de/13372

September 8 – 13 , 2013, Dagstuhl Seminar 13372

Integration of Tools for Rigorous Software Construction and Analysis

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)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 3, Issue 9 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]

Summary

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:

  1. Inspire exchange and joint use of formal modelling tool technologies
  2. Establish long-term cross-community collaboration
  3. 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.

License
  Creative Commons BY 3.0 Unported license
  Uwe Glässer, Stefan Hallerstede, Michael Leuschel, and Elvinia Riccobene

Related Dagstuhl Seminar

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)

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.