Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
A Unified Model Checking Approach with Projection Temporal Logic
verfasst von : Zhenhua Duan, Cong Tian
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
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
This paper presents a unified model checking approach with Projection Temporal Logic (PTL) based on Normal Form Graphs (NFGs). To this end, a Modeling, Simulation and Verification Language (MSVL) is defined based on PTL. Further, normal forms and NFGs for MSVL programs and Propositional PTL (PPTL) formulas are defined. The finiteness for NFGs of MSVL programs is proved in details. Moreover, by modeling a system with an MSVL program
p
, and specifying the desirable property of the system with a PPTL formula
φ
, whether or not the system satisfies the property (whether or not
p
→
φ
is valid) can equivalently be checked by evaluating whether or not ¬(
p
→
φ
) ≡
p
∧ ¬
φ
is unsatisfiable. Finally, the satisfiability of a formula in the form of
p
∧ ¬
φ
is checked by constructing the NFG of
p
∧ ¬
φ
, and then inspecting whether or not there exist paths in the NFG.