2017 | Book

# Concise Guide to Formal Methods

## Theory, Fundamentals and Industry Applications

Author: Prof. Dr. Gerard O'Regan

Publisher: Springer International Publishing

Book Series : Undergraduate Topics in Computer Science

2017 | Book

Author: Prof. Dr. Gerard O'Regan

Publisher: Springer International Publishing

Book Series : Undergraduate Topics in Computer Science

This invaluable textbook/reference provides an easy-to-read guide to the fundamentals of formal methods, highlighting the rich applications of formal methods across a diverse range of areas of computing.

Topics and features: introduces the key concepts in software engineering, software reliability and dependability, formal methods, and discrete mathematics; presents a short history of logic, from Aristotle’s syllogistic logic and the logic of the Stoics, through Boole’s symbolic logic, to Frege’s work on predicate logic; covers propositional and predicate logic, as well as more advanced topics such as fuzzy logic, temporal logic, intuitionistic logic, undefined values, and the applications of logic to AI; examines the Z specification language, the Vienna Development Method (VDM) and Irish School of VDM, and the unified modelling language (UML); discusses Dijkstra’s calculus of weakest preconditions, Hoare’s axiomatic semantics of programming languages, and the classical approach of Parnas and his tabular expressions; provides coverage of automata theory, probability and statistics, model checking, and the nature of proof and theorem proving; reviews a selection of tools available to support the formal methodist, and considers the transfer of formal methods to industry; includes review questions and highlights key topics in every chapter, and supplies a helpful glossary at the end of the book.

This stimulating guide provides a broad and accessible overview of formal methods for students of computer science and mathematics curious as to how formal methods are applied to the field of computing.

Advertisement

Abstract

This chapter presents a broad overview of software engineering and discusses the waterfall and spiral software lifecycle models. We discuss requirements gathering and specification, software design and implementation, software inspections and testing and maintenance. The lightweight Agile methodology is introduced, and it has become popular in software engineering. Software process maturity and project management are discussed, and formal methods are introduced. The extent to which mathematical approaches should be employed remains a topic of active debate.

Abstract

This chapter discusses software reliability and dependability, and covers topics such as software reliability and software reliability models, the Cleanroom methodology, system availability, safety and security critical software, and dependability engineering.

Abstract

This chapter discusses formal methods, which consist of a set of mathematic techniques that provide an extra level of confidence in the correctness of the software. They consist of a formal specification language and employ a collection of tools to support the syntax checking of the specification, as well as the proof of properties of the specification. They allow questions to be asked about what the system does independently of the implementation, and they may be employed to formally state the requirements of the proposed system, and to derive a program from its mathematical specification. They may be used to provide a rigorous proof that the implemented program satisfies its specification, and they have been applied mainly to the safety critical field.

Abstract

This chapter provides an introduction to fundamental building blocks in mathematics such as sets, relations and functions. Sets are collections of well-defined objects; relations indicate relationships between members of two sets A and B; and functions are a special type of relation where there is exactly (or at most) one relationship for each element a ϵ A with an element in B. A set is a collection of well-defined objects that contains no duplicates. A binary relation R (A, B) where A and B are sets is a subset of the Cartesian product (A × B) of A and B. A total function f: A → B is a special relation such that for each element a ϵ A there is exactly one element b ϵ B. This is written as f(a) = b. A partial function differs from a total function in that the function may be undefined for one or more values of A.

Abstract

Logic is concerned with reasoning and with establishing the validity of arguments. It allows conclusions to be deduced from premises according to logical rules, and the logical argument establishes the truth of the conclusion provided that the premises are true. The origins of logic are with the Greeks who were interested in the nature of truth. Aristotle developed syllogistic logic, where a syllogism consists of two premises and a conclusion. The Stoics developed an early form of propositional logic, where the assertibles (propositions) have a truth-value such that at any time they are either true or false. Boole’s symbolic logic and its application to digital computing are discussed, and we consider Frege’s work on predicate logic.

Abstract

Propositional logic is the study of propositions, where a proposition is a statement that is either true or false. Propositional logic may be used to encode simple arguments that are expressed in natural language, and to determine their validity. The validity of an argument may be determined from truth tables, or using inference rules such as modus ponens to establish the conclusion via deductive steps. Predicate logic allows complex facts about the world to be represented, and new facts may be determined via deductive reasoning. Predicate calculus includes predicates, variables and quantifiers, and a predicate is a characteristic or property that the subject of a statement can have. The universal quantifier is used to express a statement such as that all members of the domain of discourse have property P, and the existential quantifier states that there is at least one value of x has property P.

Abstract

