UML State Chart Verification with JPF
(1) JPF = explicit state SW model checker ⇒ too generic for UML?
- can check arbitrary Java bytecode programs
- open sourced on SourceForge
- so far mostly used for verification of concurrent applications
- could handle various state chart implementations
(2) Challenges for UML verification
- separate invariant model structure (hierarchy of states, transitions)
from framework implementing UML execution semantics (policy, weak definition)
- make model part suitable for simulation and model checking
- keep implementation overhead in model part low (readability)
- design framework part (execution engine) so that states of the UML model
and the Java program are in line (no "artificial" program states exposed)
- enable traces over UML model events (not bytecode instructions)
- ⇒ purpose UML state chart implementation is testing and verification,
not runtime efficiency (not for production systems)
(3) Benefits
- model can be refined (e.g. actions with side effects) without
the need for another verification tool
- verification can be guided (series of events) and free (exhaustive
search over all possible events)
- various, extensible properties (by means of JPF listener infrastructure):
safety (assertions, ambiguous transitions, ..), temporal (via synchronized
property automata)