Specification of software systems (Q4210110)

The book presents the fundamentals principles of formal methods in the construction of modular and verifiable formal specifications. It discusses formalisms that provide a theoretical foundation for the principles of software engineering, emphasizing mathematical structures that support writing and reasoning about specifications. The general features of specification language are also presented in an unified frame provided by set theory and logic. The languages discussed in the book are OBJ3, VDM, Z, Larch and Larch/C++. Their expression power is illustrated for different classes of applications too. The first three chapters of the book debate how to integrate formal methods in a development process and what are the attributes for a formal specification language. Chapters and 5 introduce the concept of formalism and abstraction and discuss extension of BNF and finite state machines. Chapters 6 and 7 discuss specification based on logic, set theory and relations and include material on proofs. Chapters 8-11 describe four representative specification languages: OBJ3 for algebraic specification, VDM and Z for model-based specification, Larch (and Larch/C++) for interface specification. The goal is to treat specification languages from abstract to concrete levels and to show how they can be utilized for specifying sequential systems. The book make a rigorous exposure of the construction of verifiable software. The topics are presented in a justifiable manner and are accompanied by proofs in rigorous as well as in formal style. The length of proofs is kept inside manageable boundaries. The book is self-contained and all chapters include a section of exercises. The features of OBJ3, VDM, Z, Larch and Larch/C++ are illustrated by case studies in Chapters 8-11. The material of Chapters 8-11 may be taught with provided tool-supported laboratory projects. Each chapter contains a section on bibliographical notes which give a broad account of work related to the topic discussed and help software professionals to identify industrial applications and learn from the experience reported on the use of tools. The material is designed to be used as a textbook both by students of computer science, software engineering and information engineering and by software professionals who learn formal specification languages and use formal methods in their work.