{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:13:58Z","timestamp":1772043238412,"version":"3.50.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:00:00Z","timestamp":1704240000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:00:00Z","timestamp":1704240000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62062030"],"award-info":[{"award-number":["62062030"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100013142","name":"Key Research and Development Project of Hainan Province","doi-asserted-by":"publisher","award":["ZDYF2021SHFZ243"],"award-info":[{"award-number":["ZDYF2021SHFZ243"]}],"id":[{"id":"10.13039\/501100013142","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100013072","name":"Major Science and Technology Project of Hainan Province","doi-asserted-by":"publisher","award":["2020-009"],"award-info":[{"award-number":["2020-009"]}],"id":[{"id":"10.13039\/501100013072","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cloud Comp"],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Intelligent Transport System (ITS) is a typical class of Cyber-Physical Systems (CPS), and due to the special characteristics of such systems, higher requirements are placed on system security. Runtime verification is a lightweight verification technique which is used to improve the security of such systems. However, current runtime verification methods often ignore the effects of the physical environment (e.g., the effects of rain, snow, and other weather changes on road conditions), which results in the inability of the monitor to effectively monitor the system according to the changes in the environment. To address this problem, this paper proposes a method for constructing a runtime monitor with environmental context-awareness capability. First, the physical environment factors affecting the system are formally described and constructed into an environment model, then the system statute is transformed into a B\u00fcchi automaton, and then a synthesis algorithm combining the environment model and the B\u00fcchi automaton is designed based on the network of automatons, and the corresponding monitor is generated. Finally, the proposed method is applied and verified on simulation and real objects. The experimental results show that the monitors generated based on the method of this paper can effectively monitor unsafe events in different environments, thus improving the safety of intelligent driving systems.<\/jats:p>","DOI":"10.1186\/s13677-023-00567-8","type":"journal-article","created":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T13:02:25Z","timestamp":1704286945000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Context-aware environment online monitoring for safety autonomous vehicle systems: an automata-theoretic approach"],"prefix":"10.1186","volume":"13","author":[{"given":"Yu","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Sijie","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Hongyi","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Uzair","family":"Aslam\u00a0Bhatt","sequence":"additional","affiliation":[]},{"given":"Mengxing","family":"Huang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,3]]},"reference":[{"key":"567_CR1","doi-asserted-by":"crossref","unstructured":"Cheng M, Li D, Zhou N, Tang H, Wang G, Li S, Bhatti UA, Khan MK (2023) Vision-motion codesign for low-level trajectory generation in visual servoing systems. IEEE Trans Instrum Meas 72:1\u201314","DOI":"10.1109\/TIM.2023.3326234"},{"key":"567_CR2","doi-asserted-by":"publisher","first-page":"120496","DOI":"10.1016\/j.eswa.2023.120496","volume":"229","author":"UA Bhatti","year":"2023","unstructured":"Bhatti UA, Huang M, Neira-Molina H, Marjan S, Baryalai M, Tang H, Wu G, Bazai SU (2023) Mffcg-multi feature fusion for hyperspectral image classification using graph attention network. Expert Syst Appl 229:120496","journal-title":"Expert Syst Appl"},{"key":"567_CR3","doi-asserted-by":"crossref","unstructured":"Liu K, Li P, Zhang Y, Ren J, Wang X, Bhatti UA (2023) Self-awakened particle swarm optimization bn structure learning algorithm based on search space constraint. Comput Mater Continua 76(3):3257\u20133274","DOI":"10.32604\/cmc.2023.039430"},{"key":"567_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2023\/8342104","volume":"2023","author":"UA Bhatti","year":"2023","unstructured":"Bhatti UA, Tang H, Wu G, Marjan S, Hussain A (2023) Deep learning with graph convolutional networks: An overview and latest applications in computational intelligence. Int J Intell Syst 2023:1\u201328","journal-title":"Int J Intell Syst"},{"key":"567_CR5","doi-asserted-by":"publisher","first-page":"137969","DOI":"10.1016\/j.jclepro.2023.137969","volume":"417","author":"UA Bhatti","year":"2023","unstructured":"Bhatti UA, Marjan S, Wahid A, Syam M, Huang M, Tang H, Hasnain A (2023) The effects of socioeconomic factors on particulate matter concentration in china\u2019s: new evidence from spatial econometric model. J Clean Prod 417:137969","journal-title":"J Clean Prod"},{"key":"567_CR6","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"567_CR7","unstructured":"Yang D, Shi H, Dong W, Liu ZL, Zhou G (2018) Security and safety threat detection method for unmanned aerial system based on runtime verification. J Softw 29(5):1360\u20131378. http:\/\/www.jos.org.cn\/1000-9825\/5508.htm"},{"key":"567_CR8","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society, New York, p 322\u2013331"},{"issue":"2","key":"567_CR9","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 DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"567_CR10","unstructured":"Baier C, Katoen JP (2008) Principles of Model Checking. MIT press, Cambridge"},{"issue":"3","key":"567_CR11","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa\u2019Ar Y (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"key":"567_CR12","first-page":"46","volume-title":"A simple and optimal complementation algorithm for b\u00fcchi automata (LICS \u201918)","author":"JD Allred","year":"2018","unstructured":"Allred JD, Ultes-Nitsche U (2018) A simple and optimal complementation algorithm for b\u00fcchi automata (LICS \u201918). Association for Computing Machinery, New York, pp 46\u201355"},{"issue":"5","key":"567_CR13","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart C (2009) A brief account of runtime verification. J Logic Algebraic Program 78(5):293\u2013303","journal-title":"J Logic Algebraic Program"},{"key":"567_CR14","unstructured":"Wang Z (2014) Research on runtime verification of real-time systems. Master\u2019s thesis, Huazhong Normal University, Wuhan, in Chinese with English abstract"},{"key":"567_CR15","doi-asserted-by":"publisher","unstructured":"(1990) IEEE Standard Glossary of Software Engineering Terminology. In: IEEE Std 61012-1990. pp 1\u201384. https:\/\/doi.org\/10.1109\/IEEESTD.1990.101064","DOI":"10.1109\/IEEESTD.1990.101064"},{"key":"567_CR16","doi-asserted-by":"crossref","unstructured":"Bayat B, Crasta N, Crespi A, Pascoal AMS, Ijspeert AJ (2017) Environmental monitoring using autonomous vehicles: a survey of recent searching techniques. Curr Opin Biotechnol 45:76\u201384. https:\/\/api.semanticscholar.org\/CorpusID:4312879","DOI":"10.1016\/j.copbio.2017.01.009"},{"issue":"2","key":"567_CR17","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/42186.42323","volume":"6","author":"R Snodgrass","year":"1988","unstructured":"Snodgrass R (1988) A relational approach to monitoring complex systems. ACM Trans Comput Syst 6(2):157\u2013195. https:\/\/doi.org\/10.1145\/42186.42323","journal-title":"ACM Trans Comput Syst"},{"key":"567_CR18","doi-asserted-by":"publisher","unstructured":"Basin D, Klaedtke F, M\u00fcller S, Z\u0103linescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2). https:\/\/doi.org\/10.1145\/2699444","DOI":"10.1145\/2699444"},{"key":"567_CR19","doi-asserted-by":"publisher","unstructured":"Zhao C, Dong W, Qi Z (2010) Active monitoring for control systems under anticipatory semantics. In: 2010 10th International Conference on Quality Software. pp 318\u2013325. https:\/\/doi.org\/10.1109\/QSIC.2010.82","DOI":"10.1109\/QSIC.2010.82"},{"key":"567_CR20","doi-asserted-by":"publisher","unstructured":"Matos\u00a0Pedro A, Pereira D, Pinho LM, Pinto JS (2014) A compositional monitoring framework for hard real-time systems. In: Proceedings of the 6th International Symposium on NASA Formal Methods - Volume 8430. Springer-Verlag, Berlin, pp 16\u201330. https:\/\/doi.org\/10.1007\/978-3-319-06200-6_2","DOI":"10.1007\/978-3-319-06200-6_2"},{"key":"567_CR21","doi-asserted-by":"publisher","first-page":"111733","DOI":"10.1016\/j.jss.2023.111733","volume":"203","author":"M Vierhauser","year":"2023","unstructured":"Vierhauser M, Garmendia A, Stadler M, Wimmer M, Cleland-Huang J (2023) Grum - a flexible model-driven runtime monitoring framework and its application to automated aerial and ground vehicles. J Syst Softw 203:111733. https:\/\/doi.org\/10.1016\/j.jss.2023.111733","journal-title":"J Syst Softw"},{"key":"567_CR22","doi-asserted-by":"crossref","unstructured":"Heffernan D (2014) Runtime verification monitoring for automotive embedded systems using the iso 26262 functional safety standard as a guide for the definition of the monitored properties. IET Softw 8:193\u2013203(10). https:\/\/digital-library.theiet.org\/content\/journals\/10.1049\/iet-sen.2013.0236","DOI":"10.1049\/iet-sen.2013.0236"},{"key":"567_CR23","doi-asserted-by":"publisher","unstructured":"Vierhauser M, Wohlrab R, Stadler M, Cleland-Huang J (2023) Amon: A domain-specific language and framework for adaptive monitoring of cyber-physical systems. J Syst Softw 195(C). https:\/\/doi.org\/10.1016\/j.jss.2022.111507","DOI":"10.1016\/j.jss.2022.111507"},{"key":"567_CR24","doi-asserted-by":"publisher","unstructured":"Stadler M, Vierhauser M, Garmendia A, Wimmer M, Cleland-Huang J (2022) Flexible model-driven runtime monitoring support for cyber-physical systems. In: Proceedings of the ACM\/IEEE 44th International Conference on Software Engineering: Companion Proceedings (ICSE \u201922). Association for Computing Machinery, New York, pp 350\u2013351. https:\/\/doi.org\/10.1145\/3510454.3528647","DOI":"10.1145\/3510454.3528647"},{"key":"567_CR25","unstructured":"Mehmed A (2020) Runtime monitoring for safe automated driving systems. PhD thesis, M\u00e4lardalen University"},{"key":"567_CR26","doi-asserted-by":"publisher","unstructured":"Machin M, Dufoss\u00e9 F, Blanquart JP, Guiochet J, Powell D, Waeselynck H (2014) Specifying safety monitors for autonomous systems using model-checking. In: Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security - Volume 8666 (SAFECOMP 2014). Springer-Verlag, Berlin, pp 262-277. https:\/\/doi.org\/10.1007\/978-3-319-10506-2_18","DOI":"10.1007\/978-3-319-10506-2_18"},{"key":"567_CR27","unstructured":"Luo C, Wang R, Guan Y, Li X, Shi Z, Xiaoyu S (2019) Integrated modeling method of cps for real-time data. J Softw 30(7):1966\u20131979. http:\/\/www.jos.org.cn\/1000-9825\/5753.htm"},{"key":"567_CR28","doi-asserted-by":"crossref","unstructured":"Gastin P, Oddoux D (2001) Fast ltl to b\u00fcchi automata translation. In: Berry G, Comon H, Finkel A (eds) Proc. of the 13th Int\u2019l Conf. on Computer Aided Verification, LNCS, vol 2102. Springer-Verlag, Heidelberg, pp 53\u201365","DOI":"10.1007\/3-540-44585-4_6"}],"container-title":["Journal of Cloud Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13677-023-00567-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13677-023-00567-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13677-023-00567-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T13:05:46Z","timestamp":1704287146000},"score":1,"resource":{"primary":{"URL":"https:\/\/journalofcloudcomputing.springeropen.com\/articles\/10.1186\/s13677-023-00567-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,3]]},"references-count":28,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,12]]}},"alternative-id":["567"],"URL":"https:\/\/doi.org\/10.1186\/s13677-023-00567-8","relation":{},"ISSN":["2192-113X"],"issn-type":[{"value":"2192-113X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,3]]},"assertion":[{"value":"27 October 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 January 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval and consent to participate"}},{"value":"The authors read and approved the fnal manuscript.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"The authors declare no competing interests.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"6"}}