{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T23:03:32Z","timestamp":1774479812557,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,1,28]],"date-time":"2013-01-28T00:00:00Z","timestamp":1359331200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s11704-013-2008-1","type":"journal-article","created":{"date-parts":[[2013,1,28]],"date-time":"2013-01-28T03:14:49Z","timestamp":1359342889000},"page":"214-235","source":"Crossref","is-referenced-by-count":5,"title":["A novel requirement analysis approach for periodic control systems"],"prefix":"10.1007","volume":"7","author":[{"given":"Zheng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiangwen","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxiang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingsong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bin","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,1,28]]},"reference":[{"key":"2008_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126: 183\u2013235","journal-title":"Theoretical Computer Science"},{"key":"2008_CR2","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/j.entcs.2005.12.093","volume":"162","author":"J Ouaknine","year":"2006","unstructured":"Ouaknine J, Schneider S. Timed csp: a retrospective. Electronics Notes in Theoretical Computer Science, 2006, 162: 273\u2013276","journal-title":"Electronics Notes in Theoretical Computer Science"},{"issue":"1","key":"2008_CR3","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2005.12.014","volume":"148","author":"L Baresi","year":"2006","unstructured":"Baresi L, Pezz\u00e8 M. An introduction to software testing. Electronics Notes in Theoretical Computer Science, 2006, 148(1): 89\u2013111","journal-title":"Electronics Notes in Theoretical Computer Science"},{"key":"2008_CR4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1109\/APAQ.2000.883800","volume-title":"Proceedings of Asia-Pacific Conference on Quality Software (APAQS)","author":"J Zhang","year":"2000","unstructured":"Zhang J. Specification analysis and test data generation by solving Boolean combinations of numeric constraints. In: Proceedings of Asia-Pacific Conference on Quality Software (APAQS). 2000, 267\u2013274"},{"key":"2008_CR5","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/1985793.1985847","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE)","author":"M Staats","year":"2011","unstructured":"Staats M, Whalen M W, Heimdahl M P. Programs, tests, and oracles: the foundations of testing revisited. In: Proceedings of the International Conference on Software Engineering (ICSE). 2011, 391\u2013400"},{"key":"2008_CR6","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s10617-010-9052-4","volume":"14","author":"M Chen","year":"2010","unstructured":"Chen M, Mishra P, Kalita D. Efficient test case generation for validation of UML activity diagrams. Design Automation for Embedded Systems, 2010, 14: 105\u2013130","journal-title":"Design Automation for Embedded Systems"},{"issue":"6","key":"2008_CR7","doi-asserted-by":"crossref","first-page":"852","DOI":"10.1109\/TC.2011.49","volume":"60","author":"M Chen","year":"2011","unstructured":"Chen M, Mishra P. Property learning techniques for efficient generation of directed tests. IEEE Trans. Computers, 2011, 60(6): 852\u2013864","journal-title":"IEEE Trans. Computers"},{"key":"2008_CR8","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1109\/TASE.2009.10","volume-title":"Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"Z Wang","year":"2009","unstructured":"Wang Z, Yu X, Sun T, Pu G, Ding Z, Hu J. Test data generation for derived types in c program. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 155\u2013162"},{"key":"2008_CR9","first-page":"17","volume":"60\u201361","author":"G D Plotkin","year":"2004","unstructured":"Plotkin G D. A structural approach to operational semantics. Journal of Logic and Algebra Programming, 2004, 60\u201361: 17\u2013139","journal-title":"Journal of Logic and Algebra Programming"},{"key":"2008_CR10","first-page":"594","volume-title":"Proceedings of International Symposium on Leveraging Applications (ISoLA)","author":"Z Wang","year":"2010","unstructured":"Wang Z, Li J, Zhao Y, Qi Y, Pu G, He J, Gu B. SPARDL: a requirement modeling language for periodic control system. In: Proceedings of International Symposium on Leveraging Applications (ISoLA). 2010, 594\u2013608"},{"key":"2008_CR11","first-page":"41","volume-title":"Proceedings of the 13th International Symposium on High-Assurance System Engineering","author":"J Li","year":"2011","unstructured":"Li J, Wang Z, Zhao Y, Pu G, Qi Y, Gu B. An event-b interpretation for spardl model. In: Proceedings of the 13th International Symposium on High-Assurance System Engineering. 2011, 41\u201348"},{"key":"2008_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of program analysis","author":"F Nielson","year":"1999","unstructured":"Nielson F, Nielson H R, Hankin C. Principles of program analysis. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999"},{"key":"2008_CR13","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-540-39815-8_3","volume-title":"Proceedings of Conference on Generative Programming and Component Engineering (GPCE)","author":"K Hammond","year":"2003","unstructured":"Hammond K, Michaelson G. Hume: a domain-specific language for real-time embedded systems. In: Proceedings of Conference on Generative Programming and Component Engineering (GPCE). 2003, 37\u201356"},{"key":"2008_CR14","first-page":"12","volume-title":"Proceedings of the IEEE Workshop on Industrial Strength Formal Specification Techniques (WIFT)","author":"C Heitmeyer","year":"1998","unstructured":"Heitmeyer C. Using the scr toolset to specify software requirements. In: Proceedings of the IEEE Workshop on Industrial Strength Formal Specification Techniques (WIFT). 1998, 12\u201313"},{"key":"2008_CR15","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/IWSSD.1996.501143","volume-title":"Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD)","author":"P C Clements","year":"1996","unstructured":"Clements P C. A survey of architecture description languages. In: Proceedings of the 8th International Workshop on Software Specification and Design (IWSSD). 1996, 16\u201325"},{"key":"2008_CR16","doi-asserted-by":"crossref","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 realtime systems. IEEE Transactions on Software Engineering, 1994, 20: 933\u2013947","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2008_CR17","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/774789.774817","volume-title":"Proceedings of the International Symposium on Hardware\/Software Codesign (CODES)","author":"H Oh","year":"2002","unstructured":"Oh H, Ha S. Hardware-software cosynthesis of multi-mode multi-task embedded systems with real-time constraints. In: Proceedings of the International Symposium on Hardware\/Software Codesign (CODES). 2002, 133\u2013138"},{"issue":"2","key":"2008_CR18","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1109\/TCAD.2004.837729","volume":"24","author":"M T Schmitz","year":"2005","unstructured":"Schmitz M T, Al-Hashimi B M, Eles P. Cosynthesis of energy-efficient multimode embedded systems with consideration of mode-execution probabilities. IEEE Transactions on CAD of Integrated Circuits and Systems, 2005, 24(2): 153\u2013169","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"issue":"3","key":"2008_CR19","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. Science of Computer Programming, 1987, 8(3): 231\u2013274","journal-title":"Science of Computer Programming"},{"key":"2008_CR20","unstructured":"Architecture analysis & design language (AADL). http:\/\/http:\/\/www.aadl.info\/"},{"key":"2008_CR21","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/1101908.1101960","volume-title":"Proceedings of the IEEE\/ACM international Conference on Automated Software Engineering (ASE)","author":"N Liu","year":"2005","unstructured":"Liu N, Grundy J, Hosking J. A visual language and environment for composing web services. In: Proceedings of the IEEE\/ACM international Conference on Automated Software Engineering (ASE). 2005, 321\u2013324"},{"issue":"4","key":"2008_CR22","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s00766-011-0124-1","volume":"16","author":"E R Luna","year":"2011","unstructured":"Luna E R, Rossi G, Garrig\u00f3s I. Webspec: a visual language for specifying interaction and navigation requirements in web applications. Requirements Engineering, 2011, 16(4): 297\u2013321","journal-title":"Requirements Engineering"},{"key":"2008_CR23","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1109\/TSE.2010.47","volume":"37","author":"B Cornelissen","year":"2011","unstructured":"Cornelissen B, Zaidman A, Deursen V A. A controlled experiment for program comprehension through trace visualization. IEEE Transactions on Software Engineering, 2011, 37: 341\u2013355","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2008_CR24","volume-title":"System-level validation: high-level modeling and directed test generation techniques","author":"M Chen","year":"2012","unstructured":"Chen M, Qin X, Koo H M, Mishra P. System-level validation: high-level modeling and directed test generation techniques. Springer, 2012"},{"key":"2008_CR25","first-page":"183","volume-title":"Proceedings of the International Requirements Engineering Conference (RE)","author":"M Smith","year":"2008","unstructured":"Smith M, Havelund K. Requirements capture with rcat. In: Proceedings of the International Requirements Engineering Conference (RE). 2008, 183\u2013192"},{"key":"2008_CR26","unstructured":"Spin model checker. http:\/\/spinroot.com\/"},{"issue":"7","key":"2008_CR27","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/780731.780756","volume":"38","author":"R Alur","year":"2003","unstructured":"Alur R, Ivancic F, Kim J, Lee I, Sokolsky O. Generating embedded software from hierarchical hybrid models. ACM SIGPLAN Notice, 2003, 38(7): 171\u2013182","journal-title":"ACM SIGPLAN Notice"},{"key":"2008_CR28","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/978-3-540-68524-1_3","volume-title":"Proceedings of the International conference on Testing of Software and Communicating Systems (TestCom)","author":"K Havelund","year":"2008","unstructured":"Havelund K. Runtime verification of c programs. In: Proceedings of the International conference on Testing of Software and Communicating Systems (TestCom). 2008, 7\u201322"},{"key":"2008_CR29","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.entcs.2006.02.007","volume":"144","author":"V Stolz","year":"2006","unstructured":"Stolz V, Bodden E. Temporal assertions using aspectj. Electronics Notes on Theoretical Computer Science, 2006, 144: 109\u2013124","journal-title":"Electronics Notes on Theoretical Computer Science"},{"key":"2008_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45449-7_12","volume-title":"Giotto: a time-triggered language for embedded programming","author":"T A Henzinger","year":"2001","unstructured":"Henzinger T A, Horowitz B, Kirsch C M. Giotto: a time-triggered language for embedded programming. Technical Report, Department of Electronic Engineering and Computer Science, University of California, Berkeley, 2001"},{"key":"2008_CR31","first-page":"50","volume-title":"Proceedings of the IEEE Symposia on Human Centric Computing Languages and Environments (HCC)","author":"X Liu","year":"2001","unstructured":"Liu X, Xiong Y, Lee E A. The ptolemy ii framework for visual languages. In: Proceedings of the IEEE Symposia on Human Centric Computing Languages and Environments (HCC). 2001, 50\u201351"},{"key":"2008_CR32","unstructured":"The mathworks: stateflow and stateflow coder, user\u2019s guide. www.mathworks.com\/help\/releases\/R13sp2\/pdf_doc\/stateflow\/sf_ug.pdf"},{"key":"2008_CR33","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. An operational semantics for stateflow. International Journal on Software Tools for Technology Transfer, 2007, 9: 447\u2013456","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2008_CR34","first-page":"49","volume-title":"Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL)","author":"T Reps","year":"1995","unstructured":"Reps T, Horwitz S, Sagiv M. Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL). 1995, 49\u201361"},{"issue":"1\u20132","key":"2008_CR35","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"M Sagiv","year":"1996","unstructured":"Sagiv M, Reps T, Horwitz S. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 1996, 167(1\u20132): 131\u2013170","journal-title":"Theoretical Computer Science"},{"key":"2008_CR36","first-page":"122","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"D W Goodwin","year":"1997","unstructured":"Goodwin D W. Interprocedural dataflow analysis in an executable optimizer. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 1997, 122\u2013133"},{"key":"2008_CR37","first-page":"97","volume-title":"Proceedings of ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE)","author":"T Ball","year":"2001","unstructured":"Ball T, Rajamani S K. Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE). 2001, 97\u2013103"},{"issue":"7","key":"2008_CR38","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball T, Levin V, Rajamani S K. A decade of software model checking with slam. Communications of ACM, 2011, 54(7): 68\u201376","journal-title":"Communications of ACM"},{"key":"2008_CR39","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/1190216.1190226","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"P Godefroid","year":"2007","unstructured":"Godefroid P. Compositional dynamic test generation. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 2007, 47\u201354"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-2008-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-013-2008-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-2008-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,6]],"date-time":"2022-02-06T21:33:58Z","timestamp":1644183238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-013-2008-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,28]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["2008"],"URL":"https:\/\/doi.org\/10.1007\/s11704-013-2008-1","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1,28]]}}}