Cited By
View all- Abbasi RGhassemi FKhosravi R(2019)Verification of asynchronous systems with an unspecified componentActa Informatica10.1007/s00236-018-0317-x56:2(161-203)Online publication date: 1-Mar-2019
Jacco: more efficient model checking toolset for Java actor programs
Pages 37 - 44
Abstract
Actors provide concurrent, distributed, and event-driven autonomous objects which communicate asynchronously. Actor model benefits from higher level of scalability and actor programs are less error-prone in comparison to programs developed in other concurrent models. However, it does not prevent the racing and concurrency errors. So, to guarantee the correctness of mission critical actor programs, verification techniques like model checking are needed. Previously, Basset has been developed based on Java PathFinder, for model checking of Java actor programs. The message scheduling approach of Basset can cause false negative results as well as and early state space exploration. In addition, using Java PathFinder as the back-end model checker imposes the execution time inefficiencies. To resolve these issues, we developed Jacco as the direct model checking toolset for Java actor programs. We provided a new message scheduling approach and implemented it in Java. To illustrate how efficiently Jacco works, Basset and Jacco model checking results are compared for a number of case studies. We also used Jacco for the model checking of a real-world program in robotics systems.
References
[1]
Akka Java Documentation. http://akka.io/docs/.
[2]
Akka Programming Language Homepage. http://www.akka.io.
[3]
Erlang Programming Language Homepage. http://www.erlang.org.
[4]
Husky Robot Web Page. wiki.ros.org/Robots/Husky.
[5]
Rebeca Home Page. http://www.rebeca-lang.org.
[6]
ROS Web Page. http://www.ros.org.
[7]
Turtlebot Web Page. wiki.ros.org/Robots/Turtlebot.
[8]
G. Agha, I. A. Mason, S. F. Smith, and C. L. Talcott. A foundation for actor computation. J. Funct. Program., 7(1):1– 72, 1997.
[9]
G. A. Agha. ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press series in artificial intelligence. MIT Press, 1990.
[10]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: extracting finitestate models from java source code. In C. Ghezzi, M. Jazayeri, and A. L. Wolf, editors, Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000.
[11]
, pages 439–448. ACM, 2000.
[12]
M. d’Amorim and K. Havelund. Event-based runtime verification of java programs. ACM SIGSOFT Software Engineering Notes, 30(4):1–7, 2005.
[13]
L. Fredlund and H. Svensson. McErlang: a model checker for a distributed functional programming language. In R. Hinze and N. Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 125–136. ACM, 2007.
[14]
C. Hewitt. Description and Theoretical Analysis (Using Schemata) of PLANNER: A Language for Proving Theorems and Manipulating Models in a Robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science, MIT, Apr. 1972.
[15]
J. Hughes. Software testing with QuickCheck. In Z. Horváth, R. Plasmeijer, and V. Zs´ok, editors, Central European Functional Programming School - Third Summer School, CEFP 2009, Budapest, Hungary, May 21-23, 2009 and Komárno, Slovakia, May 25-30, 2009, Revised Selected Lectures, volume 6299 of Lecture Notes in Computer Science, pages 183– 223. Springer, 2009.
[16]
S. Lauterburg, M. Dotta, D. Marinov, and G. A. Agha. A framework for state-space exploration of java-based actor programs. In ASE 2009, 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, November 16-20, 2009, pages 468–479. IEEE Computer Society, 2009.
[17]
S. Lauterburg, R. K. Karmani, D. Marinov, and G. Agha. Evaluating ordering heuristics for dynamic partial-order reduction techniques. In D. S. Rosenblum and G. Taentzer, editors, Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6013 of Lecture Notes in Computer Science, pages 308– 322. Springer, 2010.
[18]
K. Sen and G. Agha. Automated systematic testing of open distributed programs. In L. Baresi and R. Heckel, editors, Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, volume 3922 of Lecture Notes in Computer Science, pages 339–356. Springer, 2006.
[19]
S. Tasharofi, R. K. Karmani, S. Lauterburg, A. Legay, D. Marinov, and G. Agha. TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In H. Giese and G. Rosu, editors, Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings, volume 7273 of Lecture Notes in Computer Science, pages 219–234. Springer, 2012.
[20]
S. Tasharofi, M. Pradel, Y. Lin, and R. E. Johnson. Bita: Coverage-guided, automatic testing of actor programs. In E. Denney, T. Bultan, and A. Zeller, editors, 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11-15, 2013, pages 114–124. IEEE, 2013.
[21]
W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. Autom. Softw. Eng., 10(2):203– 232, 2003.
Index Terms
- Jacco: more efficient model checking toolset for Java actor programs
Recommendations
Efficient TCTL Model Checking Algorithm for Timed Actors
AGERE! '14: Proceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized ControlNon-Polynomial time complexity of model checking algorithms for TCTL properties in dense time is one of the obstacles against using model checking for timed systems. Alternatively, polynomial time algorithms are suggested for model checking discrete ...
Model Checking Multithreaded Programs by Means of Reduced Models
Java is largely used to develop distributed and concurrent systems, but testing multithreaded systems cannot guarantee the quality of the software; in contrast, verification techniques give us a higher confidence about the system and, among these, model ...
Modeling and Verification of Reactive Systems using Rebeca
Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Comments
Information & Contributors
Information
Published In
October 2015
64 pages
ISBN:9781450339018
DOI:10.1145/2824815
- Program Chairs:
- Elisa Gonzalez Boix,
- Philipp Haller,
- Alessandro Ricci,
- Carlos Varela
Copyright © 2015 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 26 October 2015
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
SPLASH '15
Sponsor:
SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity
October 26, 2015
PA, Pittsburgh, USA
Acceptance Rates
Overall Acceptance Rate 19 of 35 submissions, 54%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 100Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)0
Reflects downloads up to 08 Mar 2025
Other Metrics
Citations
Cited By
View all- Abbasi RGhassemi FKhosravi R(2019)Verification of asynchronous systems with an unspecified componentActa Informatica10.1007/s00236-018-0317-x56:2(161-203)Online publication date: 1-Mar-2019
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in