Foundations for using linear temporal logic in Event-B refinement
- Submitting institution
-
University of Portsmouth
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 14612413
- Type
- D - Journal article
- DOI
-
10.1007/s00165-016-0376-0
- Title of journal
- Formal Aspects of Computing
- Article number
- -
- First page
- 909
- Volume
- 28
- Issue
- 6
- ISSN
- 0934-5043
- Open access status
- Out of scope for open access requirements
- Month of publication
- April
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
C - Cyber Security
- Citation count
- 3
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Safety critical industries often mandate formal verification, but some requirements could not be ‘linear temporal logic (LTL) model checked’ or ‘refinement checked’ independently. Our mathematical proofs combine both, unleashing explicit verification of infinite state systems against LTL properties under fairness. This work motivated the extension of current tooling [ProB DOI:10.1007/978-3-319-41591-8_14], used by Thales, Siemens and DeutscheBahn. Our approach is helping UK charities [DOI:10.1007/s00165-020-00512-5] access over half a billion GBP of unclaimed Gift Aid annually and HMRC [Ref: SR350506347] modernise VAT collection through split payments, bringing formal verification to new industries.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -