|
 ABSTRACT
There has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model-checking, in which large finite-state machines are encoded into compact data structures such as Binary Decision Diagrams (BDDs), and are then checked for safety and liveness properties. However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs, even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model-checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types—which are not efficiently representable using arithmetic constraints. In this article we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations in a single model-checker. A system's transitions and fixpoint computations are encoded using both BDD (for boolean and enumerated types) and arithmetic constraints (for integers) representations, where the choice depends on the variable types. Our composite model-checking strategy can be extended to other symbolic representations provided that they support operations such as intersection, union, complement, equivalence checking, and relational image computation. We also present conservative approximation techniques for composite representations to address the undecidability of model-checking on infinite-state systems. We demonstrate the effectiveness of our approach by analyzing two example software specifications which include a mixture of booleans, integers, and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor's cooling system, and the other one is a protocol specification.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995
[doi> 10.1016/0304-3975(94)00202-T]
|
| |
2
|
|
| |
3
|
|
 |
4
|
Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.156-166, October 16-18, 1996, San Francisco, California, United States
|
| |
5
|
|
| |
6
|
|
| |
7
|
|
| |
8
|
|
| |
9
|
BHARADWAJ, R. AND HEITMEYER, C. 1997. Verifying SCR requirements specifications using state exploration. In Proceedings of the 1st ACM SIGPLAN Workshop on Automatic Analysis of Software (Jan.), ACM Press, New York, NY.
|
| |
10
|
|
| |
11
|
|
| |
12
|
|
| |
13
|
|
| |
14
|
|
| |
15
|
|
| |
16
|
BULTAN, T. AND GERBER, R. 1998. Composite model checking with type specific symbolic encodings. Tech. Rep. CS-TR-3871. Department of Computer Science, University of Maryland, College Park, MD.
|
| |
17
|
|
| |
18
|
|
| |
19
|
|
| |
20
|
|
| |
21
|
BURCH, J. R., CLARKE, E. M., AND LONG, D. E. 1991. Symbolic model checking with partitioned transition relations. In Proceedings of the 1991 University of California~Santa Cruz Conference on Advanced Research in VLSI (Edimburgh, Scotland), C. H. S quin, Ed. MIT Press, Cambridge, MA, 49-58.
|
| |
22
|
BURCH, J. R., CLARKE, E. M., LONG, D. E., MCMILLAN, K. L., AND DILL, D. L. 1994. Symbolic model checking for sequential circuit verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 13, 4 (Apr.), 401-424.
|
| |
23
|
BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, L.J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS '90, June), IEEE Press, Piscataway, NJ, 428-439.
|
| |
24
|
William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
[doi> 10.1109/32.708566]
|
| |
25
|
|
| |
26
|
|
| |
27
|
|
| |
28
|
|
| |
29
|
|
| |
30
|
|
| |
31
|
|
| |
32
|
|
| |
33
|
|
| |
34
|
|
| |
35
|
|
| |
36
|
CRIDLIG, R. 1996. Semantic analsis of concurrent ML by abstract model-checking. In Proceedings of the INFINITY International Workshop on Infinite State Systems, 71-86. Tech. Rep. MIP-9614.
|
| |
37
|
|
| |
38
|
ESPARZA, g. 1997. Decidability of model checking for infinite-state concurrent systems. Acta Inf. 34, 2, 85-107.
|
| |
39
|
FISCHER, M. J. AND RABIN, M. O. 1974. Super-exponential complexity of Presburger arithmetic. SIAM-AMS Proc. 7, 27-41.
|
| |
40
|
|
| |
41
|
|
| |
42
|
HALBWACHS, N., RAYMOND, P., AND PROY, Y. 1994. Verification of linear hybrid systems by means of convex approximations. In Proceedings of the International Symposium on Static Analysis (Sept.), B. LeCharlier, Ed. Springer Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Vienna, Austria.
|
| |
43
|
|
| |
44
|
Jesper G. Henriksen , Jakob L. Jensen , Michael E. Jørgensen , Nils Klarlund , Robert Paige , Theis Rauhe , Anders Sandholm, Mona: Monadic Second-Order Logic in Practice, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.89-110, May 19-20, 1995
|
| |
45
|
|
| |
46
|
JACKSON, D. 1996. Nitpick: A checkable specification language. In Proceedings of the Workshop on Formal Methods in Software Practice,
|
| |
47
|
|
| |
48
|
JACKSON, D., NG, Y., AND WING, J. 1998. A Nitpick analysis of mobile IPv6. Tech. Rep. CMU-CS-98-113. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.
|
| |
49
|
|
| |
50
|
KELB, P., DAMS, D., AND GERTH, R. 1995. Practical symbolic model checking of the full tL-calculus using compositional abstractions. Tech. Rep. 95-31. Department of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, Netherlands.
|
| |
51
|
Wayne Kelly , Vadim Maslov , William Pugh , Evan Rosser , Tatiana Shpeisman , David Wonnacott, The Omega Library interface guide, University of Maryland at College Park, College Park, MD, 1995
|
| |
52
|
|
| |
53
|
|
| |
54
|
|
| |
55
|
OPPEN, D. C. 1978. A 222" upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci. 16, 3, 323-332.
|
| |
56
|
|
| |
57
|
|
| |
58
|
SREEMANI, T. AND ATLEE, J. M. 1996. Feasibility of model checking software requirements. In Proceedings of the 11th Annual Conference on Computer Assurance on Proceedings of the 11th Annual Conference on Computer Assurance (COMPASS '96, Gaithersburg, MD, June), IEEE Computer Society, Washington, DC, 77-88.
|
| |
59
|
STENNING, N.V. 1976. A data transfer protocol. Comput. Netw. J. 1, 99-110.
|
| |
60
|
TARSKI, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285-309.
|
| |
61
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2