Published: 24th May 2013|
|Preface Eerke Boiten, John Derrick and Steve Reeves|
|On Kaisa Sere's Contributions to Refinement Research Luigia Petre, Elena Troubitsyna and Marina Waldén|
|On a New Notion of Partial Refinement Emil Sekerinski and Tian Zhang||1|
|Data refinement for true concurrency Brijesh Dongol and John Derrick||15|
|Modelling and Refinement in CODA Michael Butler, John Colley, Andrew Edmunds, Colin Snook, Neil Evans, Neil Grant and Helen Marshall||36|
|Refining SCJ Mission Specifications into Parallel Handler Designs Frank Zeyda and Ana Cavalcanti||52|
|Relaxing Behavioural Inheritance Nuno Amálio||68|
|Bisimilarity and refinement for hybrid(ised) logics Alexandre Madeira, Manuel A. Martins and Luís Soares Barbosa||84|
We are proud to present the papers from the 16th Refinement Workshop, co-located with iFM 2013 held in Turku, Finland on June 11th, 2013.
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 16th 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. Seven 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 16th edition was co-located with a major formal methods conference, this year we were delighted to be co-located with the iFM international conference, which again proved to be a very productive pairing of events. This volume contains 6 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.
The workshop, and iFM, was saddened by the recent death of Kaisa Sere, who had undertaken work on program refinement for many, many years. She was not only a pioneer in the subject, but a tower of strength at Abo Akademi University in Turku, where this year's Refinement Workshop and iFM are located. This year's workshop is dedicated to her memory. We felt it only fitting that the central talk this year was devoted to her work, and were pleased that three of her former female students contributed a joint talk in her memory. Kaisa's work lives on through their own work at Abo Akademi. You will find the abstract of their talk in this volume.
This is the second 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.
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 iFM 2013 for their help in organising this workshop, the participants of the workshop, and the reviewers involved in selecting the papers.
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
Ana Cavalcanti, University of York, UK
Steve Dunne, Teesside University, UK
Lindsay Groves, Victoria University of Wellington, NZ
Stefan Hallerstede, Aarhus University, DK
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
Kaisa Sere (1954-2012) built her career starting from the core paradigm of stepwise derivation of parallel algorithms, i.e., by applying a correct-by-construction refinement approach to address practical problems. She succeeded remarkably in integrating this paradigm into a wide range of domains. In this talk three of her closest collaborators and former PhD students overview the main achievements of Kaisa's research path from 1990 to 2012. In the first part of the talk we discuss fundamental research results on, among other topics, superposition and stepwise refinement, reverse engineering, procedures and composition, as well as scheduling. In the second part of the talk we discuss how Kaisa's research influenced a succession of European projects that resulted in the development of industrial-strength automated tools for formal modeling and refinement -- the Rodin platform. In the third part of the talk, we discuss her latest research results, aimed at addressing contemporary computing paradigms through the same correct-by-construction approach. We review some of her results on object-orientation, mobility, energy-awareness, wireless sensor networks, networks-on-chip, trustworthiness and availability.
The flagship of Kaisa's career was her passion for applying formal modeling and refinement concepts to novel domains. She cared deeply about educating more researchers in these concepts, to contribute to transforming software development into a more mature engineering discipline. We have taken the challenge of keeping her vision alive.