{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:09Z","timestamp":1773827469548,"version":"3.50.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"11","license":[{"start":{"date-parts":[[2015,9,23]],"date-time":"2015-09-23T00:00:00Z","timestamp":1442966400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s11432-015-5346-2","type":"journal-article","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T19:07:57Z","timestamp":1443121677000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL","\u57fa\u4e8eAADL\u7684\u4e2d\u56fd\u9ad8\u901f\u94c1\u8def\u63a7\u5236\u7cfb\u7edf\u4e2d\u7684\u79fb\u52a8\u6388\u6743\u573a\u666f\u5efa\u6a21\u4e0e\u9a8c\u8bc1"],"prefix":"10.1007","volume":"58","author":[{"given":"Ehsan","family":"Ahmad","sequence":"first","affiliation":[]},{"given":"YunWei","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Brian","family":"Larson","sequence":"additional","affiliation":[]},{"given":"JiDong","family":"L\u00fc","sequence":"additional","affiliation":[]},{"given":"Tao","family":"Tang","sequence":"additional","affiliation":[]},{"given":"NaiJun","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,23]]},"reference":[{"key":"5346_CR1","volume-title":"CTCS-3 Technology Specification","author":"S Zhang","year":"2000","unstructured":"Zhang S. CTCS-3 Technology Specification. Beijing: China Railway Publishing House, 2000"},{"key":"5346_CR2","unstructured":"SAE International. Architecture Analysis & Design Language (AADL). SAE AS5506 Rev B, 2012"},{"key":"5346_CR3","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/978-3-642-38088-4_19","volume-title":"Proceedings of 5th International Symposium on NASA Formal Methods","author":"R B Larson","year":"2013","unstructured":"Larson R B, Chalin P, Hatcliff J. BLESS: formal specification and verification of behaviors for embedded systems with software. In: Proceedings of 5th International Symposium on NASA Formal Methods, Moffett Field, 2013. 276\u2013290"},{"key":"5346_CR4","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/2663171.2663178","volume-title":"Proceedings of ACM SIGAda Annual Conference on High Integrity Language Technology","author":"E Ahmad","year":"2014","unstructured":"Ahmad E, Larson R B, Barrett C S, et al. Hybrid annex: an AADL extention for continuous behavior and cyberphysical interaction modeling. In: Proceedings of ACM SIGAda Annual Conference on High Integrity Language Technology, Portland, 2014. 29\u201338"},{"key":"5346_CR5","first-page":"171","volume-title":"A Classical Mind Hertfordshire: Prentice Hall","author":"J He","year":"1994","unstructured":"He J. From CSP to hybrid systems. In: Roscoe W, ed. A Classical Mind Hertfordshire: Prentice Hall, 1994. 171\u2013189"},{"key":"5346_CR6","first-page":"511","volume-title":"Hybrid Systems III","author":"C Zhou","year":"1996","unstructured":"Zhou C, Wang J, Ravn P A. A formal description of hybrid systems. In: Alur R, Henzinger T A, Sontag E D, eds. Hybrid Systems III. Berlin\/Heidelberg: Springer, 1996. 511\u2013530"},{"key":"5346_CR7","first-page":"207","volume-title":"Proceedings of ICTAC Training School on Software Engineering","author":"N Zhan","year":"2013","unstructured":"Zhan N, Wang S, Zhao H. Formal modelling, analysis and verification of hybrid systems. In: Proceedings of ICTAC Training School on Software Engineering, Shanghai, 2013. 207\u2013281"},{"key":"5346_CR8","volume-title":"Technical Report CMU\/SEI-2009-TR-017","author":"P Feiler","year":"2009","unstructured":"Feiler P, Jorgen H, Niz D, et al. System architecture virtual integration: an industrial case study. Technical Report CMU\/SEI-2009-TR-017, 2009"},{"key":"5346_CR9","unstructured":"Larson R B. BLESS language reference manual. http:\/\/www.santoslab.org\/pub\/bless\/docs\/BLESS_Language_Reference_Manual.pdf"},{"key":"5346_CR10","first-page":"228","volume-title":"Proceedings of 11th International Symposium on Formal Aspects of Component Software","author":"E Ahmad","year":"2014","unstructured":"Ahmad E, Dong Y, Wang S, et al. Adding formal meanings to AADL with hybrid annex. In: Proceedings of 11th International Symposium on Formal Aspects of Component Software, Bertinoro, 2014. 228\u2013247"},{"key":"5346_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Proceedings of 8th Asian Symposium on Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu J, Lv J, Quan Z, et al. A calculus for hybrid CSP. In: Proceedings of 8th Asian Symposium on Programming Languages and Systems, Shanghai, 2010. 1\u201315"},{"key":"5346_CR12","first-page":"262","volume-title":"Proceedings of 5th International Conference on Verified Software: Theories, Tools and Experiments","author":"L Zou","year":"2013","unstructured":"Zou L, Lv J, Wang S, et al. Verifying chinese train control system under a combined scenario by theorem proving. In: Proceedings of 5th International Conference on Verified Software: Theories, Tools and Experiments, Menlo Park, 2013. 262\u2013280"},{"key":"5346_CR13","first-page":"1","volume-title":"Proceedings of 11th ACM International Conference on Embedded Software","author":"L Zou","year":"2013","unstructured":"Zou L, Zhan N, Wang S, et al. Verifying simulink diagrams via a hybrid hoare logic prover. In: Proceedings of 11th ACM International Conference on Embedded Software, Montreal, 2013. 1\u201313"},{"key":"5346_CR14","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1360\/N112014-00017","volume":"45","author":"D Guo","year":"2015","unstructured":"Guo D, Lv J, Wang S, et al. Formal analysis and verification of chinese train control system (in Chinese). Sci Sin Inform, 2015, 45: 417\u2013438","journal-title":"Sci Sin Inform"},{"key":"5346_CR15","first-page":"246","volume-title":"Proceedings of 11th Internatinal Conference on Formal Engineering Methods","author":"A Platzer","year":"2009","unstructured":"Platzer A, David Q. European train control system: a case study in formal verification. In: Proceedings of 11th Internatinal Conference on Formal Engineering Methods, Rio de Janerio, 2009. 246\u2013265"},{"key":"5346_CR16","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1109\/TITS.2012.2237509","volume":"14","author":"H Wang","year":"2013","unstructured":"Wang H, Schmid F, Chen L, et al. A topology-based model for railway train control systems. IEEE Trans Intell Transp Syst, 2013, 14: 819\u2013827","journal-title":"IEEE Trans Intell Transp Syst"},{"key":"5346_CR17","first-page":"1","volume-title":"Proceedings of International Conference on Information Engineering and Computer Science","author":"H Wang","year":"2009","unstructured":"Wang H, Tang T. On integrating component into safety critical system. In: Proceedings of International Conference on Information Engineering and Computer Science, Wuhan, 2009. 1\u20134"},{"key":"5346_CR18","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11704-012-1301-1","volume":"7","author":"J Liu","year":"2013","unstructured":"Liu J, Liu Z, He J, et al. Hybrid MARTE statecharts. Front Comput Sci, 2013, 7: 95\u2013108","journal-title":"Front Comput Sci"},{"key":"5346_CR19","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/2000367.2000368","volume":"8","author":"L Bu","year":"2011","unstructured":"Bu L, Wang Q, Chen, X, et al. Toward online hybrid systems model checking of cyber-physical systems\u2019 time-bounded short-run behavior. ACM SIGBED Rev, 2011, 8: 7\u201310","journal-title":"ACM SIGBED Rev"},{"key":"5346_CR20","first-page":"63","volume-title":"Proceedings of 4th International Conference on Mobile, Ubiquitous, and Intelligent Computing","author":"L Zhang","year":"2013","unstructured":"Zhang L, Xu B. Specification of communication based train control system using AADL. In: Proceedings of 4th International Conference on Mobile, Ubiquitous, and Intelligent Computing, Gwangju, 2013. 63\u201368"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-5346-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-015-5346-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-5346-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,22]],"date-time":"2022-05-22T06:36:07Z","timestamp":1653201367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-015-5346-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,23]]},"references-count":20,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["5346"],"URL":"https:\/\/doi.org\/10.1007\/s11432-015-5346-2","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,23]]}}}