Formal Methods as Specification and Verification Tools Towards Stable Software Solutions

Adekola Olubukola D., Adebayo Adewale O.

Abstract


Formal Methods could provide mathematical models for specifying and verifying designs- hardware or software. Early on, formal methods had more acceptance in hardware than software. Employing mathematical models in software to proof correctness or validate requirements reduces or eliminates errors at the early stages of development and also makes testing easier. Formal methods are powerful tools in introducing rigor that would enforce correctness in design specification and help build confidence in design. Indeed, formal method should be seriously considered in safety-critical systems where there is zero tolerance for failure. Formal methods have possibility of gaining magnitude because of the capability to formulate accurate solutions. This work proposes to look into the effects of mathematical models on software system designs from the perspective of formal methods. Trends, benefits, state of the art and future prospects of formal method are considered. Formal methods might require much in terms of implementation, skills and use but there is much benefit in terms of removing design ambiguity and inconsistency and at the same time improving correctness and accuracy.


Keywords


Ambiguity; Correctness; Mathematical models; Requirements; Specification; Verification.

Full Text:

PDF

References


D. Bjørner. Software engineering 1: Abstraction and modelling. Theoretical Computer Science, EATCS Series. Germany: Springer-Verlag Berlin Heidelberd, 2006.

D. Bjorner. A Survey of Formal Methods in Software Engineering; DTU Informatics, Denmark, Univ. of Macau, APSEC 2012, Hong Kong.

M. Ben-Ari. Principles of the spin model checker. London: Springer-Verlag, 2008.

D. Craigen and S. Gerhart. Formal methods reality check: Industrial Usage. IEEE transactions on software engineering, Vol. 21(2), 1995, pp. 90-98.

S. King, J. Hammond, R. Chapman and A. Pryor. Is proof more cost-effective than testing? IEEE Transactions on Software Engineering, Vol. 26(8), 2000, pp. 675-685.

G. J. Holzmann. The spin model checker: Primer and reference manual. Canada: Pearson Education, Addison-Wesley, 2004.

G. Chris and P. Juan. Model checking RAISE specifications. The United Nations University, International Institute for Software Technology, Macao, China. 2006, UNU-IIST Report No. 331.

S. Gerardo. Motivation on Formal Methods Formalisms for Specification and Verification Summary. Department of Informatics, University of Oslo, 2009.

D. C. Stidolph and J. Whitehead. Managerial Issues for the Consideration and Use of Formal Methods. In: Araki K., Gnesi S., Mandrioli D. (eds.). FME 2003: Formal Methods. Lecture Notes in Computer Science, Vol 2805, Springer, Berlin, Heidelberg.

J. P. Bowen. Ten Commandments of Formal Methods. IEEE Computer, Vol. 28(4), 1995, pp. 56-63.

O. D. Adekola and O. Awodele. Enhancing Software Development through Software Product Line: Developing Product Family rather than Individual Products. International Journal of Advanced Studies in Computer Science and Engineering, Vol. 3(1), 2014, pp. 35-39.

R. W. Butler, J. L. Caldwell, V. A. Carreno, C. M. Holloway, and P. S. Miner. NASA Langley's Research and Technology-Transfer Program In Formal Methods. Assessment Technology Branch, NASA Langley Research Center, Hampton, Virginia: Vigyan, 1995.

M. Singh. Formal methods: A Complementary Support for Testing. International Journal of Advanced Research in Computer Science and Software Engineering, Vol. 3(2), 2013, pp. 320-322.

A. A. Saifan and W. B. Mustafa. Using Formal Methods for Test Case Generation According to Transition-Based Coverage Criteria. Jordanian Journal of Computers and Information Technology, Vol. 1(1), 2015, pp. 15-30.

B. Beckert and R. Hähnle. Reasoning and Verification: State of the Art and Current Trends. IEEE Intelligent Systems, http://www.computer.org/intelligent, 2014, pp. 20-29.

P. Dorsey. Top 10 Reasons Why Systems Projects Fail. NY: Dulcian, 2000.

I. Sommerville. Software engineering (9th ed.). New York: Addison Wesley, 2011.

A. E. Haxthausen. An Introduction to Formal Methods for the Development of Safety-critical Applications. DTU Informatics Technical University of Denmark, 2010, homepage.cs.uiowa.edu/~tinelli/classes/181/Fall15/Papers/Haxt10.pdf.

J. E. Hopcroft, R. Motwani and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd ed.). Boston, USA: Addison-Wesley, 2006.


Refbacks

  • There are currently no refbacks.


 

 
  

 

  


About IJC | Privacy PolicyTerms & Conditions | Contact Us | DisclaimerFAQs 

IJC is published by (GSSRR).