Formal methods

In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems.[1] The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.[2]

Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.[3]

Taxonomy

Formal methods can be used at a number of levels:

Level 0: Formal specification may be undertaken and then a program developed from this informally. This has been dubbed formal methods lite. This may be the most cost-effective option in many cases.

Level 1: Formal development and formal verification may be used to produce a program in a more formal manner. For example, proofs of properties or refinement from the specification to a program may be undertaken. This may be most appropriate in high-integrity systems involving safety or security.

Level 2: Theorem provers may be used to undertake fully formal machine-checked proofs. This can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high (e.g., in critical parts of microprocessor design).

Further information on this is expanded below.

As with programming language semantics, styles of formal methods may be roughly classified as follows:

Lightweight formal methods

Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.[4][5] They contend that the expressiveness of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various lightweight formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the Alloy object modelling notation,[6] Denney's synthesis of some aspects of the Z notation with use case driven development,[7] and the CSK VDM Tools.[8]

Uses

Formal methods can be applied at various points through the development process.

Specification

Formal methods may be used to give a description of the system to be developed, at whatever level(s) of detail desired. This formal description can be used to guide further development activities (see following sections); additionally, it can be used to verify that the requirements for the system being developed have been completely and accurately specified.

The need for formal specification systems has been noted for years. In the ALGOL 58 report,[9] John Backus presented a formal notation for describing programming language syntax (later named Backus Normal Form then renamed Backus-Naur Form (BNF)[10]). Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs wasn't completed in time for inclusion in the report. "Therefore the formal treatment of the semantics of legal programs will be included in a subsequent paper." It never appeared.

Development

Once a formal specification has been produced, the specification may be used as a guide while the concrete system is developed during the design process (i.e., realized typically in software, but also potentially in hardware). For example:

Verification

Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification (and hopefully by inference the developed system).

Human-directed proof

Sometimes, the motivation for proving the correctness of a system is not the obvious need for re-assurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of mathematical proof: handwritten (or typeset) using natural language, using a level of informality common to such proofs. A "good" proof is one which is readable and understandable by other human readers.

Critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

Automated proof

In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:

Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.

Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.

Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program which aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.

The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators[11] to get fast convergence.

Applications

Formal methods are applied in different areas of hardware and software, including routers, Ethernet switches, routing protocols, and security applications. There are several examples in which they have been used to verify the functionality of the hardware and software used in DCs. IBM used ACL2, a theorem prover, in AMD x86 processor development process. Intel uses such methods to verify its hardware and firmware (permanent software programmed into a read-only memory). Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long-lived commercial product.[12][13]

There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System, Unmanned Aircraft System integration in National Airspace System,[14] and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).[15] B-Method with AtelierB,[16] is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.

Formal verification has been frequently used in hardware by most of the well-known hardware vendors, such as IBM, Intel, and AMD. There are many areas of hardware, where Intel have used FMs to verify the working of the products, such as parameterized verification of cache coherent protocol,[17] Intel Core i7 processor execution engine validation [18] (using theorem proving, BDD’s, and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,[19] and verification of high performance dual-port gigabit Ethernet controller with a support for PCI express protocol and Intel advance management technology using Cadence.[20] Similarly, IBM has used formal methods in the verification of power gates,[21] registers,[22] and functional verification of the IBM Power7 microprocessor.[23]

Formal methods and notations

There are a variety of formal methods and notations available.

Specification languages
Model checkers

See also

References

  1. ↑ R. W. Butler (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ↑ C. Michael Holloway. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Retrieved 2006-11-16.
  3. ↑ Monin, pp.3-4
  4. ↑ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
  5. ↑ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003
  6. ↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290
  7. ↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  8. ↑ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
  9. ↑ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
  10. ↑ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
  11. ↑ A.Cortesi and M.Zanioli, Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24-42, Elsevier, ISSN 1477-8424 (2011)
  12. ↑ Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt. History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.
  13. ↑ Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings. Springer. pp. 42–61.
  14. ↑ Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.
  15. ↑ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  16. ↑ website : http://www.atelierb.eu/en/
  17. ↑ C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols,” Formal Methods in Computer-Aided Design, pp. 382-398, 2004.
  18. ↑ Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.
  19. ↑ J. Grundy, “Verified optimizations for the Intel IA-64 architecture,” In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215-232.
  20. ↑ E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC,” at Intel.
  21. ↑ C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning,” Computer Aided Verification Springer Berlin Heidelberg, pp. 433-445.
  22. ↑ P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations,” Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49-60.
  23. ↑ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems,” IBM Journal of Research and Development, vol. 55, no 3.

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

Further reading

External links

This article is issued from Wikipedia - version of the Tuesday, January 12, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.