Concurrency verification. Introduction to compositional and noncompositional methods

MaRDI QIDQ2768503zbMATH OpenFDO

Authors Ulrich Hannemann, Jozef Hooman, Mannes Poel, Job Zwiers, Willem-Paul de Roever, Frank S. de Boer, Yassine Lakhnech

Publication date 3 February 2002

Published in Cambridge Tracts in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

absence of deadlock assumption commitment communication-closed-layers paradigm compositional reasoning concurrent program Hoare logic inductive assertion noncompositional proof method program transformation program verification rely-guarantee method semantic completeness shared variable soundness synchronous message temporal logic transition system

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

This textbook is the first part of a work published in two volumes devoted to the state-based verification of concurrent programs. In the first chapter the authors advocate by means of 3 examples the need to use (semi-) automated proof checkers to eliminate errors in verification proofs and explain the approach taken in this volume: state-based, property-oriented, dual language, and semantically-oriented. NEWLINENEWLINENEWLINEIn Chapter 2 semantical formulation is introduced of Floyd's inductive assertion method for sequential transition systems. This simple model of sequential programming is generalised in the next 2 chapters to, respectively, shared-variable concurrency and to distributed programs communicating by means of synchronous messages. The focus is on formulating a mathematical basis for state-based program verification and on proving partial correctness, absence of deadlock, absence of runtime errors, and termination properties. All proposed verification methods are proved to be sound and semantically complete. The goal of Chapter 5 is to investigate the expressibility of mathematical entities used in the soundness and semantic completeness proofs of the previous chapters in the language of first-order predicate logic over the standard model of the natural numbers. This result allows the authors to carry these proofs from the semantic level to the syntactic level of Hoare logic and constitutes in the opinion of the authors ``one of the distinguishing methodological features of this book. Compositional reasoning on large programs, understood as a strategy to verify a program ``on the basis of the specifications of its constituent subprograms only, without any knowledge of the interior construction of those subprograms is introduced in Chapter 6. This principle is very attractive for application to parallel composition because the complexity of this reasoning increases linearly w.r.t. the number of parallel components. The next two chapters are devoted to two powerful paradigms for compositional reasoning: the assumption-commitment method for verifying synchronous distributed message passing system and the rely-guarantee method for verifying shared-variable concurrency. NEWLINENEWLINENEWLINEIn Chapters 9-11 it is given a broad interpretation of Hoare logic regarded as a structured proof method for the inductive construction of inductive assertion networks for programs. Hoare-style proof systems for sequential programs, for shared-variable concurrency, and for synchronous message passing are formulated. Soundness and relative completeness of these logics is immediately derived from results previously obtained. The last chapter of the book explains how to develop a concurrent program starting from a relatively simple version of it, proving this basic instance is correct, and then transforming the sequential version into the actual program. Several program-transforms (including the communication-closed-layers paradigm for verifying network protocols) based on linear time temporal logic are introduced and proved correct. NEWLINENEWLINENEWLINEAll chapters end with exercises of various degrees of difficulty; the hardest ones and the open problems are marked as such. Ample historical notes serve as annotations for the more than 650 references listed in the bibliography. Every method is illustrated by examples explained at length. The formal exposition of essential ideas is preceded by informal discussions. The proofs are clear, detailed, and accompanied by enlightening comments. NEWLINENEWLINENEWLINEThe material contained in this textbook has been already used for courses of various duration. It is partly accessible for undergraduate students. Many themes appear for the first time in a self-contained textbook. More technical sections are aimed to lead up to state-of-the-art research in the area of compositional methods for concurrent program verification. The present textbook is a highly welcome addition to the existing literature on program verification, particularly valuable for the well-arranged, methodically unified framework for a wealth of material.

Recommendations

Cited in

(71)

This page was built for publication: Concurrency verification. Introduction to compositional and noncompositional methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2768503)