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 OctDisplayed time zone: Eastern Time (US & Canada) change
15:30 - 17:00 | |||
15:30 20mTalk | Akka.js: Towards a portable actor runtime environment AGERE! | ||
15:50 20mTalk | 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 20mTalk | 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 30mOther | Discussion/Panel AGERE! |