Access Restriction

Author Frossl, J. ♦ Gerlach, J. ♦ Kropf, T.
Source IEEE Xplore Digital Library
Content type Text
Publisher Institute of Electrical and Electronics Engineers, Inc. (IEEE)
File Format PDF
Copyright Year ©1996
Language English
Subject Domain (in DDC) Technology ♦ Engineering & allied operations
Subject Keyword Logic ♦ Circuits ♦ Real time systems ♦ Delay ♦ Automata ♦ Timing ♦ Boolean functions ♦ Runtime ♦ Hardware ♦ Clocks
Abstract The verification of real-time properties requires model checking techniques for quantitative temporal structures and real-time temporal logics. However, up to now, most of those problems were solved by a translation into a standard CTL model checking problem with unit-delay structures. Although usual CTL model checkers like SMV can be used then, the translation leads to large structures and CTL formulas, such that the verification requires large computation times and only small circuits can be verified. In this paper a new model checking algorithm for quantitative temporal structures and quantitative temporal logic is presented, which avoids these drawbacks. Motivated by low level circuit verification, the implemented prover can be used for verifying general real-time systems. Although it has been proved that the complexity of the new algorithm is identical to the corresponding CTL model checking problem, the application of the new algorithms leads to significant better runtimes and larger verifiable structures. The paper presents the underlying algorithms, the complexity proof, implementational issues and concludes with experimental results, demonstrating the advantages of our approach.
Description Author affiliation: Inst. fur Rechnerentwurf und Fehlertoleranz, Karlsruhe Univ., Germany (Frossl, J.; Gerlach, J.; Kropf, T.)
ISBN 0818674245
ISSN 10661409
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research ♦ Reading
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1996-03-11
Publisher Place France
Rights Holder Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Size (in Bytes) 724.77 kB
Page Count 6
Starting Page 15
Ending Page 20

Source: IEEE Xplore Digital Library