The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - November/December (2011 vol.37)
pp: 845-857
Gerard J. Holzmann , California Institute of Technology, Pasadena
Rajeev Joshi , California Institute of Technology, Pasadena
Alex Groce , Oregon State University, Corvallis
ABSTRACT
The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances and new theoretical insights, but it has also benefitted from the steady increase in processing speeds and main memory sizes on standard computers. The steady increase in processing speeds, though, ended when chip-makers started redirecting their efforts to the development of multicore systems. For the near-term future, we can anticipate the appearance of systems with large numbers of CPU cores, but without matching increases in clock-speeds. We will describe a model checking strategy that can allow us to leverage this trend and that allows us to tackle significantly larger problem sizes than before.
INDEX TERMS
Software engineering tools and techniques, logic model checking, distributed algorithms, software verification.
CITATION
Gerard J. Holzmann, Rajeev Joshi, Alex Groce, "Swarm Verification Techniques", IEEE Transactions on Software Engineering, vol.37, no. 6, pp. 845-857, November/December 2011, doi:10.1109/TSE.2010.110
REFERENCES
[1] D.L. Bird and C.U. Munoz, "Automatic Generation of Random Self-Checking Test Cases," IBM System J., vol. 22, no. 3, pp. 229-245, 1983.
[2] T. Ball and S.K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces," Proc. Spin Workshop Model Checking Software, pp. 103-122, May 2001.
[3] M.B. Dwyer et al., "Parallel Randomized State-Space Search," Proc. Int'l Conf. Software Eng., pp. 3-12, 2007.
[4] G.E. Moore, "Cramming More Components onto Integrated Circuits," Electronics, vol. 38, no. 8, pp. 114-117, Apr. 1965.
[5] G.J. Holzmann, "Tracing Protocols," AT&T Technical J., vol. 64, no. 10, pp. 2413-2433, Dec. 1985.
[6] G.J. Holzmann, "On Limits and Possibilities of Automated Protocol Analysis," Proc. Sixth Int'l Conf. Protocol Specification, Testing, and Verification, June 1987.
[7] G.J. Holzmann, "Logic Verification of ANSI-C Code with Spin," Proc. Seventh Spin Workshop, pp. 131-147, Aug. 2000.
[8] G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.
[9] G.J. Holzmann and M.H. Smith, "Automating Software Feature Verification," Bell Labs Technical J., vol. 5, no. 2, pp. 72-87, Apr.-June 2000.
[10] G.J. Holzmann and R. Joshi, "Model-Driven Software Verification," Proc. 11th Spin Workshop, pp. 77-92, Apr. 2004.
[11] G.J. Holzmann and D. Bosnacki, "The Design of a Multi-Core Extension to the Spin Model Checker," IEEE Trans. Software Eng., vol. 33, no. 10, pp. 659-674, Oct. 2007.
[12] G.J. Holzmann and M. Florian, "Model Checking with Bounded Context Switching," technical report, JPL LaRS Oct. 2009.
[13] A.E.J. Hyvärinen, T. Junttila, and I. Niemelä, "Strategies for Solving SAT in Grids by Randomized Search," Intelligent Computer Math., pp. 125-140, Springer, 2008.
[14] M. Musuvathi and S. Qadeer, "Fair Stateless Model Checking," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 7-13, June 2008.
[15] K. Ohmura and K. Ueda, "C-Sat: A Parallel SAT Solver for Clusters," Proc. 12th Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 524-537, 2009.
[16] D. Owen and T. Menzies, "Lurch: A Lightweight Alternative to Model Checking," Proc. 15th Int'l Conf. Software Eng. and Knowledge Eng., July 2003.
[17] J. Penix, W. Visser, C. Pasareanu, E. Engstrom, A. Larson, and N. Weininger, "Verifying Time Partitioning in the DEOS Scheduling Kernel," Formal Methods in Systems Design J., vol. 26, no. 2, Mar. 2005.
[18] C. West, "Protocol Validation in Complex Systems," Proc. Symp. Comm. Architecture and Protocols, pp. 303-312, 1989.
[19] S. Qadeer and J. Rehof, "Context-Bounded Model Checking," Proc. Tools and Algorithms for the Construction and Analysis of Systems, pp. 93-107, 2005.
[20] H. Sivaraj and G. Gopalakrishnan, "Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking," Proc. Second Int'l Workshop Parallel and Distributed Model Checking, July 2003.
[21] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model Checking," Programs Int'l J. Automated Software Eng. vol. 10, no. 2, pp. 3-12, Apr. 2003.
[22] C.M. Wintersteiger, Y. Hamadi, and L.de Moura, "A Concurrent Portfolio Approach to SMT Solving," Proc. Int'l Conf. Computer Aided Verification, pp. 715-720, 2009.
1046 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool