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

DOI10.1007/s00165-007-0065-0zbMath1149.68056OpenAlexW2032270529MaRDI QIDQ931435

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

CSPSpecificationTemporal logicRefinement testingRefusals

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) Temporal logic (03B44)

Related Items (7)

Formal Methods to Improve Public Administration Business Processes ⋮ Foundations for using linear temporal logic in Event-B refinement ⋮ Temporal reasoning through automatic translation of tock-CSP into timed automata ⋮ On the limits of refinement-testing for model-checking CSP ⋮ Formalisations and applications of BPMN ⋮ Property specifications for workflow modelling ⋮ Property Specifications for Workflow Modelling

Uses Software

• SPIN
• Casper

Cites Work

• Refusal testing
• Graphical versus logical specifications
• The temporal semantics of concurrent programs
• A formal language for cryptographic protocol requirements
• On the expressive power of CSP refinement
• Temporal logic can be more expressive
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Algebraic laws for nondeterminism and concurrency
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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