Compositional CSP traces refinement checking

DOI10.1016/J.ENTCS.2009.08.022MaRDI QIDQ5178982zbMATH OpenOpenAlexFDO

Authors Daniel Wonisch, Heike Wehrheim

Publication date 18 March 2015

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.2009.08.022

zbMATH Keywords

learningCSPcompositional verificationrefinementassume-guarantee rule

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) 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

• scientific article; zbMATH DE number 1956591
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Automatic symbolic compositional verification by learning assumptions
• Refining Interface Alphabets for Compositional Verification
• Computer Aided Verification

Cites work

• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1903348 (Why is no real title available?)
• 25 years of model checking. History, achievements, perspectives
• Communicating sequential processes
• Concurrency verification. Introduction to compositional and noncompositional methods
• Inference of finite automata using homing sequences
• Insights to Angluin's learning
• Learning regular sets from queries and counterexamples
• Proofs of Networks of Processes
• Using partial orders for the efficient verification of deadlock freedom and safety properties

Cited in

(3)

• Assumption-commitment support for CSP model checking
• SAT-solving in CSP trace refinement
• Integrated Formal Methods

Describes a project that uses

Uses Software

• FDR2

This page was built for publication: Compositional CSP traces refinement checking

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