A Model-Based Quantitative Analysis Methodology for Automatic Train Operation System via Conformance Relation

Verification and validation (V&V) processes specified in international standards focus on systematic functional testing (black-box) for safety-critical systems in order to achieve the high trustworthiness of the system based on specification. However, there are different understandings of the specification which can lead to different or even error implementations. It is inefficient and not always accurate to attach most attention on manual analysis for complex Chinese Train Control System (CTCS) with automatic train operation (ATO) function. In order to verify implementations after performing a large number of repeated tests in the laboratory, the authors propose a methodology to analyze the device using input-output conformance relation (named CSPIO) based on communication sequence process (CSP). The authors model specification and implementation, respectively, and achieve quantitative results. The verification using PAT for refinement checking is automatically performed. The novelty of this approach is that it handles state spaces in a fully automated manner.

Language

  • English

Media Info

  • Media Type: Web
  • Features: References;
  • Pagination: pp 547-556
  • Monograph Title: Proceedings of the 4th International Conference on Electrical and Information Technologies for Rail Transportation (EITRT) 2019: Rail Transportation Information Processing and Operational Management Technologies
  • Serial:

Subject/Index Terms

Filing Info

  • Accession Number: 01934885
  • Record Type: Publication
  • ISBN: 9789811529146
  • Files: TRIS
  • Created Date: Oct 23 2024 9:00AM