2004 | OriginalPaper | Buchkapitel
Bounded Model Checking for Region Automata
verfasst von : Fang Yu, Bow-Yaw Wang, Yao-Wen Huang
Erschienen in: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
For successful software verification, model checkers must be capable of handling a large number of program variables. Traditional, BDD-based model checking is deficient in this regard, but bounded model checking (BMC) shows some promise. However, unlike traditional model checking, for which time systems have been thoroughly researched, BMC is less capable of modeling timing behavior – an essential task for verifying many types of software. Here we describe a new bounded model checker we have named xBMC, which we believe solves the reachability problem of dense-time systems. In xBMC, regions and transition relations are represented as Boolean formulae using discrete interpretations. In an experiment using well- developed model checkers to verify Fischer’s protocol, xBMC outperformed both traditional (Kronos [8], Uppaal [16], and Red [26]) and bounded (SAL [21]) model checkers by being able to verify up to 22 processes, followed by Red with 15 processes. Therefore, although xBMC is less efficient in guaranteeing system correctness, it provides an effective and practical method for timing behavior verification of large systems.