Specification Case Studies in RAISE

The book describes 12 case studies which use RAISE (Rigorous Approach to Industrial Software Engineering) to con- struct, analyse, develop and apply formal specifications. The case studies present a wide range of application areas: authentication of communications protocols, error detection in programs, geographic information systems, library management, multi-lingual documents, production planning, run-time verification, software design patterns, software reuse, taxation management, telephony, and travel planning. Most have little or nothing to do with safety-critical systems, traditionally considered as the area in which formal methods are most applicable, and many of them do not involve verification. The cases studies illustrate diverse uses of formal specifications: to capture requirements for new software, to carry out software development from requirements, to formalise algorithms in order to prove their correctness, to check if software behaves correctly at run-time, to build models of application domains, to relate descriptive and prescriptive models, to formalise notations for software development, and various other uses. They also try to put the task of creating formal specifications into perspective, asking questions about the purpose, scope and use of the formal models before the models are built.

The case study chapters have each been written by one of this book's editors. Each case study describes work done at the United Nations University's International Institute for Software Technology (UNU-IIST) in Macau by that editor in collaboration with fellows (lecturers or post-graduate students from developing countries). Each case study chapter concludes with information about the fellows involved, the relevant UNU-IIST technical report(s), and other related work.