The Open UniversitySkip to content
 

Simplifying the Formal Verification of Safety Requirements in Zone Controllers through Problem Frames and Constraints based Projection

Yuan, Zhengheng; Chen, Xiaohong; Liu, Jing; Yu, Yijun; Sun, Haiying; Zhou, Tingliang and Jin, Zhi (2018). Simplifying the Formal Verification of Safety Requirements in Zone Controllers through Problem Frames and Constraints based Projection. IEEE Transactions on Intelligent Transportation Systems (In Press).

Full text available as:
Full text not publicly available (Accepted Manuscript)
Due to publisher licensing restrictions, this file is not available for public download
Click here to request a copy from the OU Author.
Google Scholar: Look up in Google Scholar

Abstract

Formal methods have been applied widely to verifying the safety requirements of Communication-Based Train Control (CBTC) systems, while the problem situations could be much simplified. In industrial practices of CBTC systems, however, huge complexity arises, which renders those methods nearly impossible to apply. In this paper, we aim to reduce the state space of formal verification problems in Zone Controller, a sub-system of a typical CBTC. We achieve the simplification goal by reducing the total number of device variables. To do this, two projection methods are proposed based on Problem Frames and constraints, respectively. The Problem Frames based method decomposes the system according to sub-properties through functional decomposition, whilst the constraints based projection method removes redundant variables. Our industrial case study demonstrates the feasibility though an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain.

Item Type: Journal Item
ISSN: 1558-0016
Project Funding Details:
Funded Project NameProject IDFunding Body
SAUSE: Secure, Adaptive, Usable Software EngineeringEP/R013144/1 (previous: EP/R005095/1)EPSRC (Engineering and Physical Sciences Research Council)
Keywords: Problem Frames Approach; Projection; Zone Controller; Constraints; Formal Verification
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Research Group: Centre for Research in Computing (CRC)
Item ID: 56334
Depositing User: Yijun Yu
Date Deposited: 31 Aug 2018 11:05
Last Modified: 15 Sep 2018 16:20
URI: http://oro.open.ac.uk/id/eprint/56334
Share this page:

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU