This research paper explores the use of formal methods in software engineering to design reliable and secure software systems. Formal methods are mathematically focused languages or visual notations to specify behavior, algorithms or other types of program execution while remaining technology independent. This paper provides a brief overview of formal methods and several of the more popular implementations of formal methods in use today for software and systems development. It presents the benefits and drawbacks to formal methods, including reasons why formal methods are not commonplace for all software development. The precision of formal methods provides some opportunity for automation in the software development lifecycle including code generation and automated testing. An exploration of several problem domains where formal methods are often applied is provided. The paper concludes with discussion on the viability of formal methods as a continuing tool of software engineering.

Hinchey (2008) defines formal methods as “[…] a specification notation with formal semantics, along with a deductive apparatus for reasoning, is used to specify, design, analyze, and ultimately implement a hardware or software (or hybrid) system.” Formal methods have a relationship to some of the earliest research in algorithms and automated computation. Pure mathematics and symbolic languages were the sole means of algorithmic expression before general-purpose software languages and microprocessors. One such early incarnation of a language for computation was the Turing machine, conceived by Alan Turing in 1936. Turing machines are “[…] simple abstract computational devices intended to help investigate the extent and limitations of what can be computed.” (TM, 2009). Before automated computation was truly possible, many scientific minds were working on ways to direct a computational machine in precise ways.

Traditionally, formal methods are used in the specification and development of systems requiring high dependability, such as communication, flight control and life support. Something is dependable if its performance is constant. Reliability is the degree to which something is accurate, stable, and consistent. Security is a guarantee against loss or harm. Hanmer (2007) discusses the relationship between security and dependability, and the common quality attributes of the two when developing a system. He states that something is dependable if it exhibits reliability, maintainability, availability and integrity. Something is secure if it exhibits availability, integrity and confidentiality. The commonality between the two sets is availability and integrity. In the information technology world, the opposite of these two qualities are downtime and inconsistency - something we often see today resulting from informal software specification and lackluster development processes.

As mentioned above, formal methods can be applied in the phases of specification, design, implementation or verification of software systems. There is potential use for formal methods throughout the entire development lifecycle. Requirements for software systems typically come from stakeholders in the domain in which the software is used, such as aerospace or finance. Those requirements are provided in human-readable form and need an initial transformation into a more precise language. Software designers can refine the formal specification through a series of iterations and deliver them to developers for implementation. The architecture, functionality and quality attributes of the software can be checked against the formal specifications during peer reviews with other designers and developers. Finally, the teams responsible for testing and verification of the system’s proper operation can use the formal specifications as scripts in developing test suites for automated or manual execution.

The specifications from formal methods can be used for more than documentation of a system’s requirements and behavior. The precision in many formal methods allows the utilization of automation to reduce human error and increase consistency in the delivery of the final product. Translation of some or all of formal method languages into general-purpose computer source languages is possible, freeing the developers to concentrate on interesting refinements and optimization of the code, versus laboriously writing every line by hand. Stotts (2002) describes their project in which JUnit test cases were generated from formal method specifications. The automated approach enabled them “[…] to generate more test methods than a programmer would by following the basic JUnit practice, but our preliminary experiments show this extra work produces test suites that are more thorough and more effective at uncovering defects.” The formal methods research team at NASA Langley Research Center has developed a domain-specific formal method language called Abstract Plan Preparation Language. The research team focus and creation of the language is, “[…] to simplify the formal analysis and specification of planning problems that are intended for safety-critical applications such as power management or automated rendezvous in future manned spacecraft.” (Butler, 2006).

There are economic disadvantages of applying formal methods in software development projects. Formal methods are typically more mathematically intensive than flowcharts or other modeling notations. They are also more precise and rigorous which result in more time spent expressing the solution using a formal method notation than a visual modeling language. A developer experienced in application-level design and implementation may have less education in computational mathematics required to work with formal method notation. A primary complaint from designers and developers is that the solution must be specified twice: once in the formal method notation and again in the software language. The same argument persists in the visual modeling community, which does embrace the use of model transformation to source code to reduce the duplication of effort. The availability of formal method transformation tools to generate source code helps eliminate this issue as a recurring reason not to use formal methods.

Several formal methods are popular today, including Abstract State Machines, B-Method, Petri Nets and Z (zed) notation. Petri nets date back to 1939, Z was introduced in 1977, abstract state machines in the 1980s and B-Method is the most recent from the 1990s. Petri nets are found in the analysis of workflows, concurrency and process control. The Z formal method language is based on notations from axiomatic set theory, lambda calculus and first-order predicate logic. (Z, 2009). It was standardized by ISO in 2002. Abstract state machines resemble pseudo-code and are easy to translate into software languages. Several tools exist to verify and execute abstract state machine code, including CoreASM available on SourceForge.net. Finally, B-Method is a lower-level specification language with a wide range of tool support. It is popular in the European development community and has been used to develop safety systems for the Paris Metro rail line. (BMETH, 2009).

The use of formal methods as a way of increasing software dependability and security remains strong in industries where even partial failure can result in unacceptable loss of money, time and most importantly, life. The choice of applying formal methods in a development project is often an economic, risk-based decision. There will continue to be application programs without the budget or convenience of time to add the extra process and labor required to transform requirements into formal method specifications and then into source code. However, the pattern of formal method use remains consistent in safety and security critical systems. The development and refinement of formal methods continues into this decade, most recently with the standardization of the Z method by ISO. The activity surrounding tooling and automation to support formal methods in during the development lifecycle appears to be growing. Perhaps the software industry is closing on a point of balance among formality in specification, time to market and automation in solution development.

References

ASM. (2009). Abstract State Machines. Retrieved 11 July 2009 from http://en.wikipedia.org/wiki/Abstract_State_Machines.

BMETH. (2009). B-Method. Retrieved 11 July 2009 from http://en.wikipedia.org/wiki/B-Method.

Butler, R. W. (2006). An Abstract Plan Preparation Language. NASA Langley Research Center, Hampton, Virginia. NASA/TM-2006-214518. Retrieved 11 July 2009 from http://shemesh.larc.nasa.gov/fm/papers/Butler-TM-2006-214518-Abstract-Plan.pdf.

Hanmer, R. S., McBride, D. T., Mendiratta, V. B. (2007). Comparing Reliability and Security: Concepts, Requirements, and Techniques. Bell Labs Technical Journal 12(3), 65–78 (2007).

Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J. P., Margaria, T. (2008). Software Engineering and Formal Methods. Communications of the ACM, 51(9). September 2008.

TM. (2009). Turing machine. Retrieved 11 July 2009 from http://plato.stanford.edu/entries/turing-machine/.

Stotts, D., Lindsey, M., Antley, A. (2002). An Informal Formal Method for Systematic JUnit Test Case Generation. Technical Report TR02-012. Department of Computer Science, Univ. of North Carolina at Chapel Hill. Retrieved 11 July 2009 from http://rockfish.cs.unc.edu/pubs/TR02-012.pdf.

Z. (2009). Z notation. Retrieved 11 July 2009 from http://en.wikipedia.org/wiki/Z_notation.