Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 09381

Refinement Based Methods for the Construction of Dependable Systems

( Sep 13 – Sep 18, 2009 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:

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



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.

  • Jens Bendisposto (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
  • Eerke Boiten (University of Kent, GB)
  • Egon Börger (University of Pisa, IT) [dblp]
  • Michael Butler (University of Southampton, GB) [dblp]
  • Mathieu Clabaut (SYSTEREL Aix en Provence, FR)
  • John Colley (University of Southampton, GB)
  • John Derrick (University of Sheffield, GB)
  • Neil Evans (AWE Plc. - Berkshire, GB)
  • Fintan Fairmichael (University College Dublin, IE)
  • Leo Freitas (University of York, GB) [dblp]
  • Gudmund Grov (University of Edinburgh, GB) [dblp]
  • Stefan Hallerstede (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
  • Maritta Heisel (Universität Duisburg-Essen, DE) [dblp]
  • Michael G. Hinchey (University of Limerick, IE) [dblp]
  • Thai Son Hoang (ETH Zürich, CH)
  • Charles Anthony Richard Hoare (Microsoft Research UK - Cambridge, GB) [dblp]
  • Alexei Iliasov (University of Newcastle, GB) [dblp]
  • Dubravka Ilic (Space Syst. Finland Ltd - Espoo, FI) [dblp]
  • Andrew Ireland (Heriot-Watt University Edinburgh, GB)
  • Michael Jackson (The Open University - Milton Keynes, GB) [dblp]
  • Cliff B. Jones (University of Newcastle, GB) [dblp]
  • Rajeev Joshi (CalTech - Pasadena, US) [dblp]
  • Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
  • Dirk Leinenbach (DFKI - Saarbrücken, DE)
  • Michael Leuschel (Heinrich-Heine-Universität Düsseldorf, DE) [dblp]
  • Felix Lösch (Robert Bosch GmbH - Stuttgart, DE)
  • Larissa Meinicke (Macquarie University - Sydney, AU)
  • Dominique Méry (LORIA - Nancy, FR) [dblp]
  • C. Carroll Morgan (UNSW - Sydney, AU)
  • Louis Mussat (CLEARSY - Aix-en-Provence, FR)
  • Alexander Romanovsky (University of Newcastle, GB) [dblp]
  • Andreas Roth (SAP Research - Darmstadt, DE) [dblp]
  • Aryldo G Russo Jr (AeS Group - Sao Paolo, BR)
  • Thomas Santen (European Microsoft Innovation Center - Aachen, DE) [dblp]
  • Manoranjan Satpathy (General Motors - Bangalore, IN)
  • Gerhard Schellhorn (Universität Augsburg, DE) [dblp]
  • Holger Schmidt (Universität Duisburg-Essen, DE)
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Emil Sekerinski (McMaster University - Hamilton, CA)
  • Kaisa Sere (Abo Akademi University - Turku, FI)
  • Colin F. Snook (University of Southampton, GB) [dblp]
  • Maria Spichkova (TU München, DE)
  • Helen Treharne (University of Surrey, GB) [dblp]
  • Elena Troubitsyna (Abo Akademi University - Turku, FI) [dblp]
  • Stephen Wright (University of Bristol, GB)

  • 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