Ebook: 4th Refinement Workshop: Proceedings of the 4th Refinement Workshop, organised by BCS-FACS, 9–11 January 1991, Cambridge

This volume contains the proceedings ofthe 4th Refinement Workshop which was organised by the British Computer Society specialist group in Formal Aspects of Computing Science and held in Wolfson College, Cambridge, on 9-11 January, 1991. The term refinement embraces the theory and practice of using formal methods for specifying and implementing hardware and software. Most of the achievements to date in the field have been in developing the theoretical framework for mathematical approaches to programming, and on the practical side in formally specifying software, while more recently we have seen the development of practical approaches to deriving programs from their speCifications. The workshop gives a fair picture of the state of the art: it presents new theories for reasoning about software and hardware and case studies in applying known theory to interesting small-and medium-scale problems. We hope the book will be Of interest both to researchers in formal methods, and to software engineers in industry who want to keep abreast of possible applications of formal methods in industry. The programme consisted both of invited talks and refereed papers. The invited speakers were Ib S0rensen, Jean-Raymond Abrial, Donald MacKenzie, Ralph Back, Robert Milne, Mike Read, Mike Gordon, and Robert Worden who gave the introductory talk. This is the first refinement workshop that solicited papers for refereeing, and despite a rather late call for papers the response was excellent.

---

This volume contains the papers presented at the 4th Refinement Workshop, organised by the Formal Aspects group of the British Computer Society, and held in Cambridge on January 9-11, 1991. Refinement is the term used to describe systematic and formal methods of specifying hardware and software, and transforming the specifications into designs and implementations. The value of formal methods in producing reliable hardware and software is by now widely appreciated among both academics and many workers in industry, although such methods - and in particular their application to industrial-scale problems - are still in their infancy. This workshop brought together some of the best European workers in the field to present tutorials on the state of the art in both theory and industrial application, to describe their latest research, and to indicate future directions. The papers cover the development of both sequential and concurrent systems, and both theoretical ideas and support tools for their effective use. This volume will be of interest to researchers in formal methods, and software engineers wanting to keep track of developments in the application of formal methods in industry.

---

This volume contains the papers presented at the 4th Refinement Workshop, organised by the Formal Aspects group of the British Computer Society, and held in Cambridge on January 9-11, 1991. Refinement is the term used to describe systematic and formal methods of specifying hardware and software, and transforming the specifications into designs and implementations. The value of formal methods in producing reliable hardware and software is by now widely appreciated among both academics and many workers in industry, although such methods - and in particular their application to industrial-scale problems - are still in their infancy. This workshop brought together some of the best European workers in the field to present tutorials on the state of the art in both theory and industrial application, to describe their latest research, and to indicate future directions. The papers cover the development of both sequential and concurrent systems, and both theoretical ideas and support tools for their effective use. This volume will be of interest to researchers in formal methods, and software engineers wanting to keep track of developments in the application of formal methods in industry.
Content:
Front Matter....Pages i-viii
The Process of Refinement....Pages 1-5
Engineering Real Software Using Formal Methods....Pages 6-33
Specialising Abstract Programs....Pages 34-50
A Refinement Case Study (using the Abstract Machine Notation)....Pages 51-96
Assertional Data Reification Proofs: Survey and Perspective....Pages 97-114
Formal Methods and the Sociology of Proof....Pages 115-124
Refinement Diagrams....Pages 125-137
A Case Study in Timed Refinement: A Central Heater....Pages 138-149
Object Oriented Specification and Refinement....Pages 150-184
The Ecology of Class Refinement....Pages 185-196
Transforming axioms for data types into sequential programs....Pages 197-240
Refinement of two graph problems....Pages 241-257
CSP and Timewise Refinement....Pages 258-280
The Elusive Software Refinery: a case study in program development....Pages 281-325
A Theory of State-based Parallel Programming: Part 1....Pages 326-359
Design, verification and documentation of concurrent systems....Pages 360-377
A Formal Method for Hard Real-Time Programming....Pages 378-410
Constructing and Refining Modules in a Type Theory....Pages 411-440
The Varieties of Refinement....Pages 441-455
Timed Process Algebra, Petri Nets, and Event Refinement....Pages 456-478
Back Matter....Pages 479-480

---

This volume contains the papers presented at the 4th Refinement Workshop, organised by the Formal Aspects group of the British Computer Society, and held in Cambridge on January 9-11, 1991. Refinement is the term used to describe systematic and formal methods of specifying hardware and software, and transforming the specifications into designs and implementations. The value of formal methods in producing reliable hardware and software is by now widely appreciated among both academics and many workers in industry, although such methods - and in particular their application to industrial-scale problems - are still in their infancy. This workshop brought together some of the best European workers in the field to present tutorials on the state of the art in both theory and industrial application, to describe their latest research, and to indicate future directions. The papers cover the development of both sequential and concurrent systems, and both theoretical ideas and support tools for their effective use. This volume will be of interest to researchers in formal methods, and software engineers wanting to keep track of developments in the application of formal methods in industry.
Content:
Front Matter....Pages i-viii
The Process of Refinement....Pages 1-5
Engineering Real Software Using Formal Methods....Pages 6-33
Specialising Abstract Programs....Pages 34-50
A Refinement Case Study (using the Abstract Machine Notation)....Pages 51-96
Assertional Data Reification Proofs: Survey and Perspective....Pages 97-114
Formal Methods and the Sociology of Proof....Pages 115-124
Refinement Diagrams....Pages 125-137
A Case Study in Timed Refinement: A Central Heater....Pages 138-149
Object Oriented Specification and Refinement....Pages 150-184
The Ecology of Class Refinement....Pages 185-196
Transforming axioms for data types into sequential programs....Pages 197-240
Refinement of two graph problems....Pages 241-257
CSP and Timewise Refinement....Pages 258-280
The Elusive Software Refinery: a case study in program development....Pages 281-325
A Theory of State-based Parallel Programming: Part 1....Pages 326-359
Design, verification and documentation of concurrent systems....Pages 360-377
A Formal Method for Hard Real-Time Programming....Pages 378-410
Constructing and Refining Modules in a Type Theory....Pages 411-440
The Varieties of Refinement....Pages 441-455
Timed Process Algebra, Petri Nets, and Event Refinement....Pages 456-478
Back Matter....Pages 479-480
....