How to make FDR spin LTL model checking of CSP by refinement

DOI10.1007/3-540-45251-6_6MaRDI QIDQ2763965zbMATH OpenFDO

Authors Michael Leuschel, Thierry Massart, Andrew O. Currie

Publication date 22 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2021/20210099

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Computing methodologies and applications (68U99)

Recommendations

• On the limits of refinement-testing for model-checking CSP
• FDR3 -- a modern refinement checker for CSP
• FDR explorer
• Model Checking LTL Formulae in RAISE with FDR
• Specification of communicating processes: temporal logic versus refusals-based refinement

Cited in

(18)

• FDR explorer
• FDR: from theory to industrial application
• Temporal-logic property preservation under Z refinement
• On the limits of refinement-testing for model-checking CSP
• Translating between models of concurrency
• Integrating a formal method into a software engineering process with UML and Java
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Timed CSP = closed timed automata
• Process algebras as specification language (work in progress)
• Model checking CSP based on ASP and critical-trace model of CSP
• Model Checking LTL Formulae in RAISE with FDR
• scientific article; zbMATH DE number 7453192 (Why is no real title available?)
• Property specifications for workflow modelling
• FDR3 -- a modern refinement checker for CSP
• Communicating Sequential Processes. The First 25 Years
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Verifying data refinements using a model checker
• Specification of communicating processes: temporal logic versus refusals-based refinement

This page was built for publication: How to make FDR spin LTL model checking of CSP by refinement

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