Specification of communicating processes: temporal logic versus refusals-based refinement

DOI10.1007/S00165-007-0065-0MaRDI QIDQ931435zbMATH OpenOpenAlexWikidataFDO

Authors Gavin Lowe

Publication date 25 June 2008

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://ora.ox.ac.uk/objects/uuid:679c0f72-cb3b-4d18-b9df-c7626d74d659

zbMATH Keywords

CSPTemporal logicSpecificationRefinement testingRefusals

Mathematics Subject Classification ID

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

Recommendations

• Timewise refinement for communicating processes
• Timewise refinement for communicating processes
• scientific article; zbMATH DE number 1318522
• scientific article; zbMATH DE number 1693430
• Temporal-logic property preservation under Z refinement

Cites work

• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1330129 (Why is no real title available?)
• scientific article; zbMATH DE number 1786477 (Why is no real title available?)
• A formal language for cryptographic protocol requirements
• Algebraic laws for nondeterminism and concurrency
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graphical versus logical specifications
• On the expressive power of CSP refinement
• Refusal testing
• Temporal logic can be more expressive
• The temporal semantics of concurrent programs

Cited in

(14)

• Formal methods to improve public administration business processes
• Formalisations and applications of BPMN
• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• Property specifications for workflow modelling
• Synthesis of communicating process skeletons from temporal-spatial logic specifications
• A refinement calculus for specifications in Hennessy-Milner logic with recursion
• Temporal reasoning through automatic translation of tock-CSP into timed automata
• Foundations for using linear temporal logic in Event-B refinement
• A hierarchy of failures-based models: theory and application
• scientific article; zbMATH DE number 3902014 (Why is no real title available?)
• Property Specifications for Workflow Modelling
• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
• On the limits of refinement-testing for model-checking CSP
• Temporal-logic property preservation under Z refinement

Describes a project that uses

Uses Software

• Casper
• SPIN

This page was built for publication: Specification of communicating processes: temporal logic versus refusals-based refinement

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