Application of formal methods in train control system

CAO Yuan; TANG Tao; XU Tian-hua; MU Jian-cheng

doi:10.19818/j.cnki.1671-1637.2010.01.020

Volume 10 Issue 1

Turn off MathJax

Article Contents

Article Navigation > Journal of Traffic and Transportation Engineering > 2010 > 10(1): 112-126

CAO Yuan, TANG Tao, XU Tian-hua, MU Jian-cheng. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020

Citation:

CAO Yuan, TANG Tao, XU Tian-hua, MU Jian-cheng. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020

Citation:

PDF( 1629 KB)

Application of formal methods in train control system

doi: 10.19818/j.cnki.1671-1637.2010.01.020

1.
State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China
2.
Bureau of Science and Technology, Ministry of Railways, Beijing 100844, China

More Information

Author Bio:
CAO Yuan(1982-), male, doctoral student, +86-10-51688537, 04120041@bjtu.edu.cn

TANG Tao(1963-), male, professor, +86-10-51684228, ttang@bjtu.edu.cn
Received Date: 2009-10-18
Publish Date: 2010-02-25

Abstract

Abstract

To ensure the correctness of train control system design and development, the ways of simulation, test and formalization were compared. According to the safe critical attribute of train control system, the characters related to system safety were propounded such as real time, hybrid, distribution(concurrence) and reactivity, and the specific formal methods associated with every character were introduced in details. The analysis and classification of the methods were done based on their mathematical basis and applications, and their advantages and disadvantages were given.Analysis result indicates that every method has determinate limitations, which is determined by the essences of model checking and theory proving. It is pointed out that the presentation of new method, the expansion of existing methods and the integration of many methods will be the development trend of formalization in train control system.
- traffic information engineering,
- formal method,
- train control system,
- safe critical system

FullText(HTML)

References(46)

References

[1]	CLARKE E M, GRUMBERG O, PELED D. Model Checking[M]. Cambridge: The MIT Press, 2000.
[2]	燕飞. 轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 北京: 北京交通大学, 2006. YAN Fei. The formal modelling and model checking research of rail transportation train control system[D]. Beijing: Beijing Jiaotong University, 2006. (in Chinese)
[3]	EN 50129: 2002, rail way applications-communication, signalling and processing systems-safety related electronic systems for signalling[S].
[4]	IEC 61508-1: 1997, functional safety of electrical/electronic/programmable electronic safety-related systems[S].
[5]	ZIMMERMANN A, HOMMEL G. A train control system case study in model-based real ti me system design[C]∥ IEEE. Proceedings of the 17th International Symposium on Parallel and Distributed Processing. Washington DC: IEEE, 2003: 118-126.
[6]	ZIMMERMANN A, HOMMEL G. Towards modeling and evaluation of ETCS real-time communication and operation[J]. The Journal of Systems and Software, 2005, 77(1): 47-54. doi: 10.1016/j.jss.2003.12.039
[7]	MEYER R. Model-checking von phasen-event-automaten bezüglich duration calculus formeln mittels testautomaten[D]. Oldenburg: Universitat Oldenburg, 2005.
[8]	Subset-052, radio transmission FFFIS for Euroradio[S].
[9]	李晓山, 周巢尘. 时段演算综述[J]. 计算机学报, 1994, 17(11): 842-851. https://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm LI Xaio-shan, ZHOU Chao-chen. Duration calculi: an overview[J]. Chinese Journal of Computers, 1994, 17(11): 842-851. (in Chinese) https://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm
[10]	ZHOU C C, HANSEN M R. Duration Calculus: a Formal Approach to Real-Time Systems[M]. Essex: Springer, 2004.
[11]	MEYER R, FABERJ, HOENICKEJ, et al. Model checking duration calculus: a practical approach[J]. Formal Aspects of Computing, 2008, 20(4/5): 481-505.
[12]	FABER J. Verifying real-ti me aspects of the European train control system[C]∥ University of Copenhagen. Proceedings of the 17th Nordic Workshop on Programming Theory. Copenhagen: DIKU, 2005: 67-70.
[13]	TAPKEN J. Model-checking of duration calculus specifications[D]. Oldenburg: Universitat Oldenburg, 2001.
[14]	DIERKS H, TAPKENJ. Moby/DC—a tool for model-checking parametric real-time specifications[J]. Tools and Algorithms for the Construction and Analysis of Systems, 2003, 2619: 271-277.
[15]	SCHAFER A. Combining real-time model-checking and fault tree analysis[C]∥ Institute of Science and Technology of Information. The 12th International Formal Methods Europe Symposium. Pisa: FME, 2003: 522-541.
[16]	PLATZER A. Differential dynamic logic for verifying parametric hybrid systems[J]. Automated Reasoning with Analytic Tableaux and Related Methods, 2007, 4548: 216-232.
[17]	PLATZER A. Atemporal dynamic logic for verifying hybrid system invariants[J]. Logical Foundations of Computer Science, 2007, 4514: 457-471.
[18]	PLATZER A, QUESEL J D. Logical verification and systematic parametric analysisintrain control[J]. Lecture Notes in Computer Science, 2008, 4981: 646-649.
[19]	ZU HORSTE M M. Modelling and si mulation of train control systems using petri nets[C]∥ Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse: Springer, 1999: 1867-1883.
[20]	AVACS S3. Afault tree based model for ETCS application level 2[R]. Bonn: AVACS, 2007.
[21]	AVACS S3. Brake risk assessment for ETCStrain platoons[R]. Bonn: AVACS, 2007.
[22]	HERBSTRITT M, WI MMER R, PEIKENKAMP T, et al. Analysis of large safety-critical systems: a quantitative approach[R]. Bonn: AVACS, 2006.
[23]	BODE E, HERBSTRITT M, HERMANNS H, et al. Compositional performability evaluation for statemate[C]∥ IEEE. Third International Conference on the Quantitative Evaluation of Systems. California: IEEE, 2006: 167-178.
[24]	FABERJ, JACOBS S, VIORICAS S. Verifying CSP-OZ-DC specifications with complex data types and timing parameters[C]∥ University of Oxford. Integrated Formal Methods 2007. Oxford: University of Oxford, 2007: 233-252.
[25]	HAXTHAUSEN A E, PELESKA J. Formal development and verification of a distributed railway control system[J]. IEEE Transactions on Software Engineering, 2000, 26(8): 687-701. doi: 10.1109/32.879808
[26]	HAXTHAUSEN A E, PELESKA J. A domain specific language for rail way control systems[C]∥ ENGELS G, SAUER S. Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology. California: University of Paderborn, 2002: 1-7.
[27]	JANSENL, ZU HORSTE M M, SCHNIEDER E. Technical issues in modellingthe Europeantrain control system(ETCS) using coloured petri nets and design/CPNtools[C]∥Aarhus University. Workshop on Practical Use of Coloured Petri Nets and Design. Aarhus: Aarhus University, 1998: 103-115.
[28]	EINER S, SLOVAK R, SCHNIEDER E. Modeling train control systems with petri nets—an operational specification[C]∥IEEE. International Conference on Systems, Man, and Cybernetics. Nashville: IEEE, 2000: 3207-3211.
[29]	ZU HORSTE M M, SCHNIEDER E. Modeling train control systems with petri nets—a functional reference-architecture[C]∥IEEE. International Conference on Systems, Man, and Cybernetics. Nashville: IEEE, 2000: 3081-3086.
[30]	OLDEROG E R. Automatic verification of combined specifications: an overview[J]. Electronic Notes in Theoretical Computer Science, 2008(207): 3-16.
[31]	JOCHEN H, PATRICK M. Model-checking of specifications integrating processes, data and ti me[C]∥ FITZGERALD J, HAYESI J, TARLECKI A. International Symposium of Formal Methods Europe. Newcastle: Springer, 2005: 465-480.
[32]	JOCHEN H. Combination of processes, data, and time[D]. Oldenburg: Universitat Oldenburg, 2006.
[33]	BRÜCKNER I, WEHRHEI M H. Slicing an integrated formal method for verification[C]∥LAU K K, BANACH R. Seventh International Conference on Formal Engineering Methods. Manchester: Springer, 2005: 360-374.
[34]	BRÜCKNERI, WEHRHEI M H. Slicing object-z specifications for verification[C]∥ University of Surrey. 4th International Conference of B and Z Users. Guildford: Springer, 2005: 415-434.
[35]	GEORGE C, HAXTHAUSEN A E, HUGHES S, et al. The RAISE Development Method[M]. Hertfordshire: Prentice Hall Int, 1995.
[36]	HAXTHAUSEN A E, PELESKA J. A distributed railway control system selected proofs[R]. Kongens Lyngby: DTU, 2000.
[37]	MADSEN M S. Modelling a distributed rail way control system[D]. Kongens Lyngby: Technical University of Denmark, 2005.
[38]	XI A Y, CHRIS G. An operational semantics for timed raise[C]∥Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse: Springer, 1999: 1008-1027.
[39]	LI Li, HE Ji-feng. A denotational semantics of timed RSL using duration calculus[J]. Journal of Software, 2001, 12(6): 802-815.
[40]	KAPUR D, WI NTER V L. On the construction of a domain language for a class of reactive systems[C]∥ WINTER V L, BHATTACHARYA S. The Kluwer International Series in Engineering and Computer Science. Boston: Kluwer Academic Publishing, 2001: 169-196.
[41]	WINTER V L, KAPUR D, BERG R S. A refinement-based approachto developing software controllers for train systems[C]∥ WINTER VL, BHATTACHARYAS. The Kluwer International Series in Engineering and Computer Science. Boston: Kluwer Academic Publishing, 2001: 197-240.
[42]	WINTER V L, KAPUR D, BERG R S. Formal specification and refinement of a safe train control function[C]∥ KORDON F, LEMOI NE M. Methods for Embedded Distributed Systems: How to Master the Complexity. Boston: Kluwer Academic Publishing, 2004: 25-64.
[43]	WINTER V L, KAPUR D. Towards dynamic partitioning of reactive systembehavior: a train controller case study[C]∥KORDON F, SZTIPANOVITSJ. Reliable Systems on Unreliable Networked Platforms. Berlin: Springer, 2007: 47-69.
[44]	VIORICA S S. Hierarchic reasoning in local theory extensions[C]∥ ROBERT N. International Conference on Automated Deduction. Tallinn: Springer, 2005: 219-234.
[45]	SWENJ, VIORICAS S. Applications of hierarchical reasoning in the verification of complex systems[J]. Electronic Notes in Theoretical Computer Science, 2007, 174(8): 39-54.
[46]	NAZIR A Z. Modeling and formal specification of automated train control system using z notation[C]∥ Mohammad Ali Jinnah University. Multitopic Conference IEEE. Islamabad: IEEE, 2006: 438-443.