| Popis: |
This work presents a specification language, called OZS, based on two formalisms: Object-Z and the statecharts. Such a specification style facilitates the modeling of systems with both reactive and functional aspects. The accent is placed on OZS semantics so as to give formal foundations to verification and simulation of OZS models. Every OZS model has a transition system as its semantic interpretation. Untimed and timed versions of the OZS semantics are presented. Both transition system models of an OZS class can be used for verification purposes by model checking. In this work, a real-word example is treated and the resulting specification is model-checked by using the Stanford Temporal Prover environment from Stanford. |
Full Text from ScienceDirect