{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:37:09Z","timestamp":1761323829987,"version":"3.40.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2012,6,6]],"date-time":"2012-06-06T00:00:00Z","timestamp":1338940800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1007\/s10009-012-0235-0","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:33:25Z","timestamp":1341797605000},"page":"653-671","source":"Crossref","is-referenced-by-count":15,"title":["Formal modeling and validation of Stateflow diagrams"],"prefix":"10.1007","volume":"14","author":[{"given":"Chunqing","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manchun","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,6]]},"reference":[{"key":"235_CR1","doi-asserted-by":"crossref","unstructured":"Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, N.: A story about formal methods adoption by a railway signaling manufacturer. In: FM\u201906: Proceedings of the 14th International Symposium on Formal Methods, pp. 179\u2013189. Springer, Berlin (2006)","DOI":"10.1007\/11813040_13"},{"key":"235_CR2","doi-asserted-by":"crossref","unstructured":"Banphawatthanarak, C., Krogh, B.H., Butts, K.: Symbolic verification of executable control specifications. In: CACSD\u201999: Proceedings of the 10th International Symposium on Computer Aided Control System Design, pp. 581\u2013586. IEEE (1999)","DOI":"10.1109\/CACSD.1999.808712"},{"key":"235_CR3","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.entcs.2009.05.043","volume":"240","author":"A. Cavalcanti","year":"2009","unstructured":"Cavalcanti A.: Stateflow diagrams in circus. Electron. Notes Theor. Comput. Sci. 240, 23\u201341 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"235_CR4","doi-asserted-by":"crossref","unstructured":"Chen, C.: Formal analysis for stateflow diagrams. In: SSIRI-C\u201910: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement Companion, pp. 102\u2013109. IEEE Computer Society (2010)","DOI":"10.1109\/SSIRI-C.2010.29"},{"key":"235_CR5","volume-title":"Model Checking","author":"J. Edmund","year":"1999","unstructured":"Edmund J., Clarke M., Grumberg O., Peled D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"235_CR6","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Fantechi, A., Bacherini, S., Zingoni, N.: Formal development for railway signaling using commercial tools. In: FMICS\u201909: Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems, pp. 197\u2013198. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_15"},{"key":"235_CR7","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for Stateflow. In: EMSOFT\u201905: Proceedings of the 5th ACM International Conference on Embedded Software, pp. 164\u2013172. ACM, New York (2005)","DOI":"10.1145\/1086228.1086260"},{"issue":"5\u20136","key":"235_CR8","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-007-0049-7","volume":"9","author":"G. Hamon","year":"2007","unstructured":"Hamon G., Rushby J.M.: An operational semantics for Stateflow. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 447\u2013456 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"3","key":"235_CR9","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":"235_CR10","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel D., Lachover H., Naamad A., Pnueli A., Politi M., Sherman R., Shtull-Trauring A., Trakhtenbrot M.B.: STATEMATE: a working environment for the development of complex reactive systems. IEEE Trans. Softw. Eng. 16(4), 403\u2013414 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"9","key":"235_CR11","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/1378727.1378742","volume":"51","author":"M. Hinchey","year":"2008","unstructured":"Hinchey M., Jackson M., Cousot P., Cook B., Bowen J.P., Margaria T.: Software engineering and formal methods. Commun. ACM 51(9), 54\u201359 (2008)","journal-title":"Commun. ACM"},{"key":"235_CR12","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"issue":"6","key":"235_CR13","doi-asserted-by":"crossref","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. Form. Asp. Comput. 11(6), 637\u2013664 (1999)","journal-title":"Form. Asp. Comput."},{"key":"235_CR14","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Analyzing hierarchical complex real-time systems. In: FSE\u201910: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 365\u2013366. ACM, New York (2010)","DOI":"10.1145\/1882291.1882350"},{"key":"235_CR15","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: ISSRE\u201911: Proceedings of the 22nd Annual International Symposium on Software Reliability Engineering, pp. 190\u2013199. IEEE (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"key":"235_CR16","unstructured":"The MathWorks. Simulink\u00ae Design Verifier TM 1\u2014User\u2019s Guide. September 2009"},{"key":"235_CR17","unstructured":"The MathWorks. Stateflow\u00ae and Stateflow\u00ae coder TM 7\u2014User\u2019s Guide. March 2009"},{"key":"235_CR18","doi-asserted-by":"crossref","unstructured":"Ng, L., Hubbard, P., O\u2019Young, S.: Simulation of fully autonomous control of unmanned air vehicles for maritime surveillance. In: Proceedings of the 2010 Spring Simulation Multiconference, SpringSim\u201910, pp. 40:1\u201340:9. ACM, New York (2010)","DOI":"10.1145\/1878537.1878579"},{"issue":"1-2","key":"235_CR19","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M. Oliveira","year":"2009","unstructured":"Oliveira M., Cavalcanti A., Woodcock J.: A utp semantics for circus. Form. Asp. Comput. 21(1-2), 3\u201332 (2009)","journal-title":"Form. Asp. Comput."},{"key":"235_CR20","doi-asserted-by":"crossref","unstructured":"Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a \u201csafe\u201d subset of Simulink\/Stateflow into Lustre. In: EMSOFT\u201904: Proceedings of the 4th International Conference on Embedded Software, pp. 259\u2013268. ACM, New York (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"235_CR21","doi-asserted-by":"crossref","unstructured":"Sims, S., Cleaveland, R., Butts, K., Ranville, S.: Automated validation of software models. In: ASE\u201901: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp. 91\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/ASE.2001.989794"},{"key":"235_CR22","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: TASE\u201909: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 127\u2013135. IEEE Computer Society (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"235_CR23","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: CAV\u201909: Proceedings of the 21th International Conference on Computer Aided Verification, pp. 709\u2013714. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"235_CR24","unstructured":"Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International (2002). http:\/\/www.csl.sri.com\/~tiwari\/~stateflow.html"},{"key":"235_CR25","doi-asserted-by":"crossref","unstructured":"Toyn, I., Galloway, A.: Proving properties of stateflow models using ISO standard Z and CADiZ. In: ZB\u201905: Proceedings of the 4th International Conference of B and Z Users, pp. 104\u2013123. Springer, Berlin (2005)","DOI":"10.1007\/11415787_7"},{"key":"235_CR26","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surveys 41(4), 1\u201336 (2009)","DOI":"10.1145\/1592434.1592436"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0235-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0235-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0235-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:19:44Z","timestamp":1743697184000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0235-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,6]]},"references-count":26,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11]]}},"alternative-id":["235"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0235-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,6,6]]}}}