Published: 17th June 2011
DOI: 10.4204/EPTCS.55
ISSN: 2075-2180

EPTCS 55

Proceedings 15th International
Refinement Workshop
Limerick, Ireland, 20th June 2011

Edited by: John Derrick, Eerke Boiten and Steve Reeves

Preface
Discovery of Invariants through Automated Theory Formation
Maria Teresa Llano, Andrew Ireland and Alison Pease
1
Bigraphical Refinement
Gian Perrone, Søren Debois and Thomas Hildebrandt
20
Building a refinement checker for Z
John Derrick, Siobhán North and Anthony J.H. Simons
37
Refinement by interpretation in π-institutions
César Rodrigues, Manuel A. Martins, Alexandre Madeira and Luis S. Barbosa
53
Refinement-based verification of sequential implementations of Stateflow charts
Alvaro Miyazawa and Ana Cavalcanti
65
Refinement for Probabilistic Systems with Nondeterminism
Steve Reeves and David Streader
84
Model exploration and analysis for quantitative safety refinement in probabilistic B
Ukachukwu Ndukwu and Annabelle McIver
101
Formalising the Continuous/Discrete Modeling Step
Richard Banach, Huibiao Zhu, Wen Su and Runlei Huang
121
A CSP Account of Event-B Refinement
Steve Schneider, Helen Treharne and Heike Wehrheim
139
Perspicuity and Granularity in Refinement
Eerke Boiten
155
Concurrent Scheduling of Event-B Models
Pontus Boström, Fredrik Degerlund, Kaisa Sere and Marina Waldén
166

Preface

We are proud to present the papers from the 15th Refinement Workshop, co-located with FM 2011 held in Ireland on June 20th, 2011. Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification.

This 15th workshop continued a 20+ year tradition in refinement workshops run under the auspices of the British Computer Society (BCS) FACS special interest group. After the first seven editions had been held in the UK, in 1998 it was combined with the Australasian Refinement Workshop to form the International Refinement Workshop, hosted at The Australian National University. Six more editions have followed in a variety of locations, all with electronic published proceedings and associated journal special issues, see the workshop homepage at www.refinenet.org.uk for more details.

Like the previous two editions, the 15th edition was co-located with the FM international conference, which again proved to be a very productive pairing of events. This volume contains 11 papers selected for presentation at the workshop following a peer review process. The papers cover a wide range of topics in the theory and application of refinement. Previous recent workshops have appeared as ENTCS proceedings; this year we are publishing with EPTCS for the first time, and we would like to thank the editorial board (and in particular Rob van Glabbeek) for their help and cooperation in making this happen. This edition had a small Program Committee, whose names appear below, and we thank them for their work.

A special issue of the journal Formal Aspects of Computing is planned containing developments and extensions of the best workshop papers.

The organisers would like to thank everyone: the authors, BCS-FACS, EPTCS, and the organisers of FM 2011 for their help in organising this workshop, the participants of the workshop, and the reviewers involved in selecting the papers.

Program committee

Eerke Boiten, University of Kent, UK (co-chair)
John Derrick, University of Sheffield, UK (co-chair)
Steve Reeves, University of Waikato, NZ (co-chair)
Richard Banach, University of Manchester, UK
Luis Barbosa, University of Minho, PT
Andrew Butterfield, Trinity College Dublin and LERO, Ireland
Ana Cavalcanti, University of York, UK
Yifeng Chen, Peking University, PR China
Steve Dunne, Teesside University, UK
Lindsay Groves, Victoria University of Wellington, NZ
Stefan Hallerstede, Heinrich-Heine-Universitaet Duesseldorf, Germany
Eric Hehner, University of Toronto, Canada
Wim Hesselink, University of Groningen, NL
Stephan Merz, Inria Nancy and LORIA, France
Marcel Oliveira, Universidade Federal do Rio Grande do Norte, Brazil
Gerhard Schellhorn, Augsburg University, Germany
Steve Schneider, University of Surrey, UK
Emil Sekerinski, McMaster University, Canada
Graeme Smith, University of Queensland, Australia
Helen Treharne, University of Surrey, UK
Heike Wehrheim, University of Paderborn, Germany

Eerke Boiten
John Derrick
Steve Reeves