• DocumentCode
    2747806
  • Title

    Combining testing and model checking for verification of high assurance systems

  • Author

    Desovski, Dejan

  • Author_Institution
    Lane Dept. of CSEE, West Virginia Univ., Morgantown, WV, USA
  • fYear
    2004
  • fDate
    25-26 March 2004
  • Firstpage
    279
  • Lastpage
    280
  • Abstract
    Proving the correctness of a developed specification with respect to the requirements is the most important and the most difficult task in the development of high assurance systems. Studies have shown that significant number of faults in real systems can be traced back to the specifications. In this short paper, we present our initial ideas on combining formal methods and specification testing for the purposes of specification verification.
  • Keywords
    program testing; program verification; safety-critical software; formal methods; formal specification; high assurance systems; model checking; software testing; system verification; Boolean functions; Data structures; Explosions; Modeling; Performance evaluation; Space exploration; State-space methods; System testing; Systems engineering and theory; Thyristors;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    High Assurance Systems Engineering, 2004. Proceedings. Eighth IEEE International Symposium on
  • ISSN
    1530-2059
  • Print_ISBN
    0-7695-2094-4
  • Type

    conf

  • DOI
    10.1109/HASE.2004.1281758
  • Filename
    1281758