TY - GEN
T1 - A framework for state-space exploration of java-based actor programs
AU - Lauterburg, Steven
AU - Dotta, Mirco
AU - Marinov, Darko
AU - Agha, Gul A
PY - 2009/12/1
Y1 - 2009/12/1
N2 - The actor programming model offers a promising model for developing reliable parallel and distributed code. Actors provide flexibility and scalability: local execution may be interleaved, and distributed nodes may operate asynchronously. The resulting nondeterminism is captured by nondeterministic processing of messages. To automate testing, researchers have developed several tools tailored to specific actor systems. As actor languages and libraries continue to evolve, such tools have to be reimplemented. Because many actor systems are compiled to Java bytecode, we have developed Basset, a general framework for testing actor systems compiled to Java bytecode. We illustrate Basset by instantiating it for the Scala programming language and for the ActorFoundry library for Java. Our implementation builds on Java PathFinder, a widely used model checker for Java. Experiments show that Basset can effectively explore executions of actor programs; e.g., it discovered a previously unknown bug in a Scala application.
AB - The actor programming model offers a promising model for developing reliable parallel and distributed code. Actors provide flexibility and scalability: local execution may be interleaved, and distributed nodes may operate asynchronously. The resulting nondeterminism is captured by nondeterministic processing of messages. To automate testing, researchers have developed several tools tailored to specific actor systems. As actor languages and libraries continue to evolve, such tools have to be reimplemented. Because many actor systems are compiled to Java bytecode, we have developed Basset, a general framework for testing actor systems compiled to Java bytecode. We illustrate Basset by instantiating it for the Scala programming language and for the ActorFoundry library for Java. Our implementation builds on Java PathFinder, a widely used model checker for Java. Experiments show that Basset can effectively explore executions of actor programs; e.g., it discovered a previously unknown bug in a Scala application.
UR - http://www.scopus.com/inward/record.url?scp=77952140568&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77952140568&partnerID=8YFLogxK
U2 - 10.1109/ASE.2009.88
DO - 10.1109/ASE.2009.88
M3 - Conference contribution
AN - SCOPUS:77952140568
SN - 9780769538914
T3 - ASE2009 - 24th IEEE/ACM International Conference on Automated Software Engineering
SP - 468
EP - 479
BT - ASE2009 - 24th IEEE/ACM International Conference on Automated Software Engineering
T2 - 24th IEEE/ACM International Conference on Automated Software Engineering, ASE2009
Y2 - 16 November 2009 through 20 November 2009
ER -