13. – 18. September 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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
Programm des Dagstuhl-Seminars [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 der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.