Domain partitioning for open reactive systems

ABSTRACT

Testing or model-checking an open reactive system often requires generating a model of the environment. We describe a static analysis for Java that computes a partition of a system's inputs: inputs in the same equivalence class lead to identical behavior. The partition provides a basis for generation of code for a most general environment of the system, i.e., one that exercises all possible behaviors of the system. The partition also helps the generated environment avoid exercising the same behavior multipletimes. Many distributed systems with security requirements can be regarded as open reactive systems whose environment is an adversary-controlled network. We illustrate our approach by applying it to a fault-tolerant and intrusion-tolerant distributed voting system and model-checking the system together with the generated environment.

REFERENCES

• 1: Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.345-357, June 17-19, 1998, Montreal, Quebec, Canada
• 2: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 3: Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.124-133, March 02-04, 1998, Clearwater Beach, Florida, United States
• 4: Gavin Lowe, Casper: A Compiler for the Analysis of Security Protocols, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.18, June 10-12, 1997
• 5: Dahlia Malkhi , Michael K. Reiter, Secure and Scalable Replication in Phalanx, Proceedings of the The 17th IEEE Symposium on Reliable Distributed Systems, p.51, October 20-23, 1998
• 6: Debra J. Richardson and Lori A. Clarke. Partition analysis: A method combining testing and verification. IEEE Transactions on Software Engineering, 11(12):1477-1490, December 1985.
• 7: A. W. Roscoe and M. H. Goldsmith. The perfect "spy" for model-checking cryptoprotocols. In Proc. DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997.
• 8: Scott D. Stoller. Domain partitioning for open reactive systems. Technical Report DAR-02-6, SUNY at Stony Brook, Computer Science Dept., February 2002. Available at www.cs.sunysb.edu/~stoller/partn.html.
• 9: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States