Formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, it is possible to verify the system's properties in a more thorough fashion than empirical testing. The phrase “mathematically rigorous” means that the specifications used in formal methods are well- formed statements in mathematical logic and that the formal verifications are rigorous deductions in that logic (i.e each step follows from a rule of inference and hence can be checked by a mechanical process)( Buth, B., Rabe, G., & Seyfarth, T. 2009).Formal method provides a symbolically way examine the entire state space of a digital design (hardware or software) and establish a correctness or safety property that is true for all possible inputs early on from specification phrase before implementation of the systems. This provides the capabilities to detect errors or faults early on in development cycle of a system. Formal method does not obviate the need for testing (Bowen 1995). Formal verification cannot fix bad assumptions in the design, but it can help identify errors in reasoning which would otherwise be left unverified. In several cases, engineers have reported finding flaws in systems once they reviewed their designs formally (kling 1995). Formal method use of relational mathematics force the user to think about the systems in several different way with the constraints of the technologies that will be use to create the system. Formal methods is normally done in three stages formal specification, verification and implementation. Formal Specification: During the formal specification phase, a modeling language is use to define the system. Modeling languages are fixed grammars which allow users to model complex structures out of predefined types. This process of formal specification is similar to the process of converting a word problem into algebraic notation.
In the verification stage the modeling language that was created is in the formal specification is tested for correctness and provablabilty by providing several properties of the specification .Implementation: Once the model has been specified and verified, it is implemented by converting the specification into code.These steps can be done by hand but would be time consume for large products. There software tools ssuch as Z, B Method and Tcal that are use in large coporations to make formal methods easier.
Benefits of formal Methods
Specifications that are done without formal methods, of some level abstraction that is leave open to one’s interpretation. In contrast to Specifications that utilize formal method that have to prove that the formal specification work by proving properties that work together. This forces the all stakeholder of the system to think more carefully about what they actually want to accomplish, since those requirements must be given in testable properties in contrast to requirements that are vague and vast. Due to the use of relational mathematics in formal specification it force the engineers, users and stakeholders of project to get to know the design, since they have to prove alternative options when define a requirement. They have to think about it in logic manner such as “that if a doesn’t happen then b need’s to happen”. This style of thinking leads engineers, user and stakeholder to gain a better understanding of the design of any system . Improved understanding can only increase the chances that that the system will be better design(Amazon).
Formal methods help’s software engineers to get the design right, which is a necessary first step toward getting the code right. If the design is broken then the code is almost certainly broken, as mistakes during coding are extremely unlikely to compensate for mistakes in design. Worse, software engineers will probably be deceived into believing that the code is ‘correct’ because it appears to correctly implement the (broken) design. Engineers are unlikely to realize that the design is incorrect while they are focusing on building the system (Newcombe 2014)
Formal Methods can be applied to the earliest stage of stage, thereby leading to earlier detection and elimination of design defects. We can systematically derive effective test cases directly from the specification. This allows the systems to be tested from early stage, when changes are made to the specification
Formal method is slowly being accepted by engineers, there exists several reasons for this, but most of the problems can be attribute to the adaption rate to the mathematics behind using formal Methods on systems. The general believe of engineers towards formal method is that you have to be a mathematician or have taken several high level Mathematics class to be able to efficiently utilize formal methods. This is false, as proven by amazon web service in which their engineers spend few weeks to learn and apply formal methods in constructive way (Newcombe ,2014).The mathematics for specification is easy, A much higher level of mathematical skill is needed if you intend to go beyond formal specification and carry out a fully formal development that includes proofs(hall 1990).The way formal method is presented makes it look intimidating because there is little clarification between formal specification and fully formal development. Which is understandable because most systems that apply formal methods are mission critical software and large corporation such as amazon and Facebook. This gives the perception that you need a large budget to teach your engineer or you have to be mathematicians to apply it or the mathematics example seems complex and will not be able apply to your simple systems.
The community around formal method is very small, doing a google search for formal method will give you results of 2.0 million search compare to object oriented at 30 million. The More narrow you search terms the less result is there for example data mining formal method google results 2.2 million compare to data mining which is 55 million. The community surrounding formal method is very small. The possibility of getting help in any specific domains is very small. This is big turn off to many people, this show how few engineers use. The size of community means it’s difficult to find people with the skills of formal method plus the skill in the domain. More people will be reluctant to try formal knowing that might not be able to replace employee with the skills rendering the initial investments a waste of money
The number of tools are limited and these tools are in the infant stage of their lifecycle which means than they can be buggy, slow to updated, not suit for every user case, and very limited in functionalities. There no guarantees say these tools will be around for a long times. The tools that available are still limited in that they do not fully integrate their self in to the development cycle or existing software developments tools that are available .
Dealing with complex language features: Formal definitions of semantics of most of the important language constructs and software system components are either not available or too complex to be useful for proving the properties of programs, these constructs or components would actually be required.Some of them are complex data structures, pointers,
human-computer interface (HCI) and error messages etc. Generally, more than half the code of any real production system consists of HCI and error messages Software systems and their social and ecological environment:
Software system normally takes inputs from external environment. These inputs may not be predictable.
There is no way to guarantee correctness and completeness of a specification (Kneuper 1997). The actually user requirement might be completely different what the user wants to accomplish/. The user might just not of the capabilities to explain in detail what they want to be able to accomplish. If the specification is false from the start formal method will be false
Because of the rigor involved, formal methods are always going to be more expensive than traditional approaches to engineering. However, given that software cost estimation is more of an art than a science, it is debatable exactly how much more expensive formal verification is. In general, formal methods involve a large initial cost followed by less consumption as the project progresses; this is a reverse from the normal cost model for software development.(Bowen 1993)
While not a universal problem, most formal methods introduce some form of computational model, usually hamstringing the operations allowed in order to make the notation elegant and the system provable. Unfortunately, these design limitations are usually considered intolerable from a developer's perspective.
An excellent example comes from SML. Statements of proof in SML depend on a purely functional programming model: all data is passed through the parameter/return mechanism of a function, no side effect alterations, modifications of global variables or the like is allowed [Paulson96]. Handling side effects and other aberrancies are a requirement for any system involving input, network operations or other systems which require interrupts, meaning that SML's model is, to some extent, broken.
Traditionally, formal methods have been judged on the richness of their descriptive model. That is, 'good' formal methods have described a wide variety of systems, and 'bad' formal methods have been limited in their descriptive capacities. While an all-encompassing formal description is attractive from a theoretical perspective, it invariably involved developing an incredibly complex and nuanced description language, which returns to the difficulties of natural language. Case studies of full formal methods often acknowledge the need for a less all-encompassing approach.(Miller 1995)
Software has grown vastly complex in both code size and functionality. So large that just to handle source code it requires new programming technique and technology to built. Due to the large nature of these code base changing them or even builted them incorrectly can be costly. By applying Formal methods into the system development cycle you able to provide early error dection and flush design faults easier. Since 2011, engineers at Amazon Web Services (AWS) have been using formal specification and model
checking to help solve difficult design problems in critical systems. Several other companies such as facebook and NASA use formal method. In fact NASA requires all mission critical software to apply formal method to their development life cycle (Holloway 1997).Formal Method will be vital role in software development in the years to come since the cost of development is increase and tool that can help reduce the cost of time and development will be of great asset to the industry.
Bowen, J. (1993, September). Formal methods in safety-critical standards. In Software Engineering Standards Symposium, 1993. Proceedings., 1993 (pp. 168-177). IEEE.
Buth, B., Rabe, G., & Seyfarth, T. (2009). Computer Safety, Reliability, and Security (1st ed., p. 203). Berlin, Heidelberg: Springer Berlin Heidelberg.
Bowen, J. P., & Hinchey, M. G. (1995). Seven more myths of formal methods. IEEE software, 12(4), 34-41.
Kling, R. (1995, October). Systems safety, normal accidents, and social vulnerability. In Computerization and controversy (2nd ed.) (pp. 746-763). Academic Press, Inc..
Kneuper, R. (1997). Limits of formal methods. Formal Aspects of Computing, 9(4), 379-394.
Miller, Steven P., and Mandayam Srivas. "Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods." Industrial-Strength Formal Specification Techniques, 1995. Proceedings., Workshop on. IEEE, 1995.
Paulson, L. C. (1996). ML for the Working Programmer. Cambridge University Press.
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., & Deardeuff, M. (2014). Use of formal methods at Amazon Web Services.
Hall, A. (1990). Seven myths of formal methods. IEEE software, 7(5), 11-19.
Holloway, C. M. (1997, October). Why engineers should consider formal methods. In Digital Avionics Systems Conference, 1997. 16th DASC., AIAA/IEEE (Vol. 1, pp. 1-3). IEEE.