CEV Example Model
(1) Purpose
- demonstrate model translation (UML to Java) in a moderately sized
but non-trivial example (using hierarchy, orthogonal regions etc.)
- demonstrate explicit and implicit statechart properties that can
checked by JPF
- demonstrate guided and non-guided verification
- demonstrate usage of state machine controlled objects (general code)
(2) Scope
- extracted from publicly available final ESAS report
- models flight phases, key events, vehicle configuration and
major abort scenarios of the "1.5 EOR-LOR" reference mission
(3) Defects
- seeded, but mostly from early CEV requirement documents
- explicit safety properties: "no lsamRendezvous without lasJettison",
"no tliBurn without lsamRendezvous", etc. (via assertions)
- implicit safety properties: "ambiguous transition during first stage abort"
- reachability: "SafeHold not reachable"
- shown in guided and scriptless JPF modes