Jacco: More Efficient Model Checking Toolset for Java Actor Programs
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 - 15:50|
|15:50 - 16:10|
|16:10 - 16:30|
|16:30 - 17:00|