Volltext-Downloads (blau) und Frontdoor-Views (grau)
  • search hit 1 of 1
Back to Result List

Formal verification made easy

  • Formal verification (FV) is considered by many to be complicated and to require considerable mathematical knowledge for successful application. We have developed a methodology in which we have added formal verification to the verification process without requiring any knowledge of formal verification languages. We use only finite-state machine notation, which is familiar and intuitive toFormal verification (FV) is considered by many to be complicated and to require considerable mathematical knowledge for successful application. We have developed a methodology in which we have added formal verification to the verification process without requiring any knowledge of formal verification languages. We use only finite-state machine notation, which is familiar and intuitive to designers. Another problem associated with formal verification is state-space explosion. If that occurs, no result is returned; our method switches to random simulation after one hour without results, and no effort is lost. We have compared FV against random simulation with respect to development time, and our results indicate that FV is at least as fast as random simulation. FV is superior in terms of verification quality, however, because it is exhaustive.show moreshow less

Export metadata

Additional Services

Share in Twitter Search Google Scholar

Statistics

frontdoor_oas
Metadaten
Author:Thomas Schlipf, Thomas Buechner, Rolf Fritz, Markus Helms, Jürgen Koehl
Publisher:IBM
Year of Publication:1997
Language:English
GND Keyword:Nachweis; Verfahren
Parent Title (English):IBM Journal of Research and Development
Volume:41
Issue:4/5
ISSN:0018-8646
First Page:567
Last Page:576
Document Type:Article (reviewed)
Open Access:Frei zugänglich
Institutes:Bibliografie
Release Date:2019/10/15
Licence (German):License LogoEs gilt das UrhG
URL:https://www.researchgate.net/publication/224103324_Formal_verification_made_easy
DOI:https://doi.org/10.1147/rd.414.0567