http://iet.metastore.ingenta.com
1887

Application and benefits of formal methods in software development

Application and benefits of formal methods in software development

For access to this article, please select a purchase option:

Buy article PDF
$19.95
(plus tax if applicable)
Buy Knowledge Pack
10 articles for $120.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
Other:
 
Software Engineering Journal — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

Formal methods for software development receive much attention in research centres, but are rarely used in industry for the development of (large) software systems. One of the reasons is that little is known about the integration of formal methods in the software process, and the exact role of formal methods in the software life-cycle is still unclear. In this paper, a detailed examination is made of the application of, and the benefits resulting from, a generally applicable formal method (VDM) in a standard model for software development (DoD-STD-2167A). Currently, there is no general agreement on how formal methods should be used, but in order to analyse the use of formal methods in the software process, a clear view of such use is essential. Therefore, we show what is meant by ‘using a formal method’. The different activities of DoD-STD-2167A are analysed with regard to their suitability for applying VDM and the benefits that may result from applying VDM for that activity. Based on this analysis, an overall view on the usage of formal methods in the software process is formulated.

References

    1. 1)
      • : FM'91—Proc. Formal Methods Workshop, 1991, Drymen Scotland.
    2. 2)
      • I. Houston , S. King . (1991) CICS Project report; experiences and results from the use of Z in IBM, VDM'91; formal software development methods.
    3. 3)
      • Interim Defence Standard 00-55, May 1989.
    4. 4)
      • Interim Defence Standard 00-56, May 1989.
    5. 5)
      • D. Bjørner , C.B. Jones . (1982) , Formal specification & software development.
    6. 6)
      • C.B. Jones . (1990) , Systematic software development using VDM.
    7. 7)
      • `VDM Specification Language: Proto-Standard (Draft)', BSI IST/5/-/19, December 1991.
    8. 8)
      • P.A. Bennett , J.A. McDermid . (1991) , Software engineer's reference book.
    9. 9)
      • `Military Standard; Defense System Software Development', DoD-STD-2167A, February 1988.
    10. 10)
      • J.M. Wing . A specifier' introduction to formal methods. Computer , 9 , 8 - 22
    11. 11)
      • Bjørner, D.: `Towards a meaning of “M” in VDM', TAPSOFT'89 Proc. Int. Joint Conf. on Theory and Practice of Software Development, March 1989, Springer-Verlag, p. 1–35, (LNCS 351).
    12. 12)
      • M. Spivey . (1988) , Understanding Z — a specification language and its formal semantics.
    13. 13)
      • J.L. Peterson . Petri nets. ACM Comput. Surv. , 3 , 223 - 252
    14. 14)
      • R. Milner . (1989) , Communication and concurrency.
    15. 15)
      • C.A.R. Hoare . (1985) , Communicating sequential processes.
    16. 16)
      • Guttag, J.V., Horning, J.J., Modet, A.: `Report on the Larch shared language: Version 2.3', 58, Technical Report, April 1990.
    17. 17)
      • D.C. Luckham , F.W. Von Henke . An overview of Anna, a specification language for Ada. IEEE Softw. , 2 , 9 - 22
    18. 18)
      • R.M. Burstall , J.A. Goguen , R.S. Boyer , J.S. Moore . (1981) An informal introduction to specifications using Clear, The correctness problem in computer science.
    19. 19)
      • Ehrig, H., Fey, W., Hansen, H.: `ACT ONE: an algebraic specification language with two levels of semantics', 83-03, Technical report, 1983.
    20. 20)
      • A. Pnueli , J.W. De Bakker , W.P. de Roever , G. Rozenberg . (1986) Applications of temporal logic to the specification and verification of reactive systems, Current trends in concurrency.
    21. 21)
      • E. Brinksma . (1988) , LOTOS — a formal description technique based on the temporal ordering of observational behaviour.
    22. 22)
      • Lewington, C.P.: `Towards constructive program derivation in VDM', Proc. Tenth Conf. on Foundations of Software Technology and Theoretical Computer Science, 1990, Springer-Verlag, p. 115–132, (LNCS 472).
    23. 23)
      • J.K. Grau , K.A. Gilroy . Compliant mappings of Ada programs to the DoD-STD-2167A static structure. Ada Lett. , 2 , 73 - 84
    24. 24)
      • S. Bear , R. Jones , R. Bloomfield , L. Marshall . (1988) Structuring for the VDM specification language, VDM'88 VDM — the way ahead.
    25. 25)
      • Shaw, R.: `VDM toolset — concrete syntax for the STC VDM reference language', 725 05305, Technical Report, July 1985.
    26. 26)
      • Alford, M.W.: `Software requirements engineering methodology (SREM) at the age of four', Proc. COMSAC 4, 1980, Chicago.
    27. 27)
      • S.J. Sadler , R. Jones , R. Bloomfield , L. Marshall . (1988) Nuclear reactor protection software — an application of VDM, VDM'88 VDM — the way ahead.
    28. 28)
      • P. Zave . An operational approach to requirements specification for embedded systems. IEEE Trans. , 3 , 250 - 269
    29. 29)
      • A. Bordiga , S. Greenspan , J. Mylopoulos . Knowledge representation as the basis for requirements specification. Computer , 4 , 82 - 91
    30. 30)
      • A.M. Davis . A comparison of techniques for the specification of external system behavior. Commun. ACM , 9 , 1098 - 1115
    31. 31)
      • C. Chedgey , S. Kearney , H.J. Kugler , C.B. Jones , D. Bjørner . (1987) Using VDM in an object-oriented development method for Ada software, VDM'87 VDM — a formal method at work.
    32. 32)
      • P.G. Larsen , P.B. Lassen , S. Prehn , W.J. Toetenel . (1991) An executable subset of Meta-IV with loose specification, VDM'91 formal software development methods.
    33. 33)
      • S. Prehn , C.B. Jones , D. Bjørner . (1987) From VDM to RAISE, VDM'87 VDM — a formal method at work.
    34. 34)
      • R.J. Crispin , C.B. Jones , D. Bjørner . (1987) Experience using VDM in STC, VDM'87 VDM — a formal method at work.
    35. 35)
      • N. Plat , J. van Katwijk , K. Pronk . (1991) A case for structured analysis/formal design, VDM'91 formal software development methods.
    36. 36)
      • G.T. Scullard , R. Jones , R. Bloomfield , L. Marshall . (1988) Test case selection using VDM, VDM'88 VDM — the way ahead.
    37. 37)
      • D. O'Neill , R. Jones , R. Bloomfield , L. Marshall . (1988) VDM development with Ada as the target language, VDM'88 VDM — the way ahead.
    38. 38)
      • : `VDM'91 formal software development methods', Proc. 4th VDM Europe Symp., 1991, Noordwijkerhout The Netherlands, Springer-Verlag, LNCS 551 (Conference Contributions), LNCS 552 (Tutorials).

Related content

content/journals/10.1049/sej.1992.0034
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address