{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/26314"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/26314","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Systematic testing for actor programs","abstract":"The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Testing such code is notoriously difficult, especially for shared-memory models of programming. The actor model of programming offers a promising alternative for developing concurrent systems based on message passing. In actor-based systems, shared-memory access is not allowed, and the key source of non-determinism is the order in which messages are delivered to and processed by the actors. As a result, errors may occur in actor programs due to the incorrect interleaving of messages, conflicting constraints on what messages can be delivered, or errors in the sequential code within individual actors. The research community has expended a great deal of effort on the testing and verification of concurrent systems. However, much of this effort has been general in nature or focused on shared-memory models. Given the differences in how errors manifest in actor programs, it seems natural that tools and techniques for testing such programs should take into account the particular nature of the actor model. To effectively and efficiently automate the detection of these errors, we propose a set of tools and techniques specifically designed to systematically explore the different behaviors of actor programs resulting from possible message delivery schedules. Specifically, this dissertation presents Basset, a general framework for the systematic testing of actor systems developed with languages that compile to Java bytecode. This framework provides a common set of capabilities designed and implemented to take advantage of actor semantics. By building these capabilities into a language-independent core, they are available for use by any instantiation of the framework. This dissertation illustrates the practicality and effectiveness of this approach by presenting two tool instantiations of the Basset framework: one for the Scala programming language and the other for the ActorFoundry library for Java. The implementation of Basset was built as an extension to Java PathFinder, a popular model checker for Java, in order to leverage capabilities that already exist in that model checker. The Basset framework approach directly enables the relatively quick development of testing environments for actor-based languages and/or libraries that compile to Java bytecode. This dissertation also considers the effectiveness of dynamic partial-order reduction techniques as they relate to the exploration of actor programs. The use of dynamic partial-order reduction speeds up systematic testing by pruning parts of the exploration space. However, the level of potential pruning is highly dependent on the order in which messages are considered for processing. This dissertation presents an evaluation of a number of heuristics for choosing the order in which messages are explored in Basset. The experiments show that the choice of heuristic can affect the number of execution paths that need to be explored by over two orders of magnitude.","abstract_html":"The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Testing such code is notoriously difficult, especially for shared-memory models of programming. The actor model of programming offers a promising alternative for developing concurrent systems based on message passing. In actor-based systems, shared-memory access is not allowed, and the key source of non-determinism is the order in which messages are delivered to and processed by the actors. As a result, errors may occur in actor programs due to the incorrect interleaving of messages, conflicting constraints on what messages can be delivered, or errors in the sequential code within individual actors. The research community has expended a great deal of effort on the testing and verification of concurrent systems. However, much of this effort has been general in nature or focused on shared-memory models. Given the differences in how errors manifest in actor programs, it seems natural that tools and techniques for testing such programs should take into account the particular nature of the actor model. To effectively and efficiently automate the detection of these errors, we propose a set of tools and techniques specifically designed to systematically explore the different behaviors of actor programs resulting from possible message delivery schedules. Specifically, this dissertation presents Basset, a general framework for the systematic testing of actor systems developed with languages that compile to Java bytecode. This framework provides a common set of capabilities designed and implemented to take advantage of actor semantics. By building these capabilities into a language-independent core, they are available for use by any instantiation of the framework. This dissertation illustrates the practicality and effectiveness of this approach by presenting two tool instantiations of the Basset framework: one for the Scala programming language and the other for the ActorFoundry library for Java. The implementation of Basset was built as an extension to Java PathFinder, a popular model checker for Java, in order to leverage capabilities that already exist in that model checker. The Basset framework approach directly enables the relatively quick development of testing environments for actor-based languages and/or libraries that compile to Java bytecode. This dissertation also considers the effectiveness of dynamic partial-order reduction techniques as they relate to the exploration of actor programs. The use of dynamic partial-order reduction speeds up systematic testing by pruning parts of the exploration space. However, the level of potential pruning is highly dependent on the order in which messages are considered for processing. This dissertation presents an evaluation of a number of heuristics for choosing the order in which messages are explored in Basset. The experiments show that the choice of heuristic can affect the number of execution paths that need to be explored by over two orders of magnitude.","abstract_has_math":false,"creators":["Lauterburg, Steven T."],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Marinov, Darko","Agha, Gul A.","Viswanathan, Mahesh","Johnson, Ralph E."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-08-26T15:22:34Z","date_published":"2011-08-26T15:22:34Z","updated_at":"2026-07-22T22:25:26Z","subjects":["systematic testing","concurrency","actor model","message passing","partial-order reduction","model checking"],"languages":["en"],"rights":["Copyright 2011 Steven Thomas Lauterburg."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/26314","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Marinov, Darko","Agha, Gul A.","Viswanathan, Mahesh","Johnson, Ralph E."]},{"key":"dc:creator","label":"Author","values":["Lauterburg, Steven T."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-08-26T15:22:34Z","2013-08-27T10:00:22Z","2011-08"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["systematic testing","concurrency","actor model","message passing","partial-order reduction","model checking"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2011 Steven Thomas Lauterburg."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/26314"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Testing such code is notoriously difficult, especially for shared-memory models of programming. The actor model of programming offers a promising alternative for developing concurrent systems based on message passing. In actor-based systems, shared-memory access is not allowed, and the key source of non-determinism is the order in which messages are delivered to and processed by the actors. As a result, errors may occur in actor programs due to the incorrect interleaving of messages, conflicting constraints on what messages can be delivered, or errors in the sequential code within individual actors. The research community has expended a great deal of effort on the testing and verification of concurrent systems. However, much of this effort has been general in nature or focused on shared-memory models. Given the differences in how errors manifest in actor programs, it seems natural that tools and techniques for testing such programs should take into account the particular nature of the actor model. To effectively and efficiently automate the detection of these errors, we propose a set of tools and techniques specifically designed to systematically explore the different behaviors of actor programs resulting from possible message delivery schedules. Specifically, this dissertation presents Basset, a general framework for the systematic testing of actor systems developed with languages that compile to Java bytecode. This framework provides a common set of capabilities designed and implemented to take advantage of actor semantics. By building these capabilities into a language-independent core, they are available for use by any instantiation of the framework. This dissertation illustrates the practicality and effectiveness of this approach by presenting two tool instantiations of the Basset framework: one for the Scala programming language and the other for the ActorFoundry library for Java. The implementation of Basset was built as an extension to Java PathFinder, a popular model checker for Java, in order to leverage capabilities that already exist in that model checker. The Basset framework approach directly enables the relatively quick development of testing environments for actor-based languages and/or libraries that compile to Java bytecode. This dissertation also considers the effectiveness of dynamic partial-order reduction techniques as they relate to the exploration of actor programs. The use of dynamic partial-order reduction speeds up systematic testing by pruning parts of the exploration space. However, the level of potential pruning is highly dependent on the order in which messages are considered for processing. This dissertation presents an evaluation of a number of heuristics for choosing the order in which messages are explored in Basset. The experiments show that the choice of heuristic can affect the number of execution paths that need to be explored by over two orders of magnitude.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-09T16:14:13Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5)","Made available in DSpace on 2011-08-26T15:22:34Z (GMT). No. of bitstreams: 2 Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5) license.txt: 4067 bytes, checksum: 3ffc0f1cd8ab1ea17b97d76c6953a15a (MD5)","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by William Ingram (wingram2@illinois.edu) on 2011-08-26T15:25:56Z Item is restricted until 2013-08-26T15:25:28Z","Item reinstated by Sarah Shreeves (sshreeve@illinois.edu) on 2013-08-27T10:00:22Z Item was in collections: University of Illinois Dissertations and Theses (ID: 204) Dissertations and Theses - Computer Science (ID: 587) No. of bitstreams: 3 Lauterburg_Steven.pdf.txt: 219191 bytes, checksum: b8af55c52d37033ce1275bdb7d93e32c (MD5) Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5) license.txt: 4067 bytes, checksum: 3ffc0f1cd8ab1ea17b97d76c6953a15a (MD5)","Item released from any restrictions by Sarah Shreeves (sshreeve@illinois.edu) on 2013-08-27T10:00:22Z"]},{"key":"dc:title","label":"Title","values":["Systematic testing for actor programs"]}]}],"canonical_facts":{"dc:contributor":["Marinov, Darko","Agha, Gul A.","Viswanathan, Mahesh","Johnson, Ralph E."],"dc:creator":["Lauterburg, Steven T."],"dc:date":["2011-08-26T15:22:34Z","2013-08-27T10:00:22Z","2011-08"],"dc:description":["The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Testing such code is notoriously difficult, especially for shared-memory models of programming. The actor model of programming offers a promising alternative for developing concurrent systems based on message passing. In actor-based systems, shared-memory access is not allowed, and the key source of non-determinism is the order in which messages are delivered to and processed by the actors. As a result, errors may occur in actor programs due to the incorrect interleaving of messages, conflicting constraints on what messages can be delivered, or errors in the sequential code within individual actors. The research community has expended a great deal of effort on the testing and verification of concurrent systems. However, much of this effort has been general in nature or focused on shared-memory models. Given the differences in how errors manifest in actor programs, it seems natural that tools and techniques for testing such programs should take into account the particular nature of the actor model. To effectively and efficiently automate the detection of these errors, we propose a set of tools and techniques specifically designed to systematically explore the different behaviors of actor programs resulting from possible message delivery schedules. Specifically, this dissertation presents Basset, a general framework for the systematic testing of actor systems developed with languages that compile to Java bytecode. This framework provides a common set of capabilities designed and implemented to take advantage of actor semantics. By building these capabilities into a language-independent core, they are available for use by any instantiation of the framework. This dissertation illustrates the practicality and effectiveness of this approach by presenting two tool instantiations of the Basset framework: one for the Scala programming language and the other for the ActorFoundry library for Java. The implementation of Basset was built as an extension to Java PathFinder, a popular model checker for Java, in order to leverage capabilities that already exist in that model checker. The Basset framework approach directly enables the relatively quick development of testing environments for actor-based languages and/or libraries that compile to Java bytecode. This dissertation also considers the effectiveness of dynamic partial-order reduction techniques as they relate to the exploration of actor programs. The use of dynamic partial-order reduction speeds up systematic testing by pruning parts of the exploration space. However, the level of potential pruning is highly dependent on the order in which messages are considered for processing. This dissertation presents an evaluation of a number of heuristics for choosing the order in which messages are explored in Basset. The experiments show that the choice of heuristic can affect the number of execution paths that need to be explored by over two orders of magnitude.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-09T16:14:13Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5)","Made available in DSpace on 2011-08-26T15:22:34Z (GMT). No. of bitstreams: 2 Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5) license.txt: 4067 bytes, checksum: 3ffc0f1cd8ab1ea17b97d76c6953a15a (MD5)","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by William Ingram (wingram2@illinois.edu) on 2011-08-26T15:25:56Z Item is restricted until 2013-08-26T15:25:28Z","Item reinstated by Sarah Shreeves (sshreeve@illinois.edu) on 2013-08-27T10:00:22Z Item was in collections: University of Illinois Dissertations and Theses (ID: 204) Dissertations and Theses - Computer Science (ID: 587) No. of bitstreams: 3 Lauterburg_Steven.pdf.txt: 219191 bytes, checksum: b8af55c52d37033ce1275bdb7d93e32c (MD5) Lauterburg_Steven.pdf: 701476 bytes, checksum: c5b045d95ff1f49e00c87c174bca6ff3 (MD5) license.txt: 4067 bytes, checksum: 3ffc0f1cd8ab1ea17b97d76c6953a15a (MD5)","Item released from any restrictions by Sarah Shreeves (sshreeve@illinois.edu) on 2013-08-27T10:00:22Z"],"dc:identifier":["http://hdl.handle.net/2142/26314"],"dc:language":["en"],"dc:rights":["Copyright 2011 Steven Thomas Lauterburg."],"dc:subject":["systematic testing","concurrency","actor model","message passing","partial-order reduction","model checking"],"dc:title":["Systematic testing for actor programs"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:26Z"}