We consider some advanced topics in logic including fuzzy logic, temporal logic, intuitionist logic, undefined values in logic, logic and AI and theorem provers. Fuzzy logic is an extension of classical logic that acts as a mathematical model for vagueness. Temporal logic is concerned with the expression of properties that have time dependencies. Brouwer and others developed intuitionist logic as the logical foundation for intuitionism, which was a controversial theory of the foundations of mathematics based on a rejection of the law of the excluded middle and an insistence on constructive existence. We discuss several approaches that have been applied to dealing with undefined values that arise with partial functions including the logic of partial functions; Dijkstra’s approach with his cand and cor operators; and Parnas’s approach which preserves a classical two-valued logic.

Abstract

This chapter presents the Z specification language, which is one of the most widely used formal methods. Z is a formal specification language based on Zermelo set theory. It was developed at the Programming Research Group at Oxford University in the early 1980s. Z specifications are mathematical and employ a classical two-valued logic. The use of mathematics ensures precision and allows inconsistencies and gaps in the specification to be identified. Theorem provers may be employed to demonstrate that the software implementation meets its specification.

Abstract

This chapter presents the Vienna Development Method, which is one of the older formal specification languages. It was developed at the IBM laboratory in Vienna as a method to specify the semantics of the PL/1 programming language, and it evolved into a formal specification language with a rigorous software development method with rules to verify the steps of development. The rules enable the executable specification, i.e. the detailed code, to be obtained from the initial specification via refinement steps, such that the executable code is a valid implementation of the formal specification.

Abstract

This chapter discusses the Irish school of VDM, which is a variant of standard VDM. It employs a constructive approach, classical mathematical style and a terse notation. Its terse style stipulates in concise form what the system should do, and furthermore, the fact that its specifications are constructive (or functional) means that that the how is included with the what.

Abstract

This Chapter presents the unified modelling language (UML), which is a visual modelling language for software systems, and it is used to present several views of the system architecture. It was developed at Rational Corporation as a notation for modelling object-oriented systems. We present various UML diagrams such as use case diagrams, sequence diagrams and activity diagrams.

Abstract

This Chapter focuses on the approach of Dijkstra, Hoare and Parnas. We discuss the calculus of weakest preconditions developed by Dijkstra and the axiomatic semantics of programming languages developed by Hoare. We then discuss the classical engineering approach of Parnas and his tabular expressions.

Abstract

Automata theory is the branch of computer science that is concerned with the study of abstract machines and automata. These include finite-state machines, pushdown automata and Turing machines. Finite-state machines are abstract machines that may be in one state at a time (current state), and the input symbol causes a transition from the current state to the next state. Pushdown automata have greater computational power, and they contain extra memory in the form of a stack from which symbols may be pushed or popped. The Turing machine is the most powerful model for computation, and this theoretical machine is equivalent to an actual computer in the sense that it can compute exactly the same set of functions.

Abstract

Model checking is an automated technique such that given a finite state model of a system and a formal property (expressed in temporal logic), then it systematically checks whether the property is true of false in a given state in the model.

Abstract

Chapter 15 discusses the nature of proof and theorem proving and considers the history of theorem proving from the development of the Logic Theorist theorem prover in 1956. We discuss automated and interactive theorem provers; the nature of mathematical proof and formal mathematical proof; and a selection of existing theorem provers.

Abstract

This chapter discusses probability and statistics and includes a discussion on discrete random variables; probability distributions; sample spaces; sampling; the abuse of statistics; variance and standard deviation; hypothesis testing. Statistics is an empirical science that is concerned with the collection, organization, analysis, interpretation and presentation of data. They allow the behaviour of a population to be studied and inferences to be made about the population.

Abstract

This chapter gives a flavour of a selection of tools that are available to support the formal methodist in the performance of the various activities. Tools for VDM, Z, B, UML, theorem provers and model checking are considered. The tools include syntax checkers to determine whether the specification is syntactically correct; specialized editors which ensure that the written specification is syntactically correct; tools to support refinement; automated code generators that generate a high-level language corresponding to the specification; theorem provers to demonstrate the correctness of the refinement steps and to identify and resolve proof obligations, as well proving the presence or absence of key properties; and specification animation tools where the execution of the specification can be simulated.

Abstract

This chapter discusses technology transfer which is concerned with the practical exploitation of new technology developed by an academic or industrial research group, and the objective is to facilitate the use of the technology in an industrial environment. Technology transfer needs to take place in a controlled manner, and it is important to conduct a pilot of the technology prior to a decision on general deployment.

Abstract

This chapter is the concluding chapter in which we summarize the journey that we have travelled in this book.