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, but in no small measure it is also made possible by increases in processing speed and main memory sizes on standard desktop systems. For the time being, though, the increase in CPU speeds has mostly ended as chip-makers are redirecting their efforts to the development of multi-core systems. In the coming years we can expect systems with very large memory sizes, and increasing numbers of CPU cores, but with each core running at a relatively low speed. We will discuss the implications of this important trend, and describe how we can leverage these developments with new tools.
The research described in this paper was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The work was supported in part by NASA’s Exploration Technology Development Program (ETDP) on Reliable Software Engineering.
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
Chien, S., Sherwood, R., Tran, D., et al.: Using Autonomy Flight Software to Improve Science Return on Earth Observing One (EO1). Journal of Aerospace Computing, Information, and Communication (April 2005)
Dwyer, M.B., Elbaum, S.G., et al.: Parallel Randomized State-Space Search. In: Proc. ICSE 2007, pp. 3–12 (2007)
Moore, G.E.: Cramming more components onto integrated circuits. Electronics 38(8) (April 9, 1965)
Gluck, P.R., Holzmann, G.J.: Using Spin Model Checking for Flight Software Verification. In: Proc. 2002 Aerospace Conf., March 2002. IEEE, Big Sky (2002)
Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Rudin, H., West, C. (eds.) Proc. 6th Int. Conf. on Protocol Specification, Testing, and Verification, INWG IFIP, Zurich, Switzerland (June 1987)
Holzmann, G.J.: Logic verification of ANSI-C Code with Spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal 5(2), 72–87 (2000)
Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 76–91. Springer, Heidelberg (2004)
Holzmann, G.J., Bosnacki, D.: The design of a multi-core extension to the Spin model checker. IEEE Trans. On Software Engineering 33(10), 659–674 (2007)
Musuvathi, M., Qadeer, S.: Fair stateless model checking. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), Tucson, AZ, June 7-13 (2008)
Penix, J., Visser, W., Pasareanu, C., Engstrom, E., Larson, A., Weininger, N.: Verifying Time Partitioning in the DEOS Scheduling Kernel. Formal Methods in Systems Design Journal 26(2) (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holzmann, G.J., Joshi, R., Groce, A. (2008). Tackling Large Verification Problems with the Swarm Tool. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)