Series Introduction:Formal methods as a branch of the discipline of computer and software engineering are increasingly entering many practical fields in the industry. Industrial standards represented by DO-333 aviation standards also explicitly require the use of formal methods in the software development process. In order to do so, combining with the successful application experience of Shanghai Kong'an formal methods technology team in the fields of aviation, aerospace, and rail transit over the years, this topic will focus on "formal methods", especially the engineering application of formal methods, organize a series of articles, and discuss the motivations and key technologies behind formal methods and their industry applications.
01Difficulties faced by traditional software engineering
Since the concept of "software engineering" was proposed in 1968, the research and practice of software engineering have effectively solved the problems of software quality and development efficiency. However, the large number of activities and subjective judgments in traditional software engineering, such as processes and technologies, have brought increasingly obvious credibility issues to software. Taking the most common "V" model in the industrial field as an example, we explore some limitations of traditional software engineering.
Figure 1: The V-model commonly seen in industrial standards
According to the V-model of software development process, we can see that even the V-model, which is highly recommended in the industry, still has obvious limitations and risks in describing the software development process:
(1) Accuracy of documents in the software development process
Software requirements are generally written in natural language, which causes documents to be difficult to accurately describe the expected functions and performance of the software due to the inherent ambiguity and ambiguity of natural language. Design documents use graphical descriptions, often lacking strict syntax and semantics. The defects of such intermediate products are often passed on to the code and testing stages, and some deep-seated problems are almost always difficult to detect.
(2) Dependency on subjective activities in the software development process
The consistency between the conversion and products of each stage in the software development process is heavily dependent on manual judgment. For example, whether the design document is consistent with the functional and behavioral descriptions in the requirement document is often reviewed and compared manually.
(3) Rigor in the software development process
Intermediate products in the process of software development lack strict analytical methods. For example, requirement documents written in natural language are difficult to be analyzed strictly. The system architecture described in design documents is verified through simple simulations and lacks in-depth verification of system behavior, such as deadlock and other security risks that are difficult to reveal.
Although the industry and academia have achieved substantial results in software engineering theory and practice, software quality issues have always been a major challenge in the industry. On November 28, 2017, the Russian "Union-2.1B" rocket launch failed, resulting in the destruction of 19 satellites due to software errors. The erroneous design of the control software for the Boeing 737MAX model led to two catastrophic crashes in 2018 and 2019.
Figure 2 Typical Software Incident: Mars Rover and Boeing 737-MAX Events (Image source: News)
With the increasing importance of software products in social production and life, how to improve and develop existing software engineering methods to provide more reliable guarantees for the safety and reliability of software has become a common concern in the industry and academia. Against this background, formal methods, with their rigorous mathematical theoretical foundation and continuously developing technical means, are considered to be a very promising solution.
02Development History of Formal Methods
In the 1960s, Floyd, Hoare, Manna, and others tried to prove the correctness of programs using mathematical methods and developed various program verification methods. Subsequently, the software engineering community recognized the great potential of mathematical methods, and the term 'formal methods' began to spread. Between 1969 and 1972, C.A.R. Hoare wrote two pioneering papers, 'The Axiomatic Basis of Computer Programming' and 'The Correctness of Data Representations', and proposed the concept of specification.
Based on formal semantics, formalized modeling, and formal specification, the analysis and verification problems of computer systems are transformed into logical reasoning problems or formal model judgment problems, and are verified using theorem proving tools/solvers or prototype tools of some formal models. Interactive theorem proving requires the mutual assistance of users and computers to carry out formalized proofs. The most commonly used proof assistants are Coq and Isabelle, both of which have successful application records in projects such as Airbus in the aviation field.
The basic idea of model checking is to traverse the state space of the system to verify whether the system model satisfies the given key properties, and to provide specific counterexample paths when the properties are not satisfied. For example, in safety-critical fields such as aviation, it is often used to analyze whether the system meets the given functional requirements or safety properties. Representative tools include SPIN, UPPAAL, and PRISM, which have achieved great success in the industrial field, especially in the analysis and verification of hardware systems.
Regarding the methods of theorem proving for formal verification, model checking, and so on, especially the successful applications in industries such as rail transit, aviation, aerospace, automotive electronics, and industrial control, as well as the development of related tools, we will make a more in-depth and systematic discussion in the subsequent articles.
03Introduction to Formal Methods
Formal Methods is a methodology for developing software systems based on mathematics, which provides a mathematical framework within which developers can gradually develop software through the means of defining and verifying systems in a systematic manner.
In the broad sense, formal methods refer to the application of discrete mathematics methods to solve problems in the field of software engineering, mainly including the establishment of precise mathematical models and the analysis activities of the models. In a narrow sense, formal methods are the methods of using formalized languages to carry out formalized specification description, model reasoning, and verification.
Generally speaking, formal methods emphasize the 'specification' and 'verification' of the expected functions and behaviors of software. Specification emphasizes the precise characterization of software through formalized languages, while verification emphasizes the rigorous analysis of whether the software is consistent and whether it satisfies the given properties through mathematical means. Therefore, we can consider that formal methods include two main branches: formal specification technology and formal verification technology. Both of these technologies are based on mathematical foundations, such as set theory, logic, and algebraic theories, as shown in Figure 3.
Figure 3 The structure of formal methods
Formal specification technology can be regarded as a process of formal modeling of software. Generally speaking, formal modeling requires a specific formal language, which can be basically divided into the following types:
Model-based languages
The basic idea of such formal languages is to construct models for the state features and behavioral features of the target software system using some known mathematical abstractions, including domains, tuples, sets, etc. Z, VDM, B, etc. are all model-oriented languages.
Algebraic method language
Algebraic methods use the representation of first-order logic with equality words without introducing the usual mathematical objects. Common algebraic methods include Larch, etc.
Process algebra language
Process algebra provides the necessary parallel composition, selection, and sequential composition statements for describing concurrent systems. It can also be used to verify that the system satisfies certain properties through the method of equation reasoning (equational reasoning). Common process algebra languages include CSP, etc.
Formal verification is based on established formal specifications and analyzes the relevant properties of the described system to evaluate whether the system meets the expected properties, aiming to discover inconsistencies, ambiguities, incompleteness, and other errors as much as possible. The main techniques of formal verification include theorem proving and model checking.
Theorem proving technology is the core of formal methods, and a theorem proving system is a formal system composed of a formal language and a reasoning mechanism. The reasoning mechanism consists of axioms and inference rules. The usual theorem proving process requires the support of tools. By using theorem proving technology, we can prove the properties that users expect or that the system should have, in order to eliminate ambiguity, inconsistency, insecurity, and other issues in the specifications.
Model detection is a method of automatically verifying the correctness of a system. The input of a model checker is usually a finite state model of a system and a set of temporal logic expressions representing the expected properties of the system. It determines whether the system properties are satisfied by searching all possible event sequences in the finite state model. Since the system model is finite, the search of the system state space can terminate. If the system properties hold, the model checker outputs a positive result. If the properties are not satisfied, the system outputs a counterexample represented by a sequence of states.
A simple example: }}
Suppose there is a control software in an aircraft that needs to complete flight control behavior. One of the functions is “find the non-negative square root of a given positive number”. We describe this software function in formalized language Z as shown in Figure 4.
Figure 4 Schema SquareRootSpec
The E-shaped box is called the Schema Box, which can be roughly regarded as an “operation”. The identifier SquareRootSpec at the top is called the schema name, and the horizontal line in the middle serves as a separator. The part above the horizontal line is called the declaration part, and the part below the horizontal line is the predicate part, consisting of several predicates. These predicates are formed into a complete predicate through the conjunction “∧”. In this example, radicand? and squareroot! are declared as real number types, respectively as input variables and output variables.
From this example, it can be seen that when formalized language describes software functions, it is more often through a mathematical “abstraction” to accurately describe the software to be developed. In this example, the detailed process of finding the square root is not the main object to be described, but a “relationship” is expressed through the equation “squareroot!2= radicand?”, that is, “the non-negative square root to be found, its square is equal to the number under the radical”. For software, this relationship is necessary and unique, while the way to implement the solution in code is diverse.
In this example, if we regard the pattern written in Z language as a “formal description of software requirements”, then we can further analyze and verify this formalized requirement. Assuming that we want to express “find the non-negative square root of a given positive number”, but the person writing the requirements mistakenly wrote the non-negative square root variable squareroot! as a negative square root, that is, the entire predicate part becomes “radicand?≥0 ∧ squareroot! 2= radicand? ∧ squareroot!<0”. How should we discover this defect?
Assuming that there is also a requirement checker in the process of requirement analysis, the checker can discover this defect through mathematical proof. For example, the checker can insert an assertion “squareroot! ≥0” after the predicate expression. At this time, the predicate expression should satisfy this assertion.
By means of mathematical proof, it is obviously found that “radicand?≥0 ∧ squareroot! 2= radicand? ∧ squareroot!<0” cannot lead to “squareroot! ≥0”, that is, the predicate originally written is contradictory to the given assertion.
The above example is a very simple example, used only to illustrate the simplest formalization description and analysis process. In our subsequent posts, we will gradually delve into the relevant technologies of formalization modeling and formalization verification as well as their industrial applications.
Main reference:
1. Industrial standards such as EN50128, DO-333, etc.
2. Naur P, Randell B. Software engineering: Report of a conference sponsored by the NATO science committee, Garmisch, Germany, 7th-11th October 1968[J]. 1969.
3. Randell B. Fifty years of software engineering or the view from garmisch[J]. School of Computing Science Technical Report Series, 2018.
4. Clarke E M, Wing J M. Formal Methods: State of the Art and Future Directions[J]. ACM Computing Surveys (CSUR), 1996, 28(4): 626-643.
5. Wing J M. An Introduction to Formal Methods for Specifiers[J]. Computer, 1990, 23(9): 8-22.
6. Jifeng He: A New Roadmap for Linking Theories of Programming. UTP 2016: 26-43.
7. Miao Hui kou, Chen Yi hai. 'Software Formal Specification Language—Z', published by Tsinghua University Press, November 2012.
评论已关闭