{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:53Z","timestamp":1750308113955,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,5,15]],"date-time":"2005-05-15T00:00:00Z","timestamp":1116115200000},"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":[[2005,7]]},"abstract":"<jats:p>This paper presents an approach for the automatic generation of shortest Distinguishing Sequences (DS) with the Uppaal model checker. The presented method is applicable to a large number of extended finite state machines and it will find an optimal result, if a DS sequence exists for the considered automaton. Our approach is situated in an integrated testing environment that is used to generate checking sequences. The generation method is based on a DS model, which is derived from the same test model that is used for generating test cover sets. The problem of generating DS is reduced to the definition of a DS model and for this reason the complexity of our approach depends mainly on the used model checking algorithm. This means, that the presented method is automatically improved, when the model checking algorithm is improved. This includes the generation of optimal DS depending on the ability of the model checker to produce optimal results.<\/jats:p>","DOI":"10.1145\/1082983.1083283","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T19:28:32Z","timestamp":1131391712000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Generating optimal distinguishing sequences with a model checker"],"prefix":"10.1145","volume":"30","author":[{"given":"Christopher","family":"Robinson-Mallett","sequence":"first","affiliation":[{"name":"University of Potsdam, Germany"}]},{"given":"Peter","family":"Liggesmeyer","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Germany"}]},{"given":"Tilo","family":"M\u00fccke","sequence":"additional","affiliation":[{"name":"University of Brunswick, Germany"}]},{"given":"Ursula","family":"Goltz","sequence":"additional","affiliation":[{"name":"University of Brunswick, Germany"}]}],"member":"320","published-online":{"date-parts":[[2005,5,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems","author":"Bengtsson J.","year":"1995","unstructured":"J. Bengtsson , K. G. Larsen . F. Larsson , P. Pettersson , W. Yi. UPPAAL - a tool suite for automatic verification of real-time systems . In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems , 1995 . J. Bengtsson, K. G. Larsen. F. Larsson, P. Pettersson, W. Yi. UPPAAL - a tool suite for automatic verification of real-time systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/186258.187153"},{"key":"e_1_2_1_4_1","unstructured":"M. Clarke O. Grumberg D. A. Peled. Model Checking. MIT Press. Boston 2000.  M. Clarke O. Grumberg D. A. Peled. Model Checking. MIT Press. Boston 2000."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.272431"},{"key":"e_1_2_1_6_1","volume-title":"Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), (34)","author":"Moore E. F.","year":"1956","unstructured":"E. F. Moore . Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), (34) , 1956 . E. F. Moore. Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), (34), 1956."},{"key":"e_1_2_1_7_1","volume-title":"Fault Detection in Digital Circuits","author":"Friedman A. D.","year":"1971","unstructured":"A. D. Friedman , P. R. Menon , Fault Detection in Digital Circuits , Prentice Hall , Englewood Cliffs, NJ , 1971 A. D. Friedman, P. R. Menon, Fault Detection in Digital Circuits, Prentice Hall, Englewood Cliffs, NJ, 1971"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.16602"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277205"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24704-3_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0140-3664(92)90092-S"},{"key":"e_1_2_1_12_1","volume-title":"Proc. 5th Annual Symposium on Switching Circuit Theory and Logical Design, NJ","author":"Hennie F. C.","year":"1964","unstructured":"F. C. Hennie , Fault-Detecting Experiments for Sequential Circuits , Proc. 5th Annual Symposium on Switching Circuit Theory and Logical Design, NJ , 1964 F. C. Hennie, Fault-Detecting Experiments for Sequential Circuits, Proc. 5th Annual Symposium on Switching Circuit Theory and Logical Design, NJ, 1964"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(88)90064-5"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083283","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1082983.1083283","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:14Z","timestamp":1750262894000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5,15]]},"references-count":13,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1082983.1083283"],"URL":"https:\/\/doi.org\/10.1145\/1082983.1083283","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1083274.1083283","asserted-by":"subject"}]},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2005,5,15]]},"assertion":[{"value":"2005-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}