Abstract
Model checking is used to uncover errors by searching the state space of a model. Informed search algorithms use heuristic strategies with problem-specific knowledge to find solutions efficiently. Generally, such heuristics estimate the distance from a given state to a goal state. In this paper, we present seven heuristics for guiding search algorithms through the state-space of actor-based models to a deadlock. In many cases, our methods can find a deadlock more efficiently than uninformed searches. The A* search algorithm guarantees an optimal solution and returns the shortest counter-example when used with an admissible heuristic. These methods are supported by a tool that performs directed search for the deadlock property. The objective is to detect errors that might not be found by simulation or by conventional model checkers before reaching an upper bound or state-space explosion.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agha, G.A., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. Journal of Functional Programming 7(1), 1–72 (1997)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 10 ∧ 20 states and beyond. In: [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, vol. (4976), pp. 428–439 (1986)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Dijkstra, E.: Self-stabilizing systems in spite of distributed control. Communications of the ACM 17(11), 643–644 (1974)
Dräger, K., Finkbeiner, B., Podelski, A.: Directed model checking with distance-preserving abstractions. International Journal on Software Tools for Technology Transfer 11(1), 27–37 (2009)
Edelkamp, S., Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, pp. 57–79. Springer-Verlag New York, Inc. (2001)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer (STTT) 5(2), 247–267 (2004)
Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on Directed Model Checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 65–89. Springer, Heidelberg (2009)
Erlang. Erlang Programming Language Homepage, http://www.erlang.org
Felner, A.: Improving search techniques and using them on different environments. Science (February 2001)
Groce, A., Visser, W.: Heuristics for model checking Java programs. International Journal on Software Tools for Technology Transfer 6(4), 260–276 (2004)
Hewitt, C.: 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 (April 1972)
Hewitt, C.: Viewing control structures as patterns of passing messages. Artificial Intelligence 8(3), 323–364 (1977)
Hewitt, C.: Orgs for scalable, robust, privacy-friendly client cloud computing. IEEE Internet Computing 12(5), 96–99 (2008)
Hewitt, C.: Actorscript(tm): Industrial strength integration of local and nonlocal concurrency for client-cloud computing. CoRR, abs/0907.3330 (2009)
Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8), 666–677 (1978)
Hoffmann, J., Smaus, J.-G., Rybalchenko, A., Kupferschmid, S., Podelski, A.: Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 51–66. Springer, Heidelberg (2007)
Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: The model-checking engine of Rebeca. In: Proceedings of the 21st Annual ACM Symposium on Applied Computing (SAC 2006), Software Verificatin Track, pp. 1810–1815 (April 2006)
Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the jvm platform: a comparative analysis. In: PPPJ 2009: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, pp. 11–20. ACM, New York (2009)
Korf, R.: Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence 27(1), 97–109 (1985)
Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. In: Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology - SIGCOMM 1987, pp. 126–135 (1988)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Pearl, J.: Heuristics: intelligent search strategies for computer problem solving. Addison-Wesley (1984)
Peled, D.: Combining Partial Order Reductions with On-the-fly Model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Russell, S.: Efficient memory-bounded search methods. In: Proceedings of the 10th European Conference on Artificial Intelligence (1992)
Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. In: Proceedings of FACS 2008. Electr. Notes Theor. Comput. Sci., vol. 260, pp. 209–224 (2010)
Scala. Scala Programming Language Homepage, http://www.scala-lang.org
Sirjani, M., Jaghoori, M.M.: Ten Years of Analyzing Actors: Rebeca Experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20–56. Springer, Heidelberg (2011)
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informatica 63(4), 385–410 (2004)
Wijs, A.J., Lisser, B.: Distributed Extended Beam Search for Quantitative Model Checking. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 166–184. Springer, Heidelberg (2007)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proceedings of the 35th Annual Conference on Design Automation Conference - DAC 1998, pp. 599–604 (1998)
Zahavi, U., Felner, A., Schaeffer, J., Sturtevant, N.: Inconsistent heuristics. In: Proceedings of the National Conference on Artificial Intelligence, vol. 22, p. 1211. AAAI Press, MIT Press, Menlo Park, Cambridge (1999, 2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sigurdarson, S.H., Sirjani, M., Björnsson, Y., Reynisson, A.H. (2013). Guided Search for Deadlocks in Actor-Based Models. In: Păsăreanu, C.S., Salaün, G. (eds) Formal Aspects of Component Software. FACS 2012. Lecture Notes in Computer Science, vol 7684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35861-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-35861-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35860-9
Online ISBN: 978-3-642-35861-6
eBook Packages: Computer ScienceComputer Science (R0)