Foundations for using linear temporal logic in Event-B refinement

DOI10.1007/s00165-016-0376-0zbMath1348.68039OpenAlexW2345050942WikidataQ59477094 ScholiaQ59477094MaRDI QIDQ333316

David M. Williams, Helen Treharne, Thai Son Hoang, S. A. Schneider

Publication date: 28 October 2016

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

Full work available at URL: https://doi.org/10.1007/s00165-016-0376-0

zbMATH Keywords

refinementlinear temporal logicEvent-B

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Trace preservation in B and Event-B refinements

Uses Software

• Rodin
• ProB
• UNITY

Cites Work

• The behavioural semantics of Event-B refinement
• Specification of communicating processes: temporal logic versus refusals-based refinement
• Appraising fairness in languages for distributed programming
• Temporal-logic property preservation under Z refinement
• On the limits of refinement-testing for model-checking CSP
• Validation of formal models by refinement animation
• Model Checking under Fairness in ProB and Its Application to Fair Exchange Protocols
• Towards Modelling Obligations in Event-B
• Fairness and hyperfairness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Foundations for using linear temporal logic in Event-B refinement