| [1] | 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.
|
| [2] | MEYER R. Model-checking von phasen-event-automaten bezüglich duration calculus formeln mittels testautomaten[D]. Oldenburg: Universit？t Oldenburg, 2005.
|
| [3] | Subset-052, radio transmission FFFIS for Euroradio[S].
|
| [4] | 李晓山,周巢尘.时段演算综述[J].计算机学报,1994,17(11):842-851. LI Xaio-shan, ZHOU Chao-chen. Duration calculi: an overview[J]. Chinese Journal of Computers, 1994, 17(11): 842-851.(in Chinese)
|
| [5] | ZHOU C C, HANSEN M R. Duration Calculus: a Formal Approach to Real-Time Systems[M]. Essex: Springer, 2004.
|
| [6] | MEYER R, FABER J, HOENICKE J, et al. Model checking duration calculus: a practical approach[J]. Formal Aspects of Computing, 2008, 20(4/5): 481-505.
|
| [7] | FABER J. Verifying real-time 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.
|
| [8] | TAPKEN J. Model-checking of duration calculus specifica-tions[D]. Oldenburg: Universit？t Oldenburg, 2001.
|
| [9] | DIERKS H, TAPKEN J. 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.
|
| [10] | 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.
|
| [11] | PLATZER A. Differential dynamic logic for verifying parametric hybrid systems[J]. Automated Reasoning with Analytic Tableaux and Related Methods, 2007, 4548: 216-232.
|
| [12] | PLATZER A. A temporal dynamic logic for verifying hybrid system invariants[J]. Logical Foundations of Computer Science, 2007, 4514: 457-471.
|
| [13] | PLATZER A, QUESEL J D. Logical verification and systematic parametric analysis in train control[J]. Lecture Notes in Computer Science, 2008, 4981: 646-649.
|
| [14] | ZU HORSTE M M. Modelling and simulation 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.
|
| [15] | AVACS S3. A fault tree based model for ETCS application level 2[R]. Bonn: AVACS, 2007.
|
| [16] | AVACS S3. Brake risk assessment for ETCS train platoons[R]. Bonn: AVACS, 2007.
|
| [17] | HERBSTRITT M, WIMMER R, PEIKENKAMP T, et al. Analysis of large safety-critical systems: a quantitative approach[R]. Bonn: AVACS, 2006.
|
| [18] | 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
|
| [19] | FABER J, JACOBS S, VIORICA S 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.
|
| [20] | 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.
|
| [21] | HAXTHAUSEN A E, PELESKA J. A domain specific language for railway 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.
|
| [22] | JANSEN L, ZU HORSTE M M, SCHNIEDER E. Technical issues in modelling the European train control system(ETCS)using coloured petri nets and design/CPN tools[C]∥Aarhus University. Workshop on Practical Use of Coloured Petri Nets and Design. Aarhus: Aarhus University, 1998: 103-115.
|
| [23] | 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.
|
| [24] | CLARKE E M, GRUMBERG O, PELED D. Model Check-ing[M]. Cambridge: The MIT Press, 2000.
|
| [25] | 燕 飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[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)
|
| [26] | EN 50129: 2002, railway applications-communication, sig-nalling and processing systems-safety related electronic systems for signalling[S].
|
| [27] | IEC 61508-1: 1997, functional safety of electrical/electronic/programmable electronic safety-related systems[S].
|
| [28] | ZIMMERMANN A, HOMMEL G. A train control system case study in model-based real time system design[C]∥IEEE. Proceedings of the 17th International Symposium on Parallel and Distributed Processing. Washington DC: IEEE, 2003: 118-126
|
| [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 time[C]∥FITZGERALD J, HAYES I 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: Universit？t Oldenburg, 2006.
|
| [33] | BRüCKNER I, WEHRHEIM 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üCKNER I, WEHRHEIM H. Slicing object-z specifica-tions 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 railway control system[D]. Kongens Lyngby: Technical University of Denmark, 2005.
|
| [38] | XIA 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, WINTER 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 approach to developing software controllers for train systems[C]∥WINTER V L, BHATTACHARYA S. 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, LEMOINE 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 system behavior: a train controller case study[C]∥KORDON F, SZTIPANOVITS J. Reliable Systems on Unreliable Networked Platforms. Berlin: Springer, 2007: 47-69.
|
| [44] | VIORICA S S. Hierarchic reasoning in local theory exten-sions[C]∥ROBERT N. International Conference on Automated Deduction. Tallinn: Springer, 2005: 219-234.
|
| [45] | SWEN J, VIORICA S 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.
|
