Extracting FSMs from Object-Z specifications with history invariants

Object-Z with history invariants can present precise and abstract models for complex systems. The system behavior patterns are often implicitly embedded within various state/operational constraints and history invariants. Without explicit system behavior representations, it is difficult to implement those abstract models. In this paper, we present a sound and systematic approach to automatically extract explicit system behaviors (as FSMs) from the abstract Object-Z specifications. Safety and liveness and additional crucial requirements for open systems are ensured.