{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:22:03Z","timestamp":1750306923911,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:p>Motivated by the need for validation methodologies for embedded systems we propose a method for embedded software testing that can be integrated with existing hardware methods. Existing coverage-directed validation methods guarantee the execution of a certain percentage of the program code under test. Yet they do not generally verify whether the statements executed have any influence on the program's output. In the proposed method, a program statement is considered covered not simply for belonging to the executed path, but only if its execution has influence in some observable output. The paths are generated by searching the longest path in terms of the number of statements in the path. Given that not all paths are valid, we check their feasibility using a method based on Mixed Integer Linear Programming (MILP). Variable aliasing is accounted for by representing variables by their memory addresses when building this MILP problem. In this manner, for feasible paths, we obtain immediately the input values that allow the execution of the path. Using these inputs, we determine the statements actually observed. We repeat this process until a user-specified level of coverage has been achieved. In the generation of each new path, the statement coverage obtained so far and the feasibility of previous paths is taken into account. We present results that demonstrate the effectiveness of this methodology.<\/jats:p>","DOI":"10.1145\/2442087.2442090","type":"journal-article","created":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T12:17:58Z","timestamp":1365509878000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Coverage-directed observability-based validation for embedded software"],"prefix":"10.1145","volume":"18","author":[{"given":"Jos\u00e9 C.","family":"Costa","sequence":"first","affiliation":[{"name":"INESC-ID\/IST, Technical University of Lisbon, Lisbon, Portugal"}]},{"given":"Jos\u00e9 C.","family":"Monteiro","sequence":"additional","affiliation":[{"name":"INESC-ID\/IST, Technical University of Lisbon, Lisbon, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2013,4,11]]},"reference":[{"volume-title":"Software Testing Techniques","author":"Beizer B.","key":"e_1_2_1_1_1","unstructured":"Beizer , B. 1990. Software Testing Techniques . Second Ed. Van Nostrand Rheinhold , New York . Beizer, B. 1990. Software Testing Techniques. Second Ed. Van Nostrand Rheinhold, New York."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/648019.761103"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/343647.343802"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1383-7621(03)00096-1"},{"volume-title":"Proceedings of the International Conference on Computer Aided Design. 27--32","author":"Costa J.","key":"e_1_2_1_8_1","unstructured":"Costa , J. , Devadas , S. , and Monteiro , J . 2000. Observability analysis of embedded software for coverage-directed validation . In Proceedings of the International Conference on Computer Aided Design. 27--32 . Costa, J., Devadas, S., and Monteiro, J. 2000. Observability analysis of embedded software for coverage-directed validation. In Proceedings of the International Conference on Computer Aided Design. 27--32."},{"volume-title":"Proceedings of the Conference and Exhibition on Design, Automation and Test in Europe. 1572--1575","author":"Costa J.","key":"e_1_2_1_9_1","unstructured":"Costa , J. and Monteiro , J . 2009a. A MILP-based approach to path sensitization of embedded software . In Proceedings of the Conference and Exhibition on Design, Automation and Test in Europe. 1572--1575 . Costa, J. and Monteiro, J. 2009a. A MILP-based approach to path sensitization of embedded software. In Proceedings of the Conference and Exhibition on Design, Automation and Test in Europe. 1572--1575."},{"volume-title":"Proceedings of the IFIP\/IEEE International Conference on Very Large Scale Integration.","author":"Costa J.","key":"e_1_2_1_10_1","unstructured":"Costa , J. and Monteiro , J . 2009b. Observability-based coverage-directed path search using PBO for automatic test vector generation . In Proceedings of the IFIP\/IEEE International Conference on Very Large Scale Integration. Costa, J. and Monteiro, J. 2009b. Observability-based coverage-directed path search using PBO for automatic test vector generation. In Proceedings of the IFIP\/IEEE International Conference on Very Large Scale Integration."},{"volume-title":"Linear Programming and Extensions","author":"Dantzig G.","key":"e_1_2_1_11_1","unstructured":"Dantzig , G. 1998. Linear Programming and Extensions . Princeton University Press . Dantzig, G. 1998. Linear Programming and Extensions. Princeton University Press."},{"volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340","author":"De Moura L.","key":"e_1_2_1_12_1","unstructured":"De Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340 . De Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.92910"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.118"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.558710"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572288"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310023"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277187"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277078"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 16th Annual Network & Distributed System Security Symposium.","author":"Godefroid P.","year":"2008","unstructured":"Godefroid , P. , Levin , M. , Molnar , D. , 2008 . Automated whitebox fuzz testing . In Proceedings of the 16th Annual Network & Distributed System Security Symposium. Godefroid, P., Levin, M., Molnar, D., et al. 2008. Automated whitebox fuzz testing. In Proceedings of the 16th Annual Network & Distributed System Security Symposium."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/154183.154269"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271790"},{"volume-title":"Proceedings of the 15th IEEE International Conference on Automated Software Engineering. 219--227","author":"Gupta N.","key":"e_1_2_1_24_1","unstructured":"Gupta , N. , Mathur , A. , and Soffa , M . 2000. Generating test data for branch coverage . In Proceedings of the 15th IEEE International Conference on Automated Software Engineering. 219--227 . Gupta, N., Mathur, A., and Soffa, M. 2000. Generating test data for branch coverage. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering. 219--227."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288321"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1128020.1128563"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-cdt:20045095"},{"key":"e_1_2_1_28_1","first-page":"105","article-title":"Recursive data structures","volume":"4","author":"Hoare C.","year":"1975","unstructured":"Hoare , C. 1975 . Recursive data structures . Int. J. Parallel Program. 4 , 2, 105 -- 132 . Hoare, C. 1975. Recursive data structures. Int. J. Parallel Program. 4, 2, 105--132.","journal-title":"Int. J. Parallel Program."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1990.131379"},{"volume-title":"Proceedings of the IEEE International High-Level Design Validation and Test Workshop. 21--26","author":"Lajolo M.","key":"e_1_2_1_31_1","unstructured":"Lajolo , M. , Rebaudengo , M. , Reorda , M. , Violante , M. , and Lavagno , L . 2000. Behavioral-level test vector generation for system-on-chip designs . In Proceedings of the IEEE International High-Level Design Validation and Test Workshop. 21--26 . Lajolo, M., Rebaudengo, M., Reorda, M., Violante, M., and Lavagno, L. 2000. Behavioral-level test vector generation for system-on-chip designs. In Proceedings of the IEEE International High-Level Design Validation and Test Workshop. 21--26."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1928028.1928039"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2007.33"},{"volume-title":"Proceedings of the IEEE International Conference on Computer Design. IEEE, 378--381","author":"Lis J.","key":"e_1_2_1_34_1","unstructured":"Lis , J. and Gajski , D . 1988. Synthesis from VHDL . In Proceedings of the IEEE International Conference on Computer Design. IEEE, 378--381 . Lis, J. and Gajski, D. 1988. Synthesis from VHDL. In Proceedings of the IEEE International Conference on Computer Design. IEEE, 378--381."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/135239.135244"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.126"},{"key":"e_1_2_1_37_1","unstructured":"Myers G. Badgett T. Thomas T. and Sandler C. 2004. The Art of Software Testing. Wiley.   Myers G. Badgett T. Thomas T. and Sandler C. 2004. The Art of Software Testing. Wiley."},{"key":"e_1_2_1_38_1","unstructured":"Press W. H. Taukolsky S. A. Vetterling W. T. and Flannery B. P. 1992. Numerical Recipes in C. 2nd Ed. Cambridge University Press.   Press W. H. Taukolsky S. A. Vetterling W. T. and Flannery B. P. 1992. Numerical Recipes in C. 2nd Ed. Cambridge University Press."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/54.844330"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001422"},{"volume-title":"NET. In Proceedings of the 2nd International Conference on Tests and Proofs. 134--153","author":"Tillmann N.","key":"e_1_2_1_42_1","unstructured":"Tillmann , N. and De Halleux, J. 2008. Pex: White box test generation for . NET. In Proceedings of the 2nd International Conference on Tests and Proofs. 134--153 . Tillmann, N. and De Halleux, J. 2008. Pex: White box test generation for. NET. In Proceedings of the 2nd International Conference on Tests and Proofs. 134--153."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132360"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.382180"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.153381"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(01)00190-2"},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer- Aided Design (Digest of Technical Papers). 584--589","author":"Yuan J.","key":"e_1_2_1_47_1","unstructured":"Yuan , J. , Shultz , K. , Pixley , C. , Miller , H. , Aziz , A. , and Austin , T . 1999. Modeling Design Constraints and Biasing in Simulation using BDDs . In Proceedings of the IEEE\/ACM International Conference on Computer- Aided Design (Digest of Technical Papers). 584--589 . Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A., and Austin, T. 1999. Modeling Design Constraints and Biasing in Simulation using BDDs. In Proceedings of the IEEE\/ACM International Conference on Computer- Aided Design (Digest of Technical Papers). 584--589."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2442087.2442090","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2442087.2442090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:35:25Z","timestamp":1750235725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2442087.2442090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["10.1145\/2442087.2442090"],"URL":"https:\/\/doi.org\/10.1145\/2442087.2442090","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2013,3]]},"assertion":[{"value":"2011-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}