Accession Number : ADA465485


Title :   On the Need for Practical Formal Methods


Corporate Author : NAVAL RESEARCH LAB WASHINGTON DC


Personal Author(s) : Heitmeyer, Constance


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a465485.pdf


Report Date : Jan 1998


Pagination or Media Count : 10


Abstract : A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method. A fundamental assumption of this paper is that formal methods research has produced several classes of analysis that can prove useful in software development. However, to be useful to software practitioners, most of whom lack advanced mathematical training and theorem proving skills, current formal methods need a number of additional attributes, including more user- friendly notations, completely automatic (i.e., push button) analysis, and useful, easy to understand feedback. Moreover, formal methods need to be integrated into a standard development process. I discuss additional research and engineering that is needed to make the current set of formal methods more practical. To illustrate the ideas, I present several examples, many taken from the SCR (Software Cost Reduction) requirements method, a formal method that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts.


Descriptors :   *SOFTWARE ENGINEERING , COMPUTER PROGRAMS , USER FRIENDLY , COST REDUCTION


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE