{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T05:08:12Z","timestamp":1761973692720,"version":"build-2065373602"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,5,3]],"date-time":"2013-05-03T00:00:00Z","timestamp":1367539200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,5]]},"DOI":"10.1007\/s10270-013-0342-8","type":"journal-article","created":{"date-parts":[[2013,5,2]],"date-time":"2013-05-02T18:37:39Z","timestamp":1367519859000},"page":"839-859","source":"Crossref","is-referenced-by-count":2,"title":["Formal synthesis of application and platform behaviors of embedded software systems"],"prefix":"10.1007","volume":"14","author":[{"given":"Jinhyun","family":"Kim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inhye","family":"Kang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin-Young","family":"Choi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sungwon","family":"Kang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,5,3]]},"reference":[{"key":"342_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 1633, p. 688. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_3"},{"key":"342_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: The theory of timed automata. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop, pp. 45\u201373. Springer, London (1992)","DOI":"10.1007\/BFb0031987"},{"key":"342_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04995-2","volume-title":"Process Algebra with Timing","author":"JCM Baeten","year":"2002","unstructured":"Baeten, J.C.M., Middelburg, C.A., Middelburg, K.: Process Algebra with Timing. Springer, Secaucus (2002)"},{"key":"342_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Revised Lectures, Lecture Notes in Computer Science, vol. 3185, pp. 200\u2013237. Springer, Berlin (2004). http:\/\/doc.utwente.nl\/51010\/","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"342_CR5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19, 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"342_CR6","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M Butler","year":"2000","unstructured":"Butler, M.: CSP2B: a practical approach to combining CSP and B. Formal Aspects Comput. 12, 182\u2013196 (2000)","journal-title":"Formal Aspects Comput."},{"key":"342_CR7","doi-asserted-by":"crossref","unstructured":"Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Proceedings of Formal Methods, pp. 221\u2013236. Springer, Berlin (2005)","DOI":"10.1007\/11526841_16"},{"key":"342_CR8","doi-asserted-by":"crossref","unstructured":"Cai, L., Gajski, D.: Transaction level modeling: an overview. In: First IEEE\/ACM\/IFIP International Conference on Hardware\/Software Codesign and System Synthesis, 2003, pp. 19\u201324 (2003)","DOI":"10.1145\/944645.944651"},{"key":"342_CR9","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, P.D.L., Castro, J.R., Gallardo, M., Merino, P.: Verification support for ARINC-653-based avionics software. Sotw. Test. Verification. Reliab. 21(4): 267\u2013298 (2011). ISSN 1099-1689","DOI":"10.1002\/stvr.422"},{"key":"342_CR10","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201987, pp. 178\u2013188. ACM, New York (1987)","DOI":"10.1145\/41625.41641"},{"key":"342_CR11","unstructured":"Clarke, D., Lee, I., Liang Xie, H.: VERSA: A tool for the specification and analysis of resource-bound real-time systems. J. Comput. Softw. Eng. 3 (1995)"},{"issue":"1","key":"342_CR12","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J Eker","year":"2003","unstructured":"Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Sachs, S., Xiong, Y.: Taming heterogeneity\u2014the ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"key":"342_CR13","unstructured":"Fischer, C., Smith, G.: Combining CSP and object-Z: finite or infinite trace semantics? In: FORTE X\/PSTV XVII \u201997: Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), pp. 503\u2013518. Chapman & Hall, London (1998)"},{"key":"342_CR14","unstructured":"Gamati\u00e9, A., Gautier, T.: Synchronous modeling of modular avionics architectures using the SIGNAL language. Research Report RR-4678, INRIA (2002)"},{"key":"342_CR15","doi-asserted-by":"crossref","unstructured":"Gamati\u00e9, A., Gautier, T.: Synchronous modeling of avionics applications using the SIGNAL language. In: Proceedings of the 9th IEEE Real-Time and Embededd Technology and Applications Sympsium, pp. 144\u2013151 (2003). ISSN 1545-3421","DOI":"10.1109\/RTTAS.2003.1203046"},{"key":"342_CR16","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.entcs.2003.05.002","volume":"88","author":"A Gamati\u00e9","year":"2004","unstructured":"Gamati\u00e9, A., Gautier, T., Besnard, L.: Modeling of avionics applications and performance evaluation techniques using the synchronous language signal. Electron. Notes Theor. Comput. Sci. 88, 87\u2013103 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"342_CR17","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"342_CR18","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"342_CR19","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1006\/inco.1995.1041","volume":"117","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117, 221\u2013239 (1995)","journal-title":"Inf. Comput."},{"key":"342_CR20","doi-asserted-by":"crossref","unstructured":"In der Rieden, T., Knapp, S.: An approach to the pervasive formal specification and verification of an automotive system: status report. In: FMICS \u201905: Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, pp. 115\u2013124. ACM, New York (2005)","DOI":"10.1145\/1081180.1081195"},{"key":"342_CR21","unstructured":"Inc, A.R.: Avionics application software standard interface part 1\u2014required services: ARINC specification 653p1-2. Aeronautical Radio Inc, Tech. rep. (2005)"},{"key":"342_CR22","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch. N., Segal, R., Vaandrager, F.: The Theory of Timed I\/O Automata. Synth. Lec. Comput. Sci. 1(1): 1\u2013114 (2006)","DOI":"10.2200\/S00006ED1V01Y200508CSL001"},{"key":"342_CR23","doi-asserted-by":"crossref","unstructured":"Kim, J., Choi, J.Y., Kang, I., Lee, I.: Generating composite behavior of embedded software components based on uml behavioral model and process algebra. SIGSOFT Softw. Eng. Notes 36, 1\u20139 (2011)","DOI":"10.1145\/1921532.1921562"},{"issue":"17","key":"342_CR24","first-page":"2415","volume":"16","author":"J Kim","year":"2010","unstructured":"Kim, J., Kang, I., Choi, J.Y., Lee, I.: UML behavior models of real-time embedded software for model-driven architecture. J. Univers. Comput. Sci. 16(17), 2415\u20132434 (2010)","journal-title":"J. Univers. Comput. Sci."},{"issue":"4","key":"342_CR25","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1109\/TII.2010.2060206","volume":"6","author":"J Kim","year":"2010","unstructured":"Kim, J., Kang, I., Choi, J.Y., Lee, I.: Timed and resource-oriented statecharts for embedded software. IEEE Trans. Ind. Inform. 6(4), 568\u2013578 (2010)","journal-title":"IEEE Trans. Ind. Inform."},{"key":"342_CR26","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1023\/A:1008293802713","volume":"8","author":"XD Koutsoukos","year":"1998","unstructured":"Koutsoukos, X.D., He, K.X., Lemmon, M.D., Antsaklis, P.J.: Timed petri nets in hybrid systems: stability and supervisorycontrol. Discret. Event Dyn. Syst. 8, 137\u2013173 (1998)","journal-title":"Discret. Event Dyn. Syst."},{"key":"342_CR27","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Finite state machines and modal models in Ptolemy II. Tech. Rep. UCB\/EECS-2009-151, EECS Department, University of California, Berkeley (2009)","DOI":"10.21236\/ADA538760"},{"key":"342_CR28","doi-asserted-by":"crossref","unstructured":"Lee, I., Br\u2019emond-Gr\u2019egoire, P., Gerber, R.: A process algebraic approach to the specification and analysis of resource-bound real-time systems. In: Proceedings of the IEEE Special Issue on, Real-Time Systems, pp. 158\u2013171 (1994)","DOI":"10.1109\/5.259433"},{"key":"342_CR29","doi-asserted-by":"crossref","unstructured":"Lee, I., Philippou, A., Sokolosky, O.: Resources in process algebra. J. Logic Algebraic Program. 72(1), 98\u2013122 (2007). [Algebraic Process Calculi: The First Twenty Five Years and Beyond. II]","DOI":"10.1016\/j.jlap.2007.02.005"},{"key":"342_CR30","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.J.: Pro B: a model checker for B. In: FME, pp. 855\u2013874 (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"342_CR31","unstructured":"Micrium\u2014 $$\\mu $$ C\/OS-II Kernel. http:\/\/www.micrium.com\/"},{"key":"342_CR32","doi-asserted-by":"crossref","unstructured":"Mallet, F., de Simone, R.: MARTE: a profile for rt\/e systems modeling, analysis-and simulation? In: Proceedings of the 1st International Conference on Simulation tools and Techniques for Communications, Networks and Systems & Workshops, Simutools \u201908, pp. 43:1\u201343:8. ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering), ICST, Brussels (2008)","DOI":"10.4108\/ICST.SIMUTOOLS2008.3097"},{"key":"342_CR33","doi-asserted-by":"crossref","unstructured":"Merritt, M., Modugno, F., Tuttle, M.R.: Time-constrained automata (extended abstract). In: Proceedings of the 2nd International Conference on Concurrency Theory, CONCUR \u201991, pp. 408\u2013423. Springer, London (1991)","DOI":"10.1007\/3-540-54430-5_103"},{"key":"342_CR34","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)"},{"key":"342_CR35","unstructured":"OMG: Object Constraint Language, Version 2.2. Object Management Group (OMG), Needham (2010)"},{"key":"342_CR36","unstructured":"Pettersson, P., Seceleanu, C., Vulgarakis, A.: Remes: a resource model for embedded systems. Technical Report ISSN 1404\u20133041 ISRN MDH-MRTC-232\/2008-1-SE, M\u00e5lardalen University (2008)"},{"key":"342_CR37","doi-asserted-by":"crossref","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58, 249\u2013261 (1988)","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"342_CR38","unstructured":"Sagonas, K. F., Armstrong, J. (eds.) Proceedings of the 2005 ACM SIGPLAN Workshop on Erlang, Tallinn, Estonia, September 26\u201328. Erlang workshop ACM, Estonia (2005). ISBN 1-59593-066-3"},{"key":"342_CR39","doi-asserted-by":"crossref","unstructured":"Schneider, S., Treharne, H., Evans, N.: Chunks: component verification in CSP $$||$$ B. In: IFM\u20192005, pp. 89\u2013108 (2005)","DOI":"10.1007\/11589976_7"},{"key":"342_CR40","doi-asserted-by":"crossref","unstructured":"Smith, G., Derrick, J.: Abstract specification in object- Z and CSP. In: Formal Methods and Software Engineering, Lecture Notes in Computer Science, vol. 2495, pp. 108\u2013119. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36103-0_14"},{"key":"342_CR41","unstructured":"The UML Profile for MARTE: Modeling and Analysis of Real-Time and Embedded Systems. http:\/\/www.omgmarte.org\/"},{"key":"342_CR42","unstructured":"Unified Modeling Language. http:\/\/www.omg.org\/spec\/UML\/2.0"},{"issue":"1","key":"342_CR43","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanz\u00e1lek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0342-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0342-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0342-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:03:17Z","timestamp":1746000197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0342-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,3]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["342"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0342-8","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2013,5,3]]}}}