Nicoletta de Francesco
Skip Abstract Section
Abstract
Equivalence checking plays a crucial role in formal verification to ensure the correctness of concurrent systems. However, this method cannot be scaled as easily with the increasing complexity of systems due to the state explosion problem. This article presents an efficient procedure, based on heuristic search, for checking Milner's strong and weak equivalence; to achieve higher efficiency, we actually search for a difference between two processes to be discovered as soon as possible, thus the heuristics aims to find a counterexample, even if not the minimum one, to prove nonequivalence. The presented algorithm builds the system state graph on-the-fly, during the checking, and the heuristics promotes the construction of the more promising subgraph. The heuristic function is syntax based, but the approach can be applied to different specification languages such as CCS, LOTOS, and CSP, provided that the language semantics is based on the concept of transition. The algorithm to explore the search space of the problem is based on a greedy technique; GreASE (Greedy Algorithm for System Equivalence), the tool supporting the approach, is used to evaluate the achieved reduction of both state-space size and time with respect to other verification environments.
- Rajeev Alur and Bow-Yaw Wang. 1999. “Next” heuristic for on-the-fly model checking. In Proceedings of the 10th International Conference on Concurrency (CONCUR'99). Jos C. M. Baeten and Sjouke Mauw, Eds., Lecture Notes in Computer Science, vol. 1664, Springer, 98--113. Google Scholar
Digital Library
- Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, and Gigliola Vaglini. 1999. Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59, 537--556. Google ScholarDigital Library
- Gerd Behrmann and Ansgar Fehnker. 2001. Efficient guiding towards cost-optimality in uppaal. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01). Tiziana Margaria and Wang Yi, Eds., Lecture Notes in Computer Science, vol. 2031, Springer, 174--188. Google ScholarDigital Library
- Ahmed Bouajjani, Jean-Claude Fernandez, and Nicolas Halbwachs. 1990. Minimal model generation. In Proceedings of the 2nd International Workshop on Computer Aided Verification (CAV'90). Lecture Notes in Computer Science, vol. 531, Springer, 197--203. Google ScholarDigital Library
- Amar Bouali, Stefania Gnesi, and Salvatore Larosa. 1994. JACK: Just another concurrency kit. The intergration projekt. Bull. EATCS 54, 207--223.Google Scholar
- Julian C. Bradfield and Colin Stirling. 1990. Verifying temporal properties of processes. In Proceedings of the Conference on Theories of Concurrency: Unification and Extension (CONCUR'90). Jos C. M. Baeten and Jan Willem Klop, Eds., Lecture Notes in Computer Science, vol. 458, Springer, 115--125. Google ScholarDigital Library
- Glenn Bruns. 1992. A case study in safety-critical design. In Proceedings of the International Conference on Computer Aided Verification (CAV'92). Gregor von Bochmann and David K. Probst, Eds., Lecture Notes in Computer Science, vol. 663, Springer, 220--233. Google ScholarDigital Library
- Glenn Bruns. 1993. A practical technique for process abstraction. In Proceedings of the International Conference on Concurrency Theory (CONCUR'93). Eike Best, Ed., Lecture Notes in Computer Science, vol. 715, Springer, 37--49. Google ScholarDigital Library
- Doron Bustan and Orna Grumberg. 2003. Simulation-based minimazation. ACM Trans. Comput. Log. 4, 2, 181--206. Google ScholarDigital Library
- Taolue Chen, Bas Ploeger, Jaco van de Pol, and Tim A. C. Willemse. 2007. Equivalence checking for infinite systems using parameterized boolean equation systems. In Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07). 120--135. Google ScholarDigital Library
- Søren Christensen, Hans Huttel, and Colin Stirling. 1995. Bisimulation equivalence is decidable for all context-free processes. Inf. Comput. 121, 2, 143--148. Google ScholarDigital Library
- Edmund M. Clarke and E. Allen Emerson. 2008. Design and synthesis of synchronization skeletons using branching time temporal logic. In 25 Years of Model Checking, Orna Grumberg and Helmut Veith, Eds., Lecture Notes in Computer Science, vol. 5000, Springer, 196--215. Google ScholarDigital Library
- Edmund M. Clarke, Orna Grumberg, and David E. Long. 1994. Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16, 5, 1512--1542. Google ScholarDigital Library
- Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. 1989. Compositional model checking. In Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS'89). IEEE Computer Society, 353--362. Google ScholarDigital Library
- Rance Cleaveland and Steve Sims. 1996. The ncsu concurrency workbench. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV'96). Lecture Notes in Computer Science, vol. 1102, Springer, 394--397. Google ScholarDigital Library
- Antonio Cuomo, Antonella Santone, and Umberto Villano. 2013. CD-form: A clone detector based on formal methods. Sci. Comput. Program. 1, 2013.Google Scholar
- Nicoletta De Francesco, Antonella Santone, and Gigliola Vaglini. 1998. State space reduction by non-standard semantics for deadlock analysis. Sci. Comput. Program. 30, 3, 309--338. Google ScholarDigital Library
- Marco Dorigo and Thomas Stuetzle. 2004. Ant Colony Optimization. MIT Press. Google Scholar
- Matthew B. Dwyer, Suzette Person, and Sebastian Elbaum. 2006. Controlling factors in evaluating path-sensitive error detection techniques. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT'06/FSE'06). ACM Press, New York, 92--104. Google ScholarDigital Library
- Stefan Edelkamp, Alberto Lluch-Lafuente, and Stefan Leue. 2001. Directed explicit model checking with hsf-spin. In Proceedings of the 8th International SPIN Workshop (SPIN'01). Matthew B. Dwyer, Ed., Lecture Notes in Computer Science, vol. 2057, Springer, 57--79. Google ScholarDigital Library
- Stefan Edelkamp and Frank Reffel. 1998. OBDDs in heuristic search. In Proceedings of the 22nd Annual German Conference on Artificial Intelligence: Advances in Artificial Intelligence (KI'98). Otthein Herzog and Andreas Gunter, Eds., Lecture Notes in Computer Science, vol. 1504, Springer, 81--92. Google ScholarDigital Library
- Jean-Claude Fernandez. 1989. An implementation of an efficient algorithm for bisimulation equivalence. Sci. Comput. Program. 13, 1, 219--236. Google ScholarDigital Library
- Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescul, and Mihaela Sighireanu. 1996. CADP - A protocol validation and verification toolbox. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV'96). Lecture Notes in Computer Science, vol. 1102, Springer, 437--440. Google ScholarDigital Library
- Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier. 1993. Symbolic equivalence checking. In Proceedings of the 5th International Conference on Computer Aided Verification (CAV'93). Lecture Notes in Computer Science, vol. 697, Springer, 85--96. Google ScholarDigital Library
- Jean-Claude Fernandez and Laurent Mounier. 1991. “On the fly” verification of behavioural equivalences and preorders. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV'91). Lecture Notes in Computer Science, vol. 575, Springer, 181--191. Google ScholarDigital Library
- Gianpiero Francesca, Antonella Santone, Gigliola Vaglini, and Maria Luisa Villani. 2011. Ant colony optimization for deadlock detection in concurrent systems. In Proceedings of the 35th Annual IEEE Computer Software and Applications Conference (COMPSAC'11). 108--117. Google ScholarDigital Library
- Raffaella Gentilini, Carla Piazza, and Alberto Policriti. 2003. From bisimulation to simulation: Coarsest partition problems. J. Autom. Reason. 31, 1, 73--103. Google ScholarDigital Library
- Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032, Springer. Google ScholarDigital Library
- Patrice Godefroid and Sarfraz Khurshid. 2002. Exploring very large state spaces using genetic algorithms. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02). Joost-Pieter Katoen and Perdita Stevens, Eds., Lecture Notes in Computer Science, vol. 2280, Springer, 266--280. Google ScholarDigital Library
- Jens C. Godskesen, Kim G. Larsen, and Michael Zeeberg. 1989. TAV - Tools for Automatic Verification: Users Manual. http://books.google.com/books?id=jiaJYgEACAAJ.Google Scholar
- Susanne Graf, Bernhard Steffen, and Gerald Luttgen. 1996. Compositional minimisation of finite state systems using interface specifications. Formal Asp. Comput. 8, 5, 607--616. Google ScholarCross Ref
- Alex Groce and Willem Visser. 2002. Heuristic model checking for java programs. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software (SPIN'02). Dragan Bosnacki and Stefan Leue, Eds., Lecture Notes in Computer Science, vol. 2318, Springer, 242--245. Google ScholarDigital Library
- Dilian Gurov and Bruce Kapron. 1998. The context management application server element. http://webhome.cs.uvic.ca/˜bmkapron/ccs.html.Google Scholar
- Eric A. Hansen and Shlomo Zilberstein. 2001. LAO*: A heuristic search algorithm that finds solutions with loops. Artif. Intell. 129, 1--2, 35--62. Google ScholarDigital Library
- Claude Jard and Thierry Jeron. 1991. Bounded-memory algorithms for verification on-the-fly. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV'91). Springer, 192--202. Google ScholarDigital Library
- Rune M. Jensen, Randal E. Bryant, and Manuela M. Veloso. 2002. SetA*: An efficient bdd-based heuristic search algorithm. In Proceedings of the National Conference on Artificial Intelligence (AAAI/IAAI'02). 668--673. Google ScholarDigital Library
- Paris C. Kanellakis and Scott A. Smolka. 1990. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86, 1, 43--68. Google ScholarDigital Library
- Antonin Kucera and Petr Jancar. 2006. Equivalence-checking on infinite-state systems: Techniques and results. Theory Pract. Logic Program. 6, 3, 227--264. Google ScholarDigital Library
- Eric Madelaine and Didier Vergamini. 1990. Finiteness conditions and structural construction of automata for all process algebras. In Proceedings of the 2nd International Workshop on Computer Aided Verification (CAV'90). Lecture Notes in Computer Science, vol. 531, Springer, 353--363. Google ScholarDigital Library
- Ambuj Mahanti and Amitava Bagchi. 1985. AND/OR graph heuristic search methods. J. ACM 32, 1, 28--51. Google ScholarDigital Library
- Ambuj Mahanti, Supriyo Ghose, and Samir K. Sadhukhan. 2003. A framework for searching and/or graphs with cycles. CoRR cs.AI/0305001.Google Scholar
- Nicola Mazzocca, Antonella Santone, Gigliola Vaglini, and Valeria Vittorini. 2002. Efficient model checking of properties of a distributed application: A multimedia case study. Softw. Test. Verif. Reliab. 12, 1, 3--21.Google ScholarCross Ref
- Kenneth L. McMillan. 1993. Symbolic Model Checking. Kluwer. Google ScholarDigital Library
- Robin Milner. 1989. Communication and Concurrency. Prentice Hall. Google ScholarDigital Library
- M. Oliver Moller and Rajeev Alur. 2001. Heuristics for hierarchical partitioning with application to model checking. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01). Tiziana Margaria and Thomas F. Melham, Eds., Lecture Notes in Computer Science, vol. 2144, Springer, 71--85. Google ScholarDigital Library
- Robert Paige and Robert Endre Tarjan. 1987. Three partition refinement algorithms. SIAM J. Comput. 16, 6, 973--989. Google ScholarDigital Library
- Atanas N. Parashkevov and Jay Yantchev. 1996. ARC - A tool for efficient refinement and equivalence checking for csp. In Proceedings of the IEEE International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP'96). 68--75.Google Scholar
- Judea Pearl. 1984. Heuristics - Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley. Google ScholarDigital Library
- Doron Peled. 1993. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference on Computer Aided Verification (CAV'93). Lecture Notes in Computer Science, vol. 697, Springer, 409--423. Google ScholarDigital Library
- Jean-Pierre Queille and Joseph Sifakis. 1982. Specification and verification of concurrent systems in cesar. In Proceedings of the 5th Colloquium on International Symposium on Programming. Mariangiola Dezani-Ciancaglini and Ugo Montanari, Eds., Lecture Notes in Computer Science, vol. 137, Springer, 337--351. Google ScholarDigital Library
- David A. Ramos and Dawson R. Engler. 2011. Practical, low-effort equivalence verification of real code. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). 669--685. Google ScholarDigital Library
- Antonella Santone. 2002. Automatic verification of concurrent systems using a formula-based compositional approach. Acta Inf. 38, 8, 531--564.Google ScholarCross Ref
- Antonella Santone. 2003. Heuristic search + local model checking in selective mu-calculus. IEEE Trans. Softw. Engin. 29, 6, 510--523. Google ScholarDigital Library
- Antonella Santone and Gigliola Vaglini. 2012. Abstract reduction in directed model checking ccs processes. Acta Inf. 49, 5, 313--341. Google ScholarDigital Library
- Antonella Santone, Gigliola Vaglini, and Maria Luisa Villani. 2013. Incremental construction of systems: An efficient characterization of the lacking sub-system. Sci. Comput. Program. 78, 9, 1346--1367.Google ScholarCross Ref
- Colin Stirling and David Walker. 1991. Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89, 1, 161--177. Google ScholarDigital Library
- Antti Valmari. 1992. A stubborn attack on state explosion. Formal Meth. Syst. Des. 1, 4, 297--322. Google ScholarDigital Library
- C. Han Yang and David L. Dill. 1998. Validation with guided search of the state space. In Proceedings of the 35th Annual Design Automation Conference (DAC'98). 599--604. Google ScholarDigital Library
Index Terms
- GreASE: A Tool for Efficient “Nonequivalence” Checking
Recommendations
An integrated environment for HDL verification
IVC '95: Proceedings of the 4th IEEE International Verilog HDL ConferenceThe functional verification of a digital design is an expensive step in the design process. As designs become more complex, simulation is challenged throughout the design and verification process, both at the low level (implementation verification), to ...
Ant Colony Optimization for Deadlock Detection in Concurrent Systems
COMPSAC '11: Proceedings of the 2011 IEEE 35th Annual Computer Software and Applications ConferenceEnsuring deadlock freedom is one of the most critical requirements in the design and validation of concurrent systems. The biggest challenge toward the development of effective deadlock detection schemes remains the state-space explosion problem when ...
Pragmatic equivalence and safety checking in Cryptol
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verificationCryptol is programming a language designed for specifying and programming cryptographic algorithms. In order to meet high-assurance requirements, Cryptol comes with a suite of formal-methods based tools allowing users to perform various program ...
Comments