Validation of Visual Contracts for Services

Visual modeling languages have specialized diagrams to represent behavior and concepts. This diagram specialization has drawbacks like the dif-ficulty to represent the effects of actions. We claim that visual contracts can de-scribe actions in a more complete and integrated way. In this paper, we propose a visual contract notation. Its semantics is illustrated by a mapping to Alloy. Thanks to this notation, the modeler can specify, within one diagram, an action and its effects. The modeler can also simulate the contract. These visual con-tracts can be used to specify IT services and check their specifications. As such they contribute to business/IT alignment. Our visual contracts take elements from several UML diagrams and are based on set-theory and on RM-ODP.