{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:46:45Z","timestamp":1760586405890,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540708889"},{"type":"electronic","value":"9783540708896"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70889-6_8","type":"book-chapter","created":{"date-parts":[[2007,5,10]],"date-time":"2007-05-10T10:04:16Z","timestamp":1178791456000},"page":"109-121","source":"Crossref","is-referenced-by-count":3,"title":["Detecting Design Flaws in UML State Charts for Embedded Software"],"prefix":"10.1007","author":[{"given":"Janees","family":"Elamkulam","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziv","family":"Glazberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ishai","family":"Rabinovitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gururaja","family":"Kowlali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Satish Chandra","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandeep","family":"Kohli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sai","family":"Dattathrani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio Paniagua","family":"Macia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R. Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Transactions on Programming Languages and Systems\u00a023(3), 273\u2013303 (2001), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/503502.503503","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/11513988_16","volume-title":"Computer Aided Verification","author":"S. Barner","year":"2005","unstructured":"Barner, S., Glazberg, Z., Rabinovitz, I.: Wolf - bug hunter for concurrent software using formal methods. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 153\u2013157. Springer, Heidelberg (2005)"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.10.024","volume":"127","author":"M.E. Beato","year":"2005","unstructured":"Beato, M.E., et al.: UML automatic verification tool with formal methods. Electronic Notes in Theoretical Computer Science\u00a0127(4), 3\u201316 (2005), \n                    \n                      http:\/\/dx.doi.org\/10.1016\/j.entcs.2004.10.024","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"8_CR4","unstructured":"Beer, I., et al.: RuleBase: an industry-oriented formal verification tool. In: Proc. of the 33rd Design Automation Conference, pp. 655\u2013660 (1996), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/240518.240642"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/349194.349197","volume":"32","author":"P. Bellini","year":"2000","unstructured":"Bellini, P., Mattonlini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Computing Surveys\u00a032(1), 12\u201342 (2000), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/349194.349197","journal-title":"ACM Computing Surveys"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1109\/WPC.2004.1311069","volume-title":"Proc. of 12th International Workshop on Program Comprehension (IWPC2004)","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., et al.: An Eclipse plug-in for model checking. In: Proc. of 12th International Workshop on Program Comprehension (IWPC2004), pp. 251\u2013255. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/10722167_45","volume-title":"Computer Aided Verification","author":"T. Bienm\u00fcller","year":"2000","unstructured":"Bienm\u00fcller, T., Damm, W., Wittke, H.: The STATEMATE verification environment \u2013 making it real. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 561\u2013567. Springer, Heidelberg (2000)"},{"key":"8_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46852-8_1","volume-title":"Unified Modeling Language User Guide","author":"G. Booch","year":"1999","unstructured":"Booch, G., Rumbaugh, J.E., Jacobson, I.: Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)"},{"issue":"2","key":"8_CR9","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the Association for Computing Machinery\u00a030(2), 323\u2013342 (1983), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/322374.322380","journal-title":"Journal of the Association for Computing Machinery"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., et al.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"issue":"7","key":"8_CR11","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., et al.: Model checking large software specifications. IEEE Transactions on Software Engineering\u00a024(7), 498\u2013520 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/5397.5399","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"5","key":"8_CR13","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/186025.186051","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"8_CR14","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"8_CR15","first-page":"70","volume-title":"Proc. of 5th IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop","author":"A. Darvas","year":"2002","unstructured":"Darvas, A., Majzik, I., Benyo, B.: Verification of UML statechart models of embedded systems. In: Proc. of 5th IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop, pp. 70\u201377. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-45800-X_16","volume-title":"\u00abUML\u00bb 2002 - The Unified Modeling Language. Model Engineering, Concepts, and Tools","author":"S. Flake","year":"2002","unstructured":"Flake, S., M\u00fcller, W.: A UML profile for real-time constraints with the OCL. In: J\u00e9z\u00e9quel, J.-M., Hussmann, H., Cook, S. (eds.) \u00abUML\u00bb 2002 - The Unified Modeling Language. Model Engineering, Concepts, and Tools. LNCS, vol.\u00a02460, pp. 179\u2013195. Springer, Heidelberg (2002)"},{"issue":"3","key":"8_CR17","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10270-003-0026-x","volume":"2","author":"S. Flake","year":"2003","unstructured":"Flake, S., M\u00fcller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Software and System Modeling\u00a02(3), 164\u2013186 (2003)","journal-title":"Software and System Modeling"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/HASE.1999.809474","volume-title":"Proc. of 4th IEEE International Symposium on High-Assurance Systems Engineering","author":"S. Gnesi","year":"1999","unstructured":"Gnesi, S., Latella, D., Massink, M.: Model checking UML statechart diagrams using JACK. In: Proc. of 4th IEEE International Symposium on High-Assurance Systems Engineering, pp. 46\u201355. IEEE Computer Society Press, Los Alamitos (1999)"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","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. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","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 Transactions on Software Engineering and Methodology\u00a05(4), 293\u2013333 (1996), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/235321.235322","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"8_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"key":"8_CR22","first-page":"122","volume-title":"Proc. of the 10th IEEE workshop on Real-time operating systems and software","author":"C.L. Heitmeyer","year":"1993","unstructured":"Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: A benchmark for comparing different approaches for specifying and verifying real-time systems. In: Proc. of the 10th IEEE workshop on Real-time operating systems and software, pp. 122\u2013129. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., et al.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"8_CR24","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"8_CR25","unstructured":"IBM: Rational Rose RealTime. \n                    \n                      http:\/\/www.ibm.com\/software\/awdtools\/developer\/technical"},{"key":"8_CR26","unstructured":"IEEE: PSL \u2013 IEEE Standard for Property Specification Language. IEEE P1850, \n                    \n                      http:\/\/www.eda.org\/ieee-1850\/"},{"issue":"12","key":"8_CR27","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1109\/32.368134","volume":"20","author":"F. Jahanian","year":"1994","unstructured":"Jahanian, F., Mok, A.K.: Modechart: A specification language for real-time systems. IEEE Transactions on Software Engineering\u00a020(12), 933\u2013947 (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/263698.263756","volume-title":"Proc. of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA97)","author":"S. Kent","year":"1997","unstructured":"Kent, S.: Constraint diagrams: visualizing invariants in object-oriented models. In: Proc. of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA97), pp. 327\u2013341. ACM Press, New York (1997), doi:10.1145\/263698.263756"},{"key":"8_CR29","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 \u2013 timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013416. Springer, Heidelberg (2002)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1007\/3-540-40011-7_39","volume-title":"UML 2000 - The Unified Modeling Language. Advancing the Standard","author":"G. Kwon","year":"2000","unstructured":"Kwon, G.: Rewrite rules and operational semantics for model checking UML statecharts. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol.\u00a01939, pp. 528\u2013540. Springer, Heidelberg (2000)"},{"issue":"1-2","key":"8_CR31","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"8_CR32","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computer Science\u00a011(6), 637\u2013664 (1999)","journal-title":"Formal Aspects of Computer Science"},{"key":"8_CR33","volume-title":"Proc. of 2rd International Conference on Formal Methods for Open Object-Based Distributed Systems, vol. 139","author":"D. Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Towards a formal operational semantics of UML statechart diagrams. In: Proc. of 2rd International Conference on Formal Methods for Open Object-Based Distributed Systems, vol. 139, Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1109\/ASE.1999.802301","volume-title":"Proc. of 14th IEEE International Conference on Automated Software Engineering","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.: vUML: a tool for verifying UML models. In: Proc. of 14th IEEE International Conference on Automated Software Engineering, pp. 255\u2013258. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"8_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"8_CR36","first-page":"90","volume-title":"Proc. of 2nd Workshop on Industrial-Strength Formal Specification Techniques","author":"E. Mikk","year":"1998","unstructured":"Mikk, E., et al.: Implementing statecharts in PROMELA\/SPIN. In: Proc. of 2nd Workshop on Industrial-Strength Formal Specification Techniques, pp. 90\u2013101. IEEE Computer Society Press, Los Alamitos (1998)"},{"issue":"1","key":"8_CR37","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/237432.237438","volume":"6","author":"L.E. Moser","year":"1997","unstructured":"Moser, L.E., et al.: A graphical environment for the design of concurrent real-time systems. ACM Transactions on Software Engineering and Methodology\u00a06(1), 31\u201379 (1997), doi:10.1145\/237432.237438","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"8_CR38","unstructured":"Object Management Group: UML 2.0 OCL Final Adopted Specification. OMG Document ptc\/03-10-14 (2003), \n                    \n                      ftp:\/\/ftp.omg.org\/pub\/docs\/ptc\/03-10-14.pdf"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","first-page":"430","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"I. Paltor","year":"1999","unstructured":"Paltor, I., Lilius, J.: Formalising UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) \u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard. LNCS, vol.\u00a01723, pp. 430\u2013445. Springer, Heidelberg (1999)"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"983","DOI":"10.1007\/3-540-48118-4_3","volume-title":"FM\u201999 - Formal Methods","author":"S.A. Seshia","year":"1999","unstructured":"Seshia, S.A., et al.: A translation of statecharts to Esterel. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 983\u20131007. Springer, Heidelberg (1999)"},{"key":"8_CR41","first-page":"315","volume-title":"Proc. of 16th IEEE International Conference on Automated Software Engineering","author":"W. Shen","year":"2001","unstructured":"Shen, W., Compton, K.J., Huggins, J.: A toolset for supporting UML static and dynamic model checking. In: Proc. of 16th IEEE International Conference on Automated Software Engineering, pp. 315\u2013318. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/997163.997200","volume-title":"Proc. of the 2004 ACM SIGPLAN\/SIGBED conference on Languages, compilers, and tools for embedded systems","author":"A. Wasowski","year":"2004","unstructured":"Wasowski, A.: Flattening statecharts without explosions. In: Proc. of the 2004 ACM SIGPLAN\/SIGBED conference on Languages, compilers, and tools for embedded systems, pp. 257\u2013266. ACM Press, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software, Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70889-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:11:18Z","timestamp":1558257078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70889-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540708889","9783540708896"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70889-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}