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