Automatic Verification of Combined Specifications: An Overview

DOI10.1016/j.entcs.2008.03.082zbMath1279.68217OpenAlexW2020801438MaRDI QIDQ2873685

Ernst-Ruediger Olderog

Publication date: 24 January 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.03.082

zbMATH Keywords

real-time systemsmodel checkingduration calculusCSPObject-Zabstraction refinementtool supportcomplex dataUML profile

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)

Uses Software

• Uppaal
• ARMC

Cites Work

• Model checking duration calculus: a practical approach
• A calculus of durations
• A theory of timed automata
• Duration calculus. A formal approach to real-time systems.
• Uppaal in a nutshell
• Modular proof systems for partial functions with Evans equality
• Integrating a formal method into a software engineering process with UML and Java
• Applications of Hierarchical Reasoning in the Verification of Complex Systems
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Model Checking Duration Calculus: A Practical Approach
• Slicing Concurrent Real-Time System Specifications for Verification
• Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
• Interpolation in Local Theory Extensions
• Transition predicate abstraction and fair termination
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item