Animating Formal Specifications with Inheritance in a DL-Based Framework

Dynamic logic (DL) provides a suitable formal framework to model actions and reasoning about them. <$>\cal OASIS<$> is a language for the specification of object-oriented conceptual models. In our model, specialisation is a relation between classes that defines an inheritance mechanism through static and dynamic partitions. A variant of DL (including the deontic operators for permission, prohibition and obligation) is the formalism used in <$>\cal OASIS<$> to deal with changes of state, triggers, preconditions, protocols and operations. The animation of conceptual models in order to validate the specification is an interesting topic. We have worked on translating <$>\cal OASIS<$> specifications automatically to concurrent environments in order to obtain a prototype useful to validate specifications by animation. The aim of this paper is to show that it is feasible to translate static and dynamic partitions automatically into dynamic logic formulae. Thus, using the same developed schema of animation it is possible to execute <$>\cal OASIS<$> specifications including inheritance.