Simplifying the Formal Verification of Safety Requirements in Zone Controllers through Problem Frames and Constraints based Projection
- Submitting institution
-
The Open University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1459767
- Type
- D - Journal article
- DOI
-
10.1109/TITS.2018.2869633
- Title of journal
- IEEE Transactions on Intelligent Transportation Systems
- Article number
- -
- First page
- 3517
- Volume
- 19
- Issue
- 11
- ISSN
- 1524-9050
- Open access status
- Compliant
- Month of publication
- October
- Year of publication
- 2018
- 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
-
6
- Research group(s)
-
-
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Trains need formal verification on their spatial and timing safety constraints; however, complexity of such constraints is exponential to the number of variables used in the program specification and the number of phenomena of the operating environment. This paper presents a new way to decomposing the specification through problem-based projection, simplification, and redundancy removal, coping with formal verifications at unprecedented scale. Subsequently, the approach has been embodied into a tool adopted by the world's largest PLC programming embedded systems company (Vice Dean, Casco Signal Ltd, details on request), for the formal verification of safety requirements of Shanghai City underground trains.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -