Specification of software systems
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.
- Software engineering 2. Specification of systems and languages. With contributions from Christian Krog Madsen.
- Rigorous software development. An introduction to program verification.
- Formal methods for software engineering. Languages, methods, application domains. With a foreword by Manfred Broy and a contribution on the origins and development of formal methods by John V. Tucker
- Logics of specification languages
- Software specifcation methods. On overview using a case study.
- scientific article; zbMATH DE number 3905823 (Why is no real title available?)
- scientific article; zbMATH DE number 1189004 (Why is no real title available?)
- Object-oriented programming and Java
- Formal specification. Techniques and applications
- Specifying Software
- scientific article; zbMATH DE number 194792 (Why is no real title available?)
- What causes a system to satisfy a specification?
- Principles of abstract interpretation
This page was built for publication: Specification of software systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4210110)
