September 13 – 18 , 2009, Dagstuhl Seminar 09381

Refinement Based Methods for the Construction of Dependable Systems


Jean-Raymond Abrial (Marseille, FR)
Michael Butler (University of Southampton, GB)
Rajeev Joshi (CalTech – Pasadena, US)
Elena Troubitsyna (Abo Akademi University – Turku, FI)
James C. P. Woodcock (University of York, GB)

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants
Dagstuhl Seminar Schedule [pdf]


The seminar brought together academicians that are experts in the area of dependability and formal methods and industry practitioners that are working on developing dependable systems. The industry practitioners have described their experience and challenges posed by formal modeling and verification. The academicians tried to address these challenges while describing their research work. We seminar proceeded in a highly interactive manner and provided us with an excellent opportunity to share experience.

One of the outcomes of that seminar was the identification of the following list of challenging issues faced by industrial users of formal methods:

  • Team-based development
  • Dealing with heavy model re-factoring
  • Linking requirements engineering and FMs
  • Abstraction is difficult
  • Refinement strategies are difficult to develop
  • Guidelines for method and tool selection
  • Keeping models and code in sync
  • Real-time modelling
  • Supporting reuse and variants
  • Proof automation
  • Proof reuse
  • Handling complex data structures
  • Code generation
  • Test case generation
  • Handling assumptions about the environment

The seminar has encouraged knowledge transfer between several major initiatives in the area of formal engineering of computer-based systems. We have got a good understanding of the advances made within the EU-funded project Deploy "Industrial deployment of system engineering methods providing high dependability and productivity". The project aims at integration of formal engineering methods into the existing development practice in such areas as automotive industry, railways, space and business domains. The participants described advantages and problems of refinement-based development using Event-B and Rodin tool platform. The advances made within the Grand Challenge in Verified Software initiative have been described by the researchers working on the Mondex system and a verified file store. Several large-scale experiments on system development and software verification were presented by the various researchers working in the software industry.

Discussions of such topics as foundations of program refinement, verification, theorem proving, techniques for ensuring dependability, automatic tool support for system development and verification, modeling concurrency and many others resulted in several new joint research initiatives and collaborative works.


  • Artificial Intelligence
  • Robotics
  • Soft Computing
  • Evol. Algorithms Interdisciplinary With Non-informatics-topic: Bioinformatics


  • Similarity-based clustering and classification
  • Metric adaptation and kernel design
  • Learning on graphs
  • Spatiotemporal data


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).

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.


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