Refinement Techniques in Software Engineering

First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004 Revised Lectures

  • Ana Cavalcanti
  • Augusto Sampaio
  • Jim Woodcock
Textbook PSSE 2004

Part of the Lecture Notes in Computer Science book series (LNCS, volume 3167)

Table of contents

  1. Front Matter
  2. Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
    Pages 1-17
  3. Augusto Sampaio, Paulo Borba
    Pages 18-63
  4. Jim Davies
    Pages 64-122
  5. Annabelle McIver, Carroll Morgan
    Pages 123-155
  6. Zhiming Liu, Mathai Joseph
    Pages 156-219
  7. Ana Cavalcanti, Jim Woodcock
    Pages 220-268
  8. Phil Clayton, Colin O’Halloran
    Pages 269-314
  9. David Déharbe
    Pages 315-367
  10. Back Matter

About this book


The Pernambuco School on Software Engineering (PSSE) 2004 was the ?rst in a series of events devoted to the study of advanced computer science and to the promotion of international scienti?c collaboration. The main theme in 2004 was re?nement (or rei?cation). Re?nement describes the veri?able relationship between a speci?cation and its implementation; it also describes the process of discoveringappropriateimplementations,givena speci?cation.Thus,in oneway or another, re?nement is at the heart of the programming process, and so is the major daily activity of everyprofessionalsoftwareengineer. The Summer School and its proceedings were intended to give a detailed tutorial introduction to the scienti?c basis of this activity. These proceedings record the contributions from the invited lecturers. Each chapter is the result of a thorough revision of the initial notes provided to the participants of the school. The revision was inspired by the synergy generated by the opportunity for the lecturers to present and discuss their work among themselves, and with the school’s attendees. The editors have tried to produce a coherent view of the topic by harmonizing these contributions, smoothing out di?erences in notation and approach, and providing links between the lectures. We apologize to the authors for any errors introduced by our extensive editing. Although the chapters are linked in severalways, each one is su?ciently se- contained to be read in isolation. Nevertheless, Chap. 1 should be read ?rst by those interested in an introduction to re?nement.


concurrency formal method logic model checking object object-oriented programming program generation program optimization programming real time systems real-time refinement temporal logic transformation of models transformation of programs

Editors and affiliations

  • Ana Cavalcanti
    • 1
  • Augusto Sampaio
    • 2
  • Jim Woodcock
    • 3
  1. 1.Department of Computer ScienceUniversity of YorkYorkUK
  2. 2.Centro de InformáticaUniversidade Federal de PernambucoRecife/PEBrazil
  3. 3.University of York 

Bibliographic information

Industry Sectors
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Energy, Utilities & Environment