Modular abstractions for verifying real-time distributed systems

DOI10.1007/BF01383942MaRDI QIDQ685095zbMATH OpenFDO

Authors Hana De-Leon, Orna Grumberg

Publication date 30 September 1993

Published in Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

model checkingabstractiontemporal logicreal-time distributed systemsverification methodology

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying abstractions of timed systems
• Network invariants for real-time systems
• Network invariants for real-time systems
• Pervasive verification of distributed real-time systems
• Temporal proof methodologies for timed transition systems

Cites work

• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 177256 (Why is no real title available?)
• A really temporal logic
• Characterizing finite Kripke structures in propositional temporal logic
• Local model checking for infinite state spaces
• Local model checking in the modal mu-calculus
• Real-time logics: Complexity and expressiveness
• Tableau-based model checking in the propositional mu-calculus
• The algebra of timed processes, ATP: Theory and application

Cited in

(15)

• Theorem Proving in Higher Order Logics
• Model checking MASL specification of distributed real-time systems
• Fundamental Approaches to Software Engineering
• Predicate abstraction for dense real-time systems
• Network invariants for real-time systems
• Modularity for timed and hybrid systems
• Network invariants for real-time systems
• Formalization and correctness of the PALS architectural pattern for distributed real-time systems
• Pervasive verification of distributed real-time systems
• scientific article; zbMATH DE number 1962789 (Why is no real title available?)
• Verifying abstractions of timed systems
• Automated compositional proofs for real-time systems
• Specification and verification of distributed systems by means of the elementary-REAL language
• Modular design of real-time systems using hierarchical communicating real-time state machines
• scientific article; zbMATH DE number 4087001 (Why is no real title available?)

This page was built for publication: Modular abstractions for verifying real-time distributed systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685095)