Formal methods are system design techniques that create software and hardware systems using a strictly specified mathematical model. Unlike other design systems, formal methods use mathematical proofs as a complement to system testing to ensure correct operation. As systems become more complex and security becomes an increasingly important issue, a formal approach to system design provides another layer of assurance. It is very important to note that formal validation does not rule out the need for testing. Formal verification can't correct bad design assumptions, but it helps identify flaws in thinking that would otherwise remain unconfirmed. In some cases, engineers report finding a bug in the system after a formal review of the design. Broadly speaking, formal design can be thought of as a three-step process that follows the following scheme.
1. Formal Specification: In the formal specification phase, engineers use a modeling language to strictly define the system. A modeling language is a fixed grammar that allows users to model complex structures from predefined types. The process of this formal specification is similar to the process of converting a word problem into algebraic notation. In many respects, this step in the formal design process is similar to the formal software engineering techniques developed by Rumbaugh, Booch, and others. At the very least, both techniques help engineers clearly define problems, goals, and solutions. However, the formal modeling language is more tightly defined. The formal grammar distinguishes between WFF (a logical expression) and NonWFF (a syntactically incorrect instruction). Already at this stage, the difference between WFF and non-WFF helps specify the design. Several engineers who have used the formal specification have stated that the clarity itself created at this stage is an advantage.
2. Verification: As mentioned above, formal methods differ from other specification systems in that they focus on provability and accuracy. By building a system using a formal specification, the designer is actually developing a set of theorems about his system. By proving these theorems correct, the formal. Verification is a difficult process, largely because even the simplest system has several dozen theorems, each of which has to be proven. Even a traditional mathematical proof is a complex affair, Wiles` proof of Fermat's Last Theorem, for example, took several years after its announcement to be completed. Given the demands of complexity and Moore's law, almost all formal systems use an automated theorem proving tool of some form. These tools can prove simple theorems, verify the semantics of theorems, and provide assistance for verifying more complicated proofs.
3. Implementation: After the model is specified and validated, the model is implemented by converting the specification into code. As the distinction between software and hardware design became narrower, formal methods for designing embedded systems emerged. For example, LARCH has a VHDL implementation. Similarly, hardware systems such as VIPER and AAMP5 processors have been developed using a formal approach.
Key concepts of formal methods:
Provability and automated verification: Formal methods differ from other specification systems in that they focus on accuracy and proof. This is ultimately another measure of system integrity. Evidence is a supplement, not an alternative to testing. Testing is an important part of ensuring the suitability of any system, but it is finite. Testing cannot show that the system is functioning properly. It can only show that the system is working in the tested cases. Testing does not show that the system works outside the tested case, so formal proof is required. Formal proof of computer system is not a new idea. Knuth and Dijkstra have written extensively on this subject, but their proofs are based on traditional mathematical methods. In pure science, evidence is verified through extensive peer review prior to publication. Such techniques are time consuming and far from perfect. It is not uncommon for published proofs to contain errors. Given the cost and time requirements of system engineering, traditional testing techniques are not really applicable. Due to the cost of manual verification, most formal methods use an automated theorem proving system to validate the design. The automated theorem prover can best be described as a mathematical CAD tool. These automatically prove simple theorems and help check more complex theorems.
Advantages:
Formal methods offer additional benefits beyond provability, and these benefits are worth mentioning. However, most of these benefits are available from other systems and usually do not have the sharp learning curve required by formal methods.
Discipline- Formal systems require engineers to think more thoroughly about their designs because of their rigor. In particular, formal justification requires rigorous specification of goals, not just operations. This thorough approach helps identify defective inferences much faster than traditional designs. Formal specification discipline has also been proven in existing systems. For example, an engineer using a PVS system reported that one of the microprocessor designs identified multiple microcode errors.
Precision- Traditionally, as the weaknesses of natural language writing became more apparent, we moved to jargon and formal notation. There is no reason that systems engineering should differ, and there are several formal methods which are used almost exclusively for notation. For engineers designing safety critical systems, the benefits of formal methods lie in their clarity. Unlike many other design approaches, the formal verification requires very clearly defined goals and approaches. In a safety critical system, ambiguity can be extremely dangerous, and one of the primary benefits of the formal approach is the elimination of ambiguity.
Disadvantage:
Bowen points out that formal methods are generally suspected by the professional engineering community, and that preliminary case studies and dissertation tendencies advocating formal methods seem to favor his dissertation. [Bowen93]. There are several reasons why formal methods are not used so often, most of them due to the exaggeration of supporters of formal methods.
Cost- Due to the strict relationship, formal methods are always costlier than traditional approaches to engineering. However, it is arguable how expensive formal verification is, as software cost estimates are more art than science. Formal methods generally have higher initial costs and consume less as the project progresses. This is the opposite of the normal software development cost model.
Computation Model Limitations- This is not a universal problem, but most formal methods introduce some form of computation model and usually do the operations allowed to make the notation elegant and proof of the system. Limit. Unfortunately, from a developer's point of view, these design limitations are usually considered intolerable.
Usability- Traditionally, formal methods have been judged on the basis of their abundance of descriptive models. That is, "good" formal methods describe different systems, and "bad" formal methods have limited ability to describe them. From a theoretical point of view, a comprehensive formal explanation is appealing, but the goal has always been to develop an incredibly complex and subtle explanation language that takes advantage of the difficulties of natural language. Fully formal method case studies often recognize the need for a more comprehensive approach.
The Lightweight approach:
In recent years, the focus has been on formal specification flaws and several alternative approaches have emerged. The traditional view of formal methods as a comprehensive and highly abstracted scheme has led to formal methods being inclusive, very rigorous and very expensive. Although attractive in theory, formal methods have generally been ignored by engineers in this area. A lightweight approach to formal design recognizes that formal methods are not a panacea. There are areas where formal methods are useful and areas where formal specifications are not. Lightweight designs use formal methods in specific locations and can be used in different subsystems. Ideally, take advantage of each method. In such systems, Petri nets can be used to describe communication protocols and LARCH systems can be used to model data storage. For the rest of the system, the formal specification can be omitted altogether. For example, you can use the rapid prototyping system and customer interviews to improve the user interface.
Available tools, techniques, and metrics
Larch: Unlike most formal systems, LARCH provides two levels of specification. A general high-level modeling language, and a collection of implementation dialects designed to work with specific programming languages.
SML: Standard Meta-Language is a strongly typed functional programming language originally designed for exploring ideas in type theory. SML has become the formal methods workhorse because of its strong typing and provability features.
HOL: HOL, short for Higher Order Logic, is an automated theorem proving system. As with most automated theorem proving systems, HOL is a computer-aided proof tool: it proves simple theorems and assists in proving more complicated statements, but is still dependent on interaction with a trained operator. HOL has been extensively used for hardware verification, the VIPER chip being a good example.
Petri Nets: Petri Nets are a good example of a very 'light' formal specification. Originally designed for modeling communications, Petri Nets are a graphically simple model for asynchronous processes.
