{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T17:40:25Z","timestamp":1709401225635},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,11,13]],"date-time":"2018-11-13T00:00:00Z","timestamp":1542067200000},"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":["Front. Comput. Sci."],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1007\/s11704-018-7054-8","type":"journal-article","created":{"date-parts":[[2018,11,13]],"date-time":"2018-11-13T03:49:31Z","timestamp":1542080971000},"page":"105-129","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A verification framework for spatio-temporal consistency language with CCSL as a specification language"],"prefix":"10.1007","volume":"14","author":[{"given":"Yuanrui","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Mallet","sequence":"additional","affiliation":[]},{"given":"Yixiang","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,13]]},"reference":[{"key":"7054_CR1","first-page":"1","volume-title":"Proceedings of the 15th IEEE International Symposium on Object\/Component\/Service\u2013Oriented Real\u2013Time Distributed Computing Workshops","author":"Y Chen","year":"2012","unstructured":"Chen Y. STeC: a location\u2013triggered specification language for real\u2013time systems. In: Proceedings of the 15th IEEE International Symposium on Object\/Component\/Service\u2013Oriented Real\u2013Time Distributed Computing Workshops. 2012, 1\u20136"},{"key":"7054_CR2","first-page":"113","volume-title":"Proceedings of International Symposium on Theoretical Aspects of Software Engineering","author":"H Wu","year":"2013","unstructured":"Wu H, Chen Y, Zhang M. On denotational semantics of spatialtemporal consistency language\u2013STeC. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering. 2013, 113\u2013120"},{"issue":"8","key":"7054_CR3","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C A R Hoare","year":"1978","unstructured":"Hoare C A R. Communicating sequential processes. Communications of the ACM, 1978, 21(8): 666\u2013677","journal-title":"Communications of the ACM"},{"key":"7054_CR4","volume-title":"A Calculus of Communicating Systems. Secaucus","author":"R Milner","year":"1982","unstructured":"Milner R. A Calculus of Communicating Systems. Secaucus, NJ, USA: Springer\u2013Verlag New York, 1982"},{"issue":"1\u20133","key":"7054_CR5","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"G M Reed","year":"1988","unstructured":"Reed G M, Roscoe AW. A timed model for communicating sequential processes. Theoretical Computer Science, 1988, 58(1\u20133): 249\u2013261","journal-title":"Theoretical Computer Science"},{"key":"7054_CR6","first-page":"217","volume-title":"Proceedings of International Colloquium on Automata, Languages and Programming","author":"Y Wang","year":"1991","unstructured":"Wang Y. CCS + time = an interleaving model for real time systems. In: Proceedings of International Colloquium on Automata, Languages and Programming. 1991, 217\u2013228"},{"issue":"1","key":"7054_CR7","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L Cardelli","year":"2000","unstructured":"Cardelli L, Gordon A D. Mobile ambients. Theoretical Computer Science, 2000, 240(1): 177\u2013213","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"7054_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner R, Parrow J, Walker D. A calculus of mobile processes. Information and Computation, 1992, 100(1): 1\u201340","journal-title":"Information and Computation"},{"issue":"3","key":"7054_CR9","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s11334-008-0055-2","volume":"4","author":"C Andr\u00e9","year":"2008","unstructured":"Andr\u00e9 C, Mallet F. Clock constraint specification language: specifying clock constraints with UML\/MARTE. Innovations in Systems and Software Engineering, 2008, 4(3): 309\u2013314","journal-title":"Innovations in Systems and Software Engineering"},{"issue":"7","key":"7054_CR10","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558\u2013565","journal-title":"Communications of the ACM"},{"key":"7054_CR11","volume-title":"UML profile for MARTE: modeling and analysis of real\u2013time embedded systems","author":"OMG.","year":"2009","unstructured":"OMG. UML profile for MARTE: modeling and analysis of real\u2013time embedded systems. Technical Report, 2009"},{"key":"7054_CR12","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J P. Principles of Model Checking (Representation and Mind Series). Cambridge, Mass: The MIT Press, 2008"},{"key":"7054_CR13","volume-title":"IEEE standard for property specification language (PSL)","author":"IEEE.","year":"2010","unstructured":"IEEE. IEEE standard for property specification language (PSL). New York: Institute of Electrical and Electronics Engineers, 2010"},{"key":"7054_CR14","first-page":"141","volume-title":"Proceedings of the 18th International Symposium on Temporal Representation and Reasoning","author":"R Gascon","year":"2011","unstructured":"Gascon R, Mallet F, Deantoni J. Logical time and temporal logics: comparing UML MARTE\/CCSL and PSL. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning. 2011, 141\u2013148"},{"key":"7054_CR15","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-540-75209-7_38","volume-title":"Proceedings of the International Conference on Model Driven Engineering Languages and Systems","author":"C Andr\u00e9","year":"2007","unstructured":"Andr\u00e9 C, Mallet F, De Simone R. Modeling time(s). In: Proceedings of the International Conference on Model Driven Engineering Languages and Systems. 2007, 559\u2013573"},{"key":"7054_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"A Tutorial on UPPAAL","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen K G. A Tutorial on UPPAAL. Berlin Heidelberg: Springer, 2004, 200\u2013236"},{"key":"7054_CR17","first-page":"1","volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods","author":"J Suryadevara","year":"2013","unstructured":"Suryadevara J, Seceleanu C, Mallet F, Pettersson P. Verifying MARTE\/CCSL mode behaviors using UPPAAL. In: Proceedings of the International Conference on Software Engineering and Formal Methods. 2013, 1\u201315"},{"key":"7054_CR18","first-page":"201","volume-title":"Proceedings of Theoretical Aspects of Software Engineering Conference","author":"Y Zhang","year":"2014","unstructured":"Zhang Y, Mallet F, Chen Y. Timed automata semantics of spatialtemporal consistency language STeC. In: Proceedings of Theoretical Aspects of Software Engineering Conference. 2014, 201\u2013208"},{"key":"7054_CR19","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/j.scico.2015.03.001","volume":"106","author":"F Mallet","year":"2015","unstructured":"Mallet F, Simone R. Correctness issues on MARTE\/CCSL constraints. Science of Computer Programming, 2015, 106: 78\u201392","journal-title":"Science of Computer Programming"},{"key":"7054_CR20","volume-title":"Syntax and semantics of the clock constraint specification language (CCSL)","author":"C Andr\u00e9","year":"2009","unstructured":"Andr\u00e9 C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR\u20136925 INRIA, 2009"},{"key":"7054_CR21","volume-title":"Logical Time @ Work for the Modeling and Analysis of Embedded Systems","author":"F Mallet","year":"2011","unstructured":"Mallet F. Logical Time @ Work for the Modeling and Analysis of Embedded Systems. Saarbr\u00fccken Allemagn: LAP Lambert Academic Publishing, 2011"},{"key":"7054_CR22","first-page":"157","volume-title":"Proceedings of ACM\/IEEE International Conference on Formal Methods and Models for Codesign","author":"F Mallet","year":"2013","unstructured":"Mallet F, Millo J V, Simone R. Safe CCSL specifications and marked graphs. In: Proceedings of ACM\/IEEE International Conference on Formal Methods and Models for Codesign. 2013, 157\u2013166"},{"issue":"2","key":"7054_CR23","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183\u2013235","journal-title":"Theoretical Computer Science"},{"key":"7054_CR24","first-page":"86","volume-title":"Proceedings of the 23rd IEEE International Symposium on Rapid System Prototyping","author":"F Mallet","year":"2012","unstructured":"Mallet F. Automatic generation of observers from MARTE\/CCSL. In: Proceedings of the 23rd IEEE International Symposium on Rapid System Prototyping. 2012, 86\u201392"},{"key":"7054_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge: Cambridge University Press, 2004"},{"key":"7054_CR26","volume-title":"Unified Modeling Language Reference Manual","author":"J Rumbaugh","year":"2005","unstructured":"Rumbaugh J, Jacobson I, Booch G. Unified Modeling Language Reference Manual. Boston: Addison\u2013Wesley, 2005"},{"issue":"1","key":"7054_CR27","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s11704-014-4096-4","volume":"9","author":"Y W Chen","year":"2015","unstructured":"Chen Y W, Chen Y X, Madelaine E. Timed\u2013pNets: a communication behavioural semantic model for distributed systems. Frontiers of Computer Science, 2015, 9(1): 87\u2013110","journal-title":"Frontiers of Computer Science"},{"key":"7054_CR28","first-page":"34","volume-title":"Proceedings of the 50th International Conference on Modelling Techniques and Tools for Computer Permance Evaluation","author":"J Deantoni","year":"2012","unstructured":"Deantoni J, Mallet F. Timesquare: treat your models with logical time. In: Proceedings of the 50th International Conference on Modelling Techniques and Tools for Computer Permance Evaluation. 2012, 34\u201341"},{"key":"7054_CR29","first-page":"22","volume-title":"Proceedings of International Colloquium on Theoretical Aspects of Computing","author":"J He","year":"2013","unstructured":"He J. A clock\u2013based framework for construction of hybrid systems. In: Proceedings of International Colloquium on Theoretical Aspects of Computing. 2013, 22\u201341"},{"key":"7054_CR30","first-page":"804","volume-title":"Proceedings of IEEE International Conference on Green Computing and Communications (Green\u2013Com) and IEEE Internet of Things (iThings) and IEEE Cyber, Physical and Social Computing (CPSCom)","author":"B Xu","year":"2013","unstructured":"Xu B, Zhang L. Formal specification of cyber physical systems: three case studies based on clock theory. In: Proceedings of IEEE International Conference on Green Computing and Communications (Green\u2013Com) and IEEE Internet of Things (iThings) and IEEE Cyber, Physical and Social Computing (CPSCom). 2013, 804\u2013811"},{"key":"7054_CR31","first-page":"167","volume-title":"Proceedings of ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems","author":"C Andr\u00e9","year":"2009","unstructured":"Andr\u00e9 C, Mallet F. Specification and verification of time requirements with CCSL and Esterel. In: Proceedings of ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. 2009, 167\u2013176"},{"issue":"2","key":"7054_CR32","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"29","author":"G Berry","year":"1992","unstructured":"Berry G, Gonthier G. The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 1992, 29(2): 87\u2013152","journal-title":"Science of Computer Programming"},{"key":"7054_CR33","first-page":"65","volume-title":"Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems","author":"L Yin","year":"2011","unstructured":"Yin L, Mallet F, Liu J. Verification of MARTE\/CCSL time requirements in Promela\/Spin. In: Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems. 2011, 65\u201374"},{"issue":"5","key":"7054_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G J Holzmann","year":"1997","unstructured":"Holzmann G J. The model checker Spin. IEEE Transactions on Software Engineering, 1997, 23(5): 279\u2013295","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-7054-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-018-7054-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-018-7054-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T00:45:05Z","timestamp":1573605905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-018-7054-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,13]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["7054"],"URL":"https:\/\/doi.org\/10.1007\/s11704-018-7054-8","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,13]]},"assertion":[{"value":"16 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}