{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:55:53Z","timestamp":1747810553509,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237242"},{"type":"electronic","value":"9783540304777"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30477-7_26","type":"book-chapter","created":{"date-parts":[[2010,2,28]],"date-time":"2010-02-28T23:53:29Z","timestamp":1267401209000},"page":"382-397","source":"Crossref","is-referenced-by-count":1,"title":["Formal Design and Verification of Real-Time Embedded Software"],"prefix":"10.1007","author":[{"given":"Pao-Ann","family":"Hsiung","sequence":"first","affiliation":[]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"26_CR1","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.: Automata for modeling real-time systems. Theoretical Computer Science\u00a0126(2), 183\u2013236 (1994)","journal-title":"Theoretical Computer Science"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Petterson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems, FORMATS, Marseille, France (September 2003)","DOI":"10.1007\/978-3-540-40903-8_6"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"26_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"26_CR5","volume-title":"Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns","author":"B.P. Douglass","year":"1999","unstructured":"Douglass, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison Wesley Longman, Inc., Reading (1999)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Fayad, M., Schmidt, D.: Object-oriented application frameworks. Communications of the ACM, Special Issue on Object-Oriented Application Frameworks\u00a040 (October 1997)","DOI":"10.1145\/262793.262798"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00337680","volume":"11","author":"H.A. Hansson","year":"1996","unstructured":"Hansson, H.A., Lawson, H.W., Stromberg, M., Larsson, S.: BASEMENT: A distributed real-time architecture for vehicle applications. Real-Time Systems\u00a011(3), 223\u2013244 (1996)","journal-title":"Real-Time Systems"},{"key":"26_CR8","first-page":"138","volume-title":"Proceedings of the 27th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS 1998)","author":"P.-A. Hsiung","year":"1998","unstructured":"Hsiung, P.-A.: RTFrame: An object-oriented application framework for real-time applications. In: Proceedings of the 27th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS 1998), pp. 138\u2013147. IEEE Computer Society Press, Los Alamitos (1998)"},{"issue":"15","key":"26_CR9","doi-asserted-by":"publisher","first-page":"1435","DOI":"10.1016\/S1383-7621(00)00034-5","volume":"46","author":"P.-A. Hsiung","year":"2000","unstructured":"Hsiung, P.-A.: Embedded software verification in hardware-software codesign. Journal of Systems Architecture - the Euromicro Journal\u00a046(15), 1435\u20131450 (2000)","journal-title":"Journal of Systems Architecture - the Euromicro Journal"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1109\/ICVD.2003.1183145","volume-title":"Proceedings of the 16th International Conference on VLSI Design (VLSI 2003)","author":"P.-A. Hsiung","year":"2003","unstructured":"Hsiung, P.-A., Cheng, S.-Y.: Automating formal modular verification of asynchronous real-time embedded systems. In: Proceedings of the 16th International Conference on VLSI Design (VLSI 2003), New Delhi, India, pp. 249\u2013254. IEEE CS Press, Los Alamitos (2003)"},{"key":"26_CR11","first-page":"114","volume-title":"Proceedings of the 1st ACM\/IEEE\/IFIP International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS 2003)","author":"P.-A. Hsiung","year":"2003","unstructured":"Hsiung, P.-A., Lin, C.-Y.: Synthesis of real-time embedded software with local and global deadlines. In: Proceedings of the 1st ACM\/IEEE\/IFIP International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS 2003), Newport Beach, CA, USA, pp. 114\u2013119. ACM Press, New York (2003)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-24686-2_14","volume-title":"Real-Time and Embedded Computing Systems and Applications","author":"P.-A. Hsiung","year":"2004","unstructured":"Hsiung, P.-A., Lin, C.-Y., Lee, T.-Y.: Quasi-dynamic scheduling for the synthesis of real-time embedded software with local and global deadlines. In: Chen, J., Hong, S. (eds.) RTCSA 2003. LNCS, vol.\u00a02968, pp. 229\u2013243. Springer, Heidelberg (2004)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaboration. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013414. Springer, Heidelberg (2002)"},{"key":"26_CR14","unstructured":"Kuan, T., See, W.-B., Chen, S.-J.: An object-oriented real-time framework and development environment. In: Proceedings OOPSLA 1995 Workshop, vol. 18 (1995)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Kodase, S., Wang, S., Shin, K.G.: Transforming structural model to runtime model of embedded software with real-time constraints. In: Proceedings of Design, Automation and Test in Europe Conference, Munich, Germany, March 2003, pp. 170\u2013175 (2003)","DOI":"10.1109\/DATE.2003.1253824"},{"key":"26_CR16","unstructured":"Lavazza, L.: A methodology for formalizing concepts underlying the DESS notation, Software Development Process for Real-Time Embedded Software Systems, EUREKA-ITEA project, D 1.7.4 (December 2001), http:\/\/www.dess-itea.org"},{"key":"26_CR17","volume-title":"Proceedings of the 16th IEEE International SoC Conference","author":"W.-S. Liao","year":"2003","unstructured":"Liao, W.-S., Hsiung, P.-A.: FVP: A formal verification platform for SoC. In: Proceedings of the 16th IEEE International SoC Conference, Portland, Oregon, USA. IEEE CS Press, Portland (2003)"},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"C. Liu","year":"1973","unstructured":"Liu, C., Layland, J.: Scheduling algorithms for multiprogramming in a hard-real time environment. Journal of the Association for Computing Machinery\u00a020, 46\u201361 (1973)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"de Niz, D., Rajkumar, R.: Time Weaver: A software-through-models framework for embedded real-time systems. In: Proceedings of the International Workshop on Languages, Compilers, and Tools for Embedded Systems, San-Diego, California, USA, June 2003, pp. 133\u2013143 (2003)","DOI":"10.1145\/780732.780751"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"26_CR21","volume-title":"The UML Reference Guide","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Booch, G., Jacobson, I.: The UML Reference Guide. Addison Wesley Longman, Redwood City (1999)"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Samek, M.: Practical Statecharts in C\/C++ Quantum Programming for Embedded Systems, CMP Books (2002)","DOI":"10.1201\/9781482280807"},{"key":"26_CR23","unstructured":"Schmidt, D.: Applying design patterns and frameworks to develop object-oriented communication software. In: Handbook of Programming Languages, vol. I (1997)"},{"key":"26_CR24","first-page":"327","volume-title":"Domain-Specific Application Frameworks (M","author":"W.-B. See","year":"2000","unstructured":"See, W.-B., Chen, S.-J.: Object-oriented real-time system framework. In: Fayad, M.E., Johnson, R.E. (eds.) Domain-Specific Application Frameworks, ch.\u00a016, pp. 327\u2013338. John Wiley, Chichester (2000)"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Selic, B.: Modeling real-time distributed software systems. In: Proceedings of the 4th International Workshop on Parallel and Distributed Real-Time Systems, pp. 11\u201318 (1996)","DOI":"10.1109\/WPDRTS.1996.557427"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Selic, B.: An efficient object-oriented variation of the statecharts formalism for distributed real-time systems. In: Proceedings of the IFIP Conference on Hardware Description Languages and Their Applications (1993)","DOI":"10.1016\/B978-0-444-81641-2.50030-7"},{"key":"26_CR27","volume-title":"Real-time Object Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"Selic, B., Gullekan, G., Ward, P.T.: Real-time Object Oriented Modeling. John Wiley and Sons, Inc., Chichester (1994)"},{"key":"26_CR28","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/774789.774832","volume-title":"Proceedings of the 10th IEEE\/ACM International Symposium on Hardware\/Software Codesign (CODES 2002)","author":"F.-S. Su","year":"2002","unstructured":"Su, F.-S., Hsiung, P.-A.: Extended quasi-static scheduling for formal synthesis and code generation of embedded software. In: Proceedings of the 10th IEEE\/ACM International Symposium on Hardware\/Software Codesign (CODES 2002), Colorado, USA, pp. 211\u2013216. ACM Press, New York (2002)"},{"issue":"1","key":"26_CR29","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/12.980017","volume":"51","author":"F. Wang","year":"2002","unstructured":"Wang, F., Hsiung, P.-A.: Efficient and user-friendly verification. IEEE Transactions on Computers\u00a051(1), 61\u201383 (2002)","journal-title":"IEEE Transactions on Computers"},{"key":"26_CR30","unstructured":"Wang, S., Kodase, S., Shin, K.G.: Automating embedded software construction and analysis with design models. In: Proceedings of International Conference of Euro-uRapid, Frankfurt, Germany (December 2002)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30477-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T22:24:57Z","timestamp":1739917497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30477-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237242","9783540304777"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30477-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}