Policy enforcement and verification with Timed Modeling Spider Diagrams

Timed Modelling Spider Diagrams (TMSDs) are a visual language which supports the modeling of object-oriented systems with time constraints. They are used to define policies in which TMSDs specify admissible evolutions of the state of some instance. We define a process for deriving a rewriting system from a policy specification, so that the generated system defines a language of sequences of basic TMSDs satisfying the policy. Moreover, by identifying the different ways in which the constraints set by the policy can be violated, we can produce special rules whose application results in erroneous sequences. The resulting transformation systems can be used both to simulate possible behaviours when reasoning on the definition of policies and to test policy verification algorithms.