TY - JOUR
T1 - Swarm verification techniques
AU - Holzmann, Gerard J.
AU - Joshi, Rajeev
AU - Groce, Alex
N1 - Funding Information:
The research described in this paper was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the US National Aeronautics and Space Administration (NASA). The work was supported in part by NASA’s Exploration Technology Development Program (ETDP) on Reliable Software Engineering.
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - Software engineering tools and techniques
KW - distributed algorithms
KW - logic model checking
KW - software verification
UR - http://www.scopus.com/inward/record.url?scp=79953213564&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79953213564&partnerID=8YFLogxK
U2 - 10.1109/TSE.2010.110
DO - 10.1109/TSE.2010.110
M3 - Article
AN - SCOPUS:79953213564
SN - 0098-5589
VL - 37
SP - 845
EP - 857
JO - IEEE Transactions on Software Engineering
JF - IEEE Transactions on Software Engineering
IS - 6
M1 - 5661793
ER -