Systematic software testing using VeriSoft-An analysis of the 4ESS™ heart-beat monitor
- 14 August 2002
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in Bell Labs Technical Journal
- Vol. 3 (2) , 32-46
- https://doi.org/10.1002/bltj.2103
Abstract
VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code written in full-fledged programming languages, such as C or C++. Using VeriSoft, we analyzed the 4ESS™ switch Heart-Beat Monitor (HBM), a telephone switching application developed at Lucent Technologies. The 4ESS HBM plays an important role in routing data in the switch and can significantly affect switch performance. Since VeriSoft automatically generates, executes, and evaluates thousands of tests per minute and has complete control over nondeterminism, our analysis revealed HBM behavior that is virtually impossible to detect or test in a traditional lab testing environment. Specifically, we discovered flaws in the existing documentation for this application and unexpected behaviors in the software itself. These results are being used as the basis for an improved design of the HBM software in the 4ESS switch.Keywords
This publication has 24 references indexed in Scilit:
- Automatic synthesis of specifications from the dynamic observation of reactive programsPublished by Springer Nature ,1997
- Improving on the Best: “Like a 1A, Only Better”AT&T Technical Journal, 1995
- Oracles for checking temporal properties of concurrent systemsACM SIGSOFT Software Engineering Notes, 1994
- The Evolution of the 4ESS™ SwitchAT&T Technical Journal, 1994
- Non-concurrency analysisACM SIGPLAN Notices, 1993
- The concurrency workbenchACM Transactions on Programming Languages and Systems, 1993
- Techniques for debugging parallel programs with flowback analysisACM Transactions on Programming Languages and Systems, 1991
- Software for Analytical Development of Communications ProtocolsAT&T Technical Journal, 1990
- Recognizing safety and livenessDistributed Computing, 1987
- A general-purpose algorithm for analyzing concurrent programsCommunications of the ACM, 1983