Foundations for using linear temporal logic in Event-B refinement

DOI10.1007/S00165-016-0376-0MaRDI QIDQ333316zbMATH OpenOpenAlexWikidataFDO

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

Publication date 28 October 2016

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

refinementlinear temporal logicEvent-B

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 1693540 (Why is no real title available?)
• scientific article; zbMATH DE number 2013594 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 1863165 (Why is no real title available?)
• Appraising fairness in languages for distributed programming
• Fairness and hyperfairness
• Model checking under fairness in ProB and its application to fair exchange protocols
• Modeling in Event B. System and software engineering.
• On the limits of refinement-testing for model-checking CSP
• Specification of communicating processes: temporal logic versus refusals-based refinement
• Temporal-logic property preservation under Z refinement
• The behavioural semantics of Event-B refinement
• Towards Modelling Obligations in Event-B
• Validation of formal models by refinement animation

Cited in

(7)

• scientific article; zbMATH DE number 2013594 (Why is no real title available?)
• Automated Technology for Verification and Analysis
• Trace preservation in B and Event-B refinements
• scientific article; zbMATH DE number 2086961 (Why is no real title available?)
• scientific article; zbMATH DE number 2227867 (Why is no real title available?)
• The behavioural semantics of Event-B refinement
• Refinement of Timing Constraints for Concurrent Tasks with Scheduling

Describes a project that uses

Uses Software

• UNITY
• ProB
• Rodin

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)