Domain Partitioning for Open Reactive Systems
Scott D. Stoller

Testing or model-checking an open reactive system often requires generating a model of the environment. For example, a web server is an open reactive system that interacts with an environment containing browsers, possibly buggy. Many distributed systems with security requirements can be regarded as open reactive systems whose environment contains an adversary-controlled network and adversary-controlled processes. It is often useful to generate a model of a system's most general environment, i.e., one that exercises all possible behaviors of the system. 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. We illustrate this approach by applying it to a fault-tolerant and intrusion-tolerant distributed voting system and using the generated environment to model-check the system.

Paper in ISSTA 2002:    BibTeX    PDF
Revised 24 June 2002

Technical Report (contains more details):    BibTeX    PDF
Revised 24 June 2002

Scott Stoller's Home Page