{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:58Z","timestamp":1750308778695,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2006,11]]},"abstract":"<jats:p>This paper considers the problem of testing the communication between components of a timed distributed software system. We assume that communication is specified using timed interface automata and use computational tree logic (CTL) to define coverage criteria that refer to send- and receive-statements and communication paths. Given such a state-based specification of a distributed system and a concrete coverage goal, a model checker is used in order to determine the coverage provided by a finite set of test-cases, expressed using sequence diagrams. If parts of the specification remain uncovered then a goal is derived so that the model checker can be used to generate test cases that increase the coverage provided by the test suite. A major benefit of the presented approach is the generation of a potentially minimal set of test cases with the confidence that every interaction between components is executed during testing. A potential additional benefit of this approach is that it provides a visual description of the state based testing of distributed systems, which may be beneficial in other contexts such as education and program comprehension. The complexity of our approach strongly depends on the input model, the testing goal, and the model checking algorithm, which is implemented in the used tool. While a particular model checker, UPPAAL, was used, it should be relatively straightforward to adapt the approach for use with other CTL based model checkers.<\/jats:p>","DOI":"10.1145\/1218776.1218786","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T19:52:18Z","timestamp":1175802738000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Achieving communication coverage in testing"],"prefix":"10.1145","volume":"31","author":[{"given":"Christopher","family":"Robinson-Mallett","sequence":"first","affiliation":[{"name":"Fraunhofer IESE, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert M.","family":"Hierons","sequence":"additional","affiliation":[{"name":"Brunel University, Uxbridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Liggesmeyer","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"volume-title":"12th International Symposium on Software Reliability Engineering (ISSRE 2001), pp. 276--286. IEEE 2001","author":"Aizenbud-Reshef N.","key":"e_1_2_1_2_1","unstructured":"Aizenbud-Reshef N. , Coverage Analysis for Message Flows , 12th International Symposium on Software Reliability Engineering (ISSRE 2001), pp. 276--286. IEEE 2001 , Aizenbud-Reshef N., Coverage Analysis for Message Flows, 12th International Symposium on Software Reliability Engineering (ISSRE 2001), pp. 276--286. IEEE 2001,"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_4_1","first-page":"108","volume-title":"Timed Interfaces. Proc. of the Second International Conference on Embedded Software, (EMSOFT 2002","author":"Alfaro L.","year":"2002","unstructured":"Alfaro L. de, Henzinger T. A. , Stroelinga M. , Timed Interfaces. Proc. of the Second International Conference on Embedded Software, (EMSOFT 2002 ), 2491 pp. 108 -- 122 . LNCS. Springer , 2002 . Alfaro L. de, Henzinger T. A., Stroelinga M., Timed Interfaces. Proc. of the Second International Conference on Embedded Software, (EMSOFT 2002), 2491 pp. 108--122. LNCS. Springer, 2002."},{"key":"e_1_2_1_5_1","volume-title":"UPPAAL - A Tool Suite for Automatic Verification of Real-Time Systems. Workshop on Verification and Control of Hybrid Systems, DIMACS","author":"Bengtsson J.","year":"1995","unstructured":"Bengtsson J. , Larsen K. G. , Larsson F. , Pettersson P. , Yi W. , UPPAAL - A Tool Suite for Automatic Verification of Real-Time Systems. Workshop on Verification and Control of Hybrid Systems, DIMACS , 1995 . Bengtsson J., Larsen K. G., Larsson F., Pettersson P., Yi W., UPPAAL - A Tool Suite for Automatic Verification of Real-Time Systems. Workshop on Verification and Control of Hybrid Systems, DIMACS, 1995."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/186258.187153"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566196"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1978.231496"},{"key":"e_1_2_1_9_1","unstructured":"Clarke E. M. Grumberg O. Peled D. A. Model Checking. MIT Press. Boston. 2000.  Clarke E. M. Grumberg O. Peled D. A. Model Checking. MIT Press. Boston. 2000."},{"key":"e_1_2_1_10_1","first-page":"52","volume-title":"Branching Time Temporal Logic. Proc. of the Workshop on Logic of Programs","author":"Clarke E. M.","year":"1981","unstructured":"Clarke E. M. , Emerson E. A. , Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Proc. of the Workshop on Logic of Programs . Yorktown Heights, NY, LNCS 131 pp. 52 -- 71 ., Springer Press. 1981 . Clarke E. M., Emerson E. A., Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Proc. of the Workshop on Logic of Programs. Yorktown Heights, NY, LNCS 131 pp. 52--71., Springer Press. 1981."},{"key":"e_1_2_1_11_1","volume-title":"Introduction to the Theory of Finite-State Machines","author":"Gill A.","year":"1962","unstructured":"Gill A. , Introduction to the Theory of Finite-State Machines . McGraw Hill . Berkeley. 1962 . Gill A., Introduction to the Theory of Finite-State Machines. McGraw Hill. Berkeley. 1962."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195402"},{"key":"e_1_2_1_13_1","first-page":"95","volume-title":"Fault-Detecting Experiments for Sequential Circuits. Proc. of the Symposium on Switching Circuit Theory and Logical Design NJ","author":"Hennie F. C.","year":"1964","unstructured":"Hennie F. C. , Fault-Detecting Experiments for Sequential Circuits. Proc. of the Symposium on Switching Circuit Theory and Logical Design NJ , pages 95 -- 110 . 1964 . Hennie F. C., Fault-Detecting Experiments for Sequential Circuits. Proc. of the Symposium on Switching Circuit Theory and Logical Design NJ, pages 95--110. 1964."},{"key":"e_1_2_1_14_1","volume-title":"Proc. 8th Intern. Symp. High Assurance Systems Engineering (HASE'04)","author":"Heimdahl M.","year":"2004","unstructured":"Heimdahl M. , George D. , Weber R. , Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria? Proc. 8th Intern. Symp. High Assurance Systems Engineering (HASE'04) , Tampa, F1, IEEE , 2004 . Heimdahl M., George D., Weber R., Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria? Proc. 8th Intern. Symp. High Assurance Systems Engineering (HASE'04), Tampa, F1, IEEE, 2004."},{"key":"e_1_2_1_15_1","first-page":"232","volume-title":"Proc. of International Conference on Software Engineering (ICSE '03)","author":"Hong H. S.","year":"2003","unstructured":"Hong H. S. , Cha S. D. , Lee I. , Sokolsky O. , Ural H. , Data Flow Testing as Model Checking , Proc. of International Conference on Software Engineering (ICSE '03) , pp. 232 -- 242 , May 2003 . Hong H. S., Cha S. D., Lee I., Sokolsky O., Ural H., Data Flow Testing as Model Checking, Proc. of International Conference on Software Engineering (ICSE '03), pp. 232--242, May 2003."},{"key":"e_1_2_1_16_1","volume-title":"International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002)","author":"Hong H.","year":"2002","unstructured":"Hong H. , Lee I. , Sokolsky O. , Ural H., A Temporal Logic Based Theory of Test Coverage and Generation , International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002) , April 8 --11 , 2002 . Hong H., Lee I., Sokolsky O., Ural H., A Temporal Logic Based Theory of Test Coverage and Generation, International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002), April 8--11, 2002."},{"key":"e_1_2_1_17_1","volume-title":"Generation of Optimized Test suites for UML Statecharts with Time. Testing of Communicating Systems (TestCom'04)","author":"Huhn M.","year":"2004","unstructured":"Huhn M. , M\u00fccke T. , Generation of Optimized Test suites for UML Statecharts with Time. Testing of Communicating Systems (TestCom'04) . Oxford . Springer . 2004 . Huhn M., M\u00fccke T., Generation of Optimized Test suites for UML Statecharts with Time. Testing of Communicating Systems (TestCom'04). Oxford. Springer. 2004."},{"key":"e_1_2_1_18_1","volume-title":"Proc. of Intern. Conf. on Software Engineering","author":"Hutchins M.","year":"1994","unstructured":"Hutchins M. , Foster H. , Goradia T. , Ostrand T. J. , Experiments of the Effectiveness of Dataflow- and Controlflow-Based Test Adequacy Criteria . Proc. of Intern. Conf. on Software Engineering , Sorento, Italy, ACM , 1994 . Hutchins M., Foster H., Goradia T., Ostrand T. J., Experiments of the Effectiveness of Dataflow- and Controlflow-Based Test Adequacy Criteria. Proc. of Intern. Conf. on Software Engineering, Sorento, Italy, ACM, 1994."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1049406"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.272431"},{"key":"e_1_2_1_21_1","first-page":"41","volume-title":"Canadian Conference on Electrical and Computer Engineering, 1","author":"Liu W.","year":"2001","unstructured":"Liu W. , Dasiewicz P. , Component Interaction Testing Using Model Checking , Canadian Conference on Electrical and Computer Engineering, 1 pp. 41 -- 46 , IEEE, 2001 . Liu W., Dasiewicz P., Component Interaction Testing Using Model Checking, Canadian Conference on Electrical and Computer Engineering, 1 pp. 41--46, IEEE, 2001."},{"key":"e_1_2_1_22_1","volume-title":"Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), 34","author":"Moore E. F.","year":"1956","unstructured":"Moore E. F. , Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), 34 . 1956 . Moore E. F., Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), 34. 1956."},{"key":"e_1_2_1_23_1","volume-title":"Proc. 5th Intern. Conf. on Engineering of Complex Computer Systems, ACM","author":"Offutt A. J.","year":"1999","unstructured":"Offutt A. J. , Xiong Y. , Liu S. , Criteria for Generating Specification-based Tests , Proc. 5th Intern. Conf. on Engineering of Complex Computer Systems, ACM , 1999 Offutt A. J., Xiong Y., Liu S., Criteria for Generating Specification-based Tests, Proc. 5th Intern. Conf. on Engineering of Complex Computer Systems, ACM, 1999"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(03)00241-3"},{"key":"e_1_2_1_25_1","first-page":"337","volume-title":"Proc. 5th Intern. Symp. on Programming","author":"Queille J. P.","year":"1982","unstructured":"Queille J. P. , Sifakis J. , Specification and Verification of Concurrent Systems in CESAR , Proc. 5th Intern. Symp. on Programming , pp. 337 -- 351 . 1982 . Queille J. P., Sifakis J., Specification and Verification of Concurrent Systems in CESAR, Proc. 5th Intern. Symp. on Programming, pp. 337--351. 1982."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1083274.1083283"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Software Engineering 2006","author":"Robinson-Mallett C.","year":"2006","unstructured":"Robinson-Mallett C. , Liggesmeyer P. , State Identification and Verification using a Model Checker . Proceedings of the Software Engineering 2006 . GI Edition Lecture Notes in Informatics, Leipzig , March 2006 Robinson-Mallett C., Liggesmeyer P., State Identification and Verification using a Model Checker. Proceedings of the Software Engineering 2006. GI Edition Lecture Notes in Informatics, Leipzig, March 2006"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2006.03.006"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1218776.1218786","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1218776.1218786","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:41Z","timestamp":1750278161000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1218776.1218786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":28,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["10.1145\/1218776.1218786"],"URL":"https:\/\/doi.org\/10.1145\/1218776.1218786","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2006,11]]},"assertion":[{"value":"2006-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}