{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T09:55:11Z","timestamp":1764842111449},"reference-count":13,"publisher":"Engineering and Technology Publishing","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["jcm"],"published-print":{"date-parts":[[2017]]},"DOI":"10.12720\/jcm.12.8.482-488","type":"journal-article","created":{"date-parts":[[2018,9,14]],"date-time":"2018-09-14T04:59:02Z","timestamp":1536901142000},"page":"482-488","source":"Crossref","is-referenced-by-count":2,"title":["Formal Specification and Verification of System of Systems Using UPPAAL: A Case Study of a Defensive Missile Systems"],"prefix":"10.12720","author":[{"name":"Department of Computer Science and Engineering, Korea University, Seoul Korea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joon-Ha","family":"Jang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin-Young","family":"Choi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"4977","published-online":{"date-parts":[[2017]]},"reference":[{"key":"ref0","unstructured":"1. South Korea Future of Creation Science Division: Press Release, Oct. 9, 2013, Media It (Reuse), Feb. 24, 2014. [2] K. M. Chandy, \"Event-Driven applications: Costs, benefits and design approaches,\" California Institute of Technology, 2006."},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/apsec.2015.17","article-title":"Verifying automotive systems in EAST-ADL\/Stateflow using UPPAAL","volume-title":"Asia-Pacific Software Engineering Conference","author":"Kang","unstructured":"[3] E. Y. Kang, L. Ke, M. Z. Hua, and Y. X. Wang, \"Verifying automotive systems in EAST-ADL\/Stateflow using UPPAAL,\" presented at Asia-Pacific Software Engineering Conference, New Delhi, India, Dec. 1-4, 2015."},{"key":"ref2","unstructured":"3. E. Morris, L. Levine, C. Meyers, P. Place, and D. Plakosh, \"System of systems interoperability (SOSI): Final report,\" Technical Report, CMU\/SEI-2004-TR-004ESC-TR-2004-004April, 2004."},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/isorc.2008.25","article-title":"Cyber physical systems: Design challenges","author":"Lee","year":"2008","unstructured":"[5] E. A. Lee, \"Cyber physical systems: Design challenges,\" presented at International Symposium on Object \/ Component \/ Service-Oriented Real-Time Distributed Computing, Orlando, FL, USA, May 2008."},{"issue":"no. 4","key":"ref4","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1002\/(SICI)1520-6858(1998)1:4<267::AID-SYS3>3.0.CO;2-D","article-title":"Arichitecing principles for systems of systems","volume":"1","author":"Maier","year":"1998","unstructured":"[6] M. W. Maier, \"Arichitecing principles for systems of systems,\" Systems Engineering, vol. 1, no. 4, pp. 267-284, 1998.","journal-title":"Syst Eng","ISSN":"http:\/\/id.crossref.org\/issn\/1098-1241","issn-type":"print"},{"issue":"no. 1","key":"ref5","article-title":"Systems-of-Systems Engineering in air and missile defense","volume":"31","author":"Sommerer","year":"2012","unstructured":"[7] S. Sommerer, M. D. Guevara, M. A. Landis, J. M. Rizzuto, J. M. Sheppard, and C. J. Grant, \"Systems-of-Systems Engineering in air and missile defense,\" Johns Hopkins Apl Technical Digest, vol. 31, no. 1, 2012.","journal-title":"Johns Hopkins APL Tech Dig","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5214","issn-type":"print"},{"key":"ref6","volume-title":"Principles of Model Checking","author":"Katoen","year":"2008","unstructured":"[8] J. P. Katoen, Principles of Model Checking, MIT Press, 2008."},{"key":"ref7","first-page":"15","volume-title":"\"Synthetic structure of industrial plastics \" in Plastics","volume":"3","author":"Young","year":"1964","unstructured":"[9] G. O. Young, \"Synthetic structure of industrial plastics,\" in Plastics, 2nd ed. vol. 3, J. Peters, Ed. New York: McGraw-Hill, 1964, pp. 15-64."},{"key":"ref8","volume-title":"\"A formal framework to prove the correctness of model driven engineering composition operators \" in Lecture Notes in Computer Science","volume":"8829","author":"Kezadri","year":"2014","unstructured":"[10] M. Kezadri, M. Pantel, B. Combemale, and X. Thirioux, \"A formal framework to prove the correctness of model driven engineering composition operators,\" in Lecture Notes in Computer Science, S. Merz and J. Pang, Eds., vol. 8829, Springer, Cham, 2014."},{"issue":"no. 2","key":"ref9","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","unstructured":"[11] R. Alur and D. L. Dill, \"A theory of timed automata,\" Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.","journal-title":"Theor Comput Sci","ISSN":"http:\/\/id.crossref.org\/issn\/0304-3975","issn-type":"print"},{"key":"ref10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2004.02.055","article-title":"Semantic translation of Simulink\/Stateflow models to hybrid automata using graph transformations","volume":"109","author":"Agrawal","year":"2004","unstructured":"[12] A. Agrawal, G. Simon, and G. Karsai, \"Semantic translation of Simulink\/Stateflow models to hybrid automata using graph transformations,\" ENTCS, vol. 109, pp. 43-56, 2004.","journal-title":"ENTCS"},{"key":"ref11","unstructured":"12. K. M. Sukumar, \"Translation of simulink-stateflow models to hybrid automata,\" Ph.D. dissertation, University of Illinois, 2011."},{"key":"ref12","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","article-title":"Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems","volume":"736","author":"Alur","year":"1993","unstructured":"[14] R. Alur, C. Courcoubetis, T. Henzinger, and P. H. Ho, \"Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems,\" Hybrid Systems, vol. 736, pp. 209-229, 1993.","journal-title":"Hybrid Systems"}],"container-title":["Journal of Communications"],"original-title":[],"link":[{"URL":"http:\/\/www.jocm.us\/uploadfile\/2017\/0825\/20170825060009442.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,12]],"date-time":"2019-02-12T22:43:57Z","timestamp":1550011437000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.jocm.us\/index.php?m=content&c=index&a=show&catid=180&id=1136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":13,"URL":"https:\/\/doi.org\/10.12720\/jcm.12.8.482-488","relation":{},"ISSN":["1796-2021"],"issn-type":[{"type":"print","value":"1796-2021"}],"subject":[],"published":{"date-parts":[[2017]]}}}