Foundations for using linear temporal logic in Event-B refinement

DOI10.1007/S00165-016-0376-0zbMATH Open1348.68039OpenAlexW2345050942WikidataQ59477094 ScholiaQ59477094MaRDI QIDQ333316FDOQ333316

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

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

Recommendations

• scientific article; zbMATH DE number 2013594
• scientific article; zbMATH DE number 1948409
• scientific article; zbMATH DE number 2227867
• The behavioural semantics of Event-B refinement
• scientific article; zbMATH DE number 1693540

zbMATH Keywords

refinementlinear temporal logicEvent-B

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Model Checking under Fairness in ProB and Its Application to Fair Exchange Protocols
• Towards Modelling Obligations in Event-B
• Title not available (Why is that?)
• Fairness and hyperfairness
• The behavioural semantics of Event-B refinement
• Specification of communicating processes: temporal logic versus refusals-based refinement

Cited In (5)

• Title not available (Why is that?)
• Trace preservation in B and Event-B refinements
• Title not available (Why is that?)
• Title not available (Why is that?)
• Refinement of Timing Constraints for Concurrent Tasks with Scheduling

Uses Software

• Rodin
• ProB
• UNITY

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

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