Actors provide concurrent, distributed, and event-driven autonomous objects which communicate by asynchronous message passing. Actor model benefits from higher level of scalability and actor programs are less error-prone in comparison to programs which are developed based on other concurrency models. However, to guarantee the correctness of mission critical actor programs, verification techniques like model checking is needed. Previously, Basset has been developed based on Java PathFinder, for model checking of Java actor programs. Although it was very successful in verification of a number of Java actor programs, the message scheduling algorithm of Basset causes false negative results for some programs. In addition, using Java PathFinder as the back-end model checker of Basset imposes execution time inefficiencies. To resolve these issues, we developed Jacco as a direct model checking toolset for Java actor programs. We proposed a new message scheduling algorithm and implemented it for Jacco. To illustrate how efficient Jacco works, Basset and Jacco model checking results are compared for a number of case studies. We also used Jacco for model checking of a real-world program in a robotics control system.

Mon 26 Oct
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

15:30 - 17:00: AGERE - Session 4 - Runtime Environments and Discussion at Grand Station 4
agere201515:30 - 15:50
Andrea Peruffo, Gianluca StivanUniCredit R&D, Philipp HallerKTH Royal Institute of Technology
agere201515:50 - 16:10
Elisa Gonzalez BoixVrije Universiteit Brussel, Christophe ScholliersVrije Universiteit Brussel, Nicolas LarreaVUB, Wolfgang De MeuterVrije Universiteit Brussel
agere201516:10 - 16:30
Arvin ZakeriyanUniversity of Tehran, Ehsan Khamespanah, Marjan SirjaniReykjavik University, Ramtin Khosravi
agere201516:30 - 17:00