We use UML Machines and UML Machine Systems to give a formal semantics for a simplified part of UML to enable advanced tool support for UMLsec. It allows one to use subsystems in a specific way to group together several kinds of diagrams, giving a formal semantics of a simplified version of UML subsystems and their interactions. Objects, or system components, can communicate by exchanging messages with parameters, which can be used in the subsequent execution. The behavior of actions and activities can be modeled explicitly. Since our semantics builds on UML Machine Systems, it allows us to make use of the treatment of security-critical systems in Chap. 7 to evaluate UML specifications for security aspects. We give consistency conditions for different diagrams in a UML specification. We define notions of refinement and behavioral equivalence, and investigate structural properties, such as substitutivity. Finally we consider rely-guarantee properties for UML specifications and their structural properties.

The proofs for the statements in this chapter are given in Appendix C.