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

Displayed time zone: Eastern Time (US & Canada) change

15:30 - 17:00
Session 4 - Runtime Environments and DiscussionAGERE! at Grand Station 4
15:30
20m
Talk
Akka.js: Towards a portable actor runtime environment
AGERE!
Andrea Peruffo , Gianluca Stivan UniCredit R&D, Philipp Haller KTH Royal Institute of Technology
15:50
20m
Talk
Connect.js: A cross mobile platform actor library for multi-networked mobile applications
AGERE!
Elisa Gonzalez Boix Vrije Universiteit Brussel, Christophe Scholliers Vrije Universiteit Brussel, Nicolas Larrea VUB, Wolfgang De Meuter Vrije Universiteit Brussel
16:10
20m
Talk
Jacco: More Efficient Model Checking Toolset for Java Actor Programs
AGERE!
Arvin Zakeriyan University of Tehran, Ehsan Khamespanah , Marjan Sirjani Reykjavik University, Ramtin Khosravi
16:30
30m
Other
Discussion/Panel
AGERE!