TY  - JOUR
U1  - Zeitschriftenartikel, wissenschaftlich - begutachtet (reviewed)
A1  - Schlipf, Thomas
A1  - Buechner, Thomas
A1  - Fritz, Rolf
A1  - Helms, Markus
A1  - Koehl, Jürgen
T1  - Formal verification made easy
JF  - IBM Journal of Research and Development
N2  - 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 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.
KW  - Nachweis
KW  - Verfahren
Y1  - 1997
UR  - https://www.researchgate.net/publication/224103324
SN  - 0018-8646
SS  - 0018-8646
U6  - https://doi.org/10.1147/rd.414.0567
DO  - https://doi.org/10.1147/rd.414.0567
VL  - 41
IS  - 4/5
SP  - 567
EP  - 576
PB  - IBM
ER  -