Automatic verification of combined specifications: an overview

DOI10.1016/J.ENTCS.2008.03.082MaRDI QIDQ2873685zbMATH OpenOpenAlexFDO

Authors Ernst-Rüdiger 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

abstraction refinementcomplex dataCSPduration calculusmodel checkingObject-Zreal-time systemstool supportUML 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)

Recommendations

• Automated Technology for Verification and Analysis
• Decomposing Integrated Specifications for Verification
• Automated formal analysis and verification: an overview
• A framework for combining analysis and verification

Cites work

• A calculus of durations
• A theory of timed automata
• Applications of hierarchical reasoning in the verification of complex systems
• Automated Deduction – CADE-20
• Automated reasoning in some local exensions of ordered structures
• Constraint Solving for Interpolation
• Duration calculus. A formal approach to real-time systems.
• FM 2005: Formal Methods
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• scientific article; zbMATH DE number 995939 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 2143088 (Why is no real title available?)
• scientific article; zbMATH DE number 1409638 (Why is no real title available?)
• Integrating a formal method into a software engineering process with UML and Java
• Interpolation in Local Theory Extensions
• Model checking duration calculus: a practical approach
• Model Checking Duration Calculus: A Practical Approach
• Modular proof systems for partial functions with Evans equality
• Optimizing slicing of formal specifications by deductive verification
• Slicing Concurrent Real-Time System Specifications for Verification
• Transition predicate abstraction and fair termination
• Uppaal in a nutshell
• Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters

Cited in

(6)

• Slicing Concurrent Real-Time System Specifications for Verification
• Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
• scientific article; zbMATH DE number 2143088 (Why is no real title available?)
• scientific article; zbMATH DE number 2086955 (Why is no real title available?)
• Automated Technology for Verification and Analysis
• FM 2005: Formal Methods

Describes a project that uses

Uses Software

• Uppaal
• ARMC

This page was built for publication: Automatic verification of combined specifications: an overview

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