• DocumentCode
    2779081
  • Title

    The use of formal methods in hardware and software cannot be abandoned

  • Author

    Kapur, Deepak

  • Author_Institution
    Dept. of Comput. Sci., New Mexico Univ., Albuquerque, NM, USA
  • fYear
    2000
  • fDate
    2000
  • Firstpage
    142
  • Lastpage
    143
  • Abstract
    The title of this paper provides an answer to the question posed by Larry King in his panel paper titled "Do formal methods really belong in the toolbox of the practicing engineer?" Yes, formal methods do indeed belong to the toolbox of the practicing engineer. The capabilities of today\´s computers are truly impressive and as a result have opened door to the design and development of increasingly ambitious systems. An almost unavoidable by-product of these systems is the growing consequences associated with their failure. Another attribute shared by most of these systems is that their complexity is of an unprecedented nature. Thus, these systems live in the cross section (or shall I say cross-hairs) of high consequence and high complexity. For these reasons, attaining and developing the ability to construct highly reliable software is be coming a significant concern. Furthermore, software manufacturers as well as consumers are getting more and more fed-up with missed deadlines, bugs crashing and freezing hardware, and in the worst case, causing havoc to organizations, as bugs/incompleteness lead to allowing trojan horses for hackers through viruses and attacks. This is leading to attempts to replace ad hoc techniques in system design by more systematic methods. What is the role that formal methods, as a field of study, can play in addressing these issues? If by formal methods, one is exclusively referring to formal verification methods for software, such tools will probably not be part of a practicing engineer\´s tool in the near future. King\´s note reflects the prevailing confusion about formal methods, what can be achieved using them, and what cannot be achieved using them, and their overall role in system design and development
  • Keywords
    formal verification; software reliability; systems analysis; bugs; complexity; formal methods; formal verification methods; highly reliable software; incompleteness; system design; system design and development; trojan horses; Computer bugs; Computer crashes; Computer hacking; Computer science; Computer viruses; Hardware; Invasive software; Length measurement; Manufacturing; Software tools;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    High Assurance Systems Engineering, 2000, Fifth IEEE International Symposim on. HASE 2000
  • Conference_Location
    Albuquerque, NM
  • Print_ISBN
    0-7695-0927-4
  • Type

    conf

  • DOI
    10.1109/HASE.2000.895453
  • Filename
    895453