Information flow property preserving transformation of UML interaction diagrams

Abstract

We present an approach for secure information flow property preserving refinement and transformation of UML inspired interaction diagrams.The approach is formally underpinned by trace-semantics.The semantics is sufficiently expressive to distinguish underspecification from explicit nondeterminism. A running example is used to introduce the approach and to demonstrate that it is of practical value.