{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:57Z","timestamp":1750308717234,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,12,1]],"date-time":"2013-12-01T00:00:00Z","timestamp":1385856000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Thomas Gessmann-Stiftung, Essen, Germany"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2013,12]]},"abstract":"<jats:p>Many future Driver-Assistance-Systems (DAS) will use components not permanently mounted to the vehicle. Unlike state-of-the-art DAS with static configurations, the system and software architecture changes at runtime. To handle configuration changes, Service Oriented Architecture (SOA) and automatic orchestration is a promising approach. Whenever systems are set up automatically, they have to be validated. This paper presents an approach based on formal methods. Existing component models are annotated with Quality-of-Service parameters and transformed automatically to Hybrid Automata. These automata are then composed to an overall system model and model checking is used to check safety properties. The complete transformation-orchestration-validation process is executed without user interaction and thus can be performed at runtime.<\/jats:p>","DOI":"10.1145\/2583687.2583699","type":"journal-article","created":{"date-parts":[[2014,2,25]],"date-time":"2014-02-25T13:20:45Z","timestamp":1393334445000},"page":"49-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal verification of service-oriented adaptive driver assistance systems"],"prefix":"10.1145","volume":"10","author":[{"given":"Christian","family":"Schwarz","sequence":"first","affiliation":[{"name":"Universit\u00e4t Koblenz-Landau, Koblenz, Germany"}]},{"given":"Dieter","family":"Z\u00f6bel","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Koblenz-Landau, Koblenz, Germany"}]},{"given":"Marco","family":"Wagner","sequence":"additional","affiliation":[{"name":"Hochschule Heilbronn, Germany"}]}],"member":"320","published-online":{"date-parts":[[2013,12]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"174","volume-title":"2011 4rd IEEE International Conference on","author":"Wagner M.","year":"2011","unstructured":"M. Wagner , D. Zoebel , and A. Meroth , \" Towards an adaptive software and system architecture for driver assistance systems,\" in Computer Science and Information Technology (ICCSIT) , 2011 4rd IEEE International Conference on , 2011 , pp. 174 -- 178 . M. Wagner, D. Zoebel, and A. Meroth, \"Towards an adaptive software and system architecture for driver assistance systems,\" in Computer Science and Information Technology (ICCSIT), 2011 4rd IEEE International Conference on, 2011, pp. 174--178."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.473.0377"},{"key":"e_1_2_1_3_1","volume-title":"1st Workshop (APRES 2012)","author":"Wagner M.","year":"2012","unstructured":"M. Wagner , A. Meroth , and D. Zoebel , \" Model-driven development of SOA-based driver assistance systems,\" in Adaptive and Reconfigurable Embedded Systems , 1st Workshop (APRES 2012) , 2012 . M. Wagner, A. Meroth, and D. Zoebel, \"Model-driven development of SOA-based driver assistance systems,\" in Adaptive and Reconfigurable Embedded Systems, 1st Workshop (APRES 2012), 2012."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2330667.2330686"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8237-7","volume-title":"Real-Time Systems: Design Principles for Distributed Embedded Applications","author":"Kopetz H.","year":"2011","unstructured":"H. Kopetz , Real-Time Systems: Design Principles for Distributed Embedded Applications , 2 nd ed. Springer , 2011 . H. Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications, 2nd ed. Springer, 2011.","edition":"2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_2_1_7_1","first-page":"278","volume-title":"IEEE Computer Society","author":"Henzinger T. A.","year":"1996","unstructured":"T. A. Henzinger , \"The theory of hybrid automata,\" in Proceedings of the 11th Annual Symposium on Logic in Computer Science . IEEE Computer Society , 1996 , pp. 278 -- 292 . T. A. Henzinger, \"The theory of hybrid automata,\" in Proceedings of the 11th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 1996, pp. 278--292."},{"key":"e_1_2_1_8_1","volume-title":"Model checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled , Model checking . The MIT Press , 1999 . E. Clarke, O. Grumberg, and D. Peled, Model checking. The MIT Press, 1999."},{"key":"e_1_2_1_9_1","first-page":"11","article-title":"Visual steering assistance for backing-up vehicles with one-axle trailer","author":"Berg U.","year":"2006","unstructured":"U. Berg and D. Zoebel , \" Visual steering assistance for backing-up vehicles with one-axle trailer ,\" in Vision in Vehicles 11 , 2006 . U. Berg and D. Zoebel, \"Visual steering assistance for backing-up vehicles with one-axle trailer,\" in Vision in Vehicles 11, 2006.","journal-title":"Vision in Vehicles"},{"volume-title":"The Object Management Group","year":"2009","key":"e_1_2_1_10_1","unstructured":"Service oriented architecture Modeling Language (SoaML) - Specification for the UML Profile and Metamodel for Services (UPMS) 1.0 Beta 2 , The Object Management Group , 2009 . Service oriented architecture Modeling Language (SoaML) - Specification for the UML Profile and Metamodel for Services (UPMS) 1.0 Beta 2, The Object Management Group, 2009."},{"key":"e_1_2_1_11_1","series-title":"32nd Annual German Conference on Artificial Intelligence","first-page":"695","volume":"5803","author":"Mohammed A.","year":"2009","unstructured":"A. Mohammed and C. Schwarz , \" HieroMate: A graphical tool for specification and verification of hierarchical hybrid automata,\" in KI 2009 , 32nd Annual German Conference on Artificial Intelligence , ser. LNAI , vol. 5803 . Springer , 2009 , pp. 695 -- 702 . A. Mohammed and C. Schwarz, \"HieroMate: A graphical tool for specification and verification of hierarchical hybrid automata,\" in KI 2009, 32nd Annual German Conference on Artificial Intelligence, ser. LNAI, vol. 5803. Springer, 2009, pp. 695--702."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/827267.828918"},{"key":"e_1_2_1_13_1","volume-title":"Using CLP to model hybrid systems,\" in Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP)","author":"Mohammed A.","year":"2008","unstructured":"A. Mohammed and U. Furbach , \" Using CLP to model hybrid systems,\" in Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP) , 2008 . A. Mohammed and U. Furbach, \"Using CLP to model hybrid systems,\" in Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP), 2008."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2011.14"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.005"},{"key":"e_1_2_1_16_1","first-page":"152","volume-title":"18th IEEE International Conference","author":"Foster H.","year":"2003","unstructured":"H. Foster , S. Uchitel , J. Magee , and J. Kramer , \" Model-based verification of web service compositions,\" in Automated Software Engineering , 18th IEEE International Conference , 2003 , pp. 152 -- 161 . H. Foster, S. Uchitel, J. Magee, and J. Kramer, \"Model-based verification of web service compositions,\" in Automated Software Engineering, 18th IEEE International Conference, 2003, pp. 152--161."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.11"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2009.2026451"},{"key":"e_1_2_1_19_1","series-title":"2nd International Conference","first-page":"645","volume":"1723","author":"Firley T.","year":"1999","unstructured":"T. Firley , M. Huhn , K. Diethers , T. Gehrke , and U. Goltz , \" Timed sequence diagrams and tool-based analysis - a case study,\" in UML'99: The Unified Modeling Language - Beyond the Standard , 2nd International Conference , ser. LNCS , vol. 1723 . Springer , 1999 , pp. 645 -- 660 . T. Firley, M. Huhn, K. Diethers, T. Gehrke, and U. Goltz, \"Timed sequence diagrams and tool-based analysis - a case study,\" in UML'99: The Unified Modeling Language - Beyond the Standard, 2nd International Conference, ser. LNCS, vol. 1723. Springer, 1999, pp. 645--660."},{"key":"e_1_2_1_20_1","volume-title":"IEEE","author":"Hendriks M.","year":"2006","unstructured":"M. Hendriks and M. Verhoef , \" Timed automata based analysis of embedded system architectures,\" in 20th International Parallel and Distributed Processing Symposium . IEEE , 2006 . M. Hendriks and M. Verhoef, \"Timed automata based analysis of embedded system architectures,\" in 20th International Parallel and Distributed Processing Symposium. IEEE, 2006."}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2583687.2583699","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2583687.2583699","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:26Z","timestamp":1750277666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2583687.2583699"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["10.1145\/2583687.2583699"],"URL":"https:\/\/doi.org\/10.1145\/2583687.2583699","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2013,12]]},"assertion":[{"value":"2013-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}