Environment Assumptions
Motivation
- reduce "false positives" and trivial errors by introducing constraints
on valid (realistic) event sequences (= environment constraints)
- automatically generate constraints that can serve as "flight rules"
Implementation
- given an alphabet of relevant events, use compositional verification
techniques to generate constraint candidates (by running JPF as an oracle)
- encode validated constraints as automata that are executed
synchronuously with the UML state machine, cutting off invalid event
sequences before they could lead to property violations