Published: 4th June 2016
DOI: 10.4204/EPTCS.209
ISSN: 2075-2180

EPTCS 209

Proceedings 17th International Workshop on
Refinement
Oslo, Norway, 22nd June 2015

Edited by: John Derrick, Eerke Boiten and Steve Reeves

Preface
Eerke A. Boiten, John Derrick and Steve Reeves
Formal refinement of extended state machines
Thomas Fayolle, Marc Frappier, Régine Laleau and Frédéric Gervais
1
Big Data Refinement
Eerke A. Boiten
17
Unifying Theories of Mobile Channels
Gerard Ekembe Ngondi
24
A logic for n-dimensional hierarchical refinement
Alexandre Madeira, Manuel A. Martins and Luís S. Barbosa
40
Program Derivation by Correctness Enhacements
Nafi Diallo, Wided Ghardallou, Jules Desharnais and Ali Mili
57
SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java
Alvaro Miyazawa and Ana Cavalcanti
71
Programming Language Features for Refinement
Jason Koenig and K. Rustan M. Leino
87
Towards linking correctness conditions for concurrent objects and contextual trace refinement
Brijesh Dongol and Lindsay Groves
107
A Theory of Service Dependency
Mats Neovius, Luigia Petre and Kaisa Sere
112

Preface

We are proud to present the papers from the 17th Refinement Workshop, co-located with FM 2015 held in Oslo, Norway on June 22nd, 2015.

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 17th 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. Eight 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 previous editions, the 17th edition was co-located with a major formal methods conference, this year we were delighted to be co-located with the FM international conference, which again proved to be a very productive pairing of events. The workshop had 10 presentations, and of those we have selected 9 papers for presentation in the published proceedings following a peer review process. The papers cover a wide range of topics in the theory and application of refinement.

This is the third volume that has appeared as an EPTCS proceedings, and we would like to thank the editorial board (and in particular Rob van Glabbeek) for their help and cooperation in making this happen. As last time, this edition had a small Program Committee, whose names appear below, and we thank them for their work.

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

Program committee

Eerke Boiten
John Derrick
Steve Reeves