Refinement-Based Verification of Interactive Real-Time Systems

DOI10.1016/J.ENTCS.2008.06.007MaRDI QIDQ5403466zbMATH OpenOpenAlexFDO

Authors Maria Spichkova

Publication date 26 March 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.06.007

zbMATH Keywords

verificationreal-time systemsrefinementformal specificationautomotive gateway

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• An iterative approach to verification of real-time systems
• scientific article; zbMATH DE number 49713
• Specification and compositional verification of real-time systems
• Verification, refinement and scheduling of real-time programs
• scientific article; zbMATH DE number 1897216
• A specification-oriented semantics for the refinement of real-time systems
• Real-time verification techniques for untimed systems

Cites work

• Compositional refinement of interactive systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Specification and Development of Interactive Systems
• The B-Book

Cited in

(1)

• An iterative approach to verification of real-time systems

Describes a project that uses

Uses Software

• Isar
• Isabelle/Isar
• Isabelle/HOL

This page was built for publication: Refinement-Based Verification of Interactive Real-Time Systems

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