@TechReport{KleinGiese2006_ag,
AUTHOR = {Klein, Florian and Giese, Holger},
TITLE = {{Integrated Visual Specification of Structural and Temporal Properties}},
YEAR = {2006},
NUMBER = {tr-ri-06-277},
INSTITUTION = {Computer Science Department, University of Paderborn},
PDF = {uploads/pdf/klein-giese-tr-ri-06-277.pdf},
ABSTRACT = {Complex software systems, and self-adaptive systems in particular, are characterized by complex structures and behavior. For their design, appropriate notations for the specification of properties that integrate structural and temporal aspects are required. The UML has become the de-facto standard in software engineering. Due to the visual nature and accessibility of its structural diagrams, it is widely accepted as the tool of choice for structural modeling. However, for specifying structural properties that go beyond cardinalities, the UML only provides a textual specification language, the OCL. For mixed structural and temporal properties, only proprietary combinations of OCL with temporal logic exist today. The intricate nature of both OCL and temporal logic already causes problems for many software engineers. When communicating with people without a computer science background, e.g. domain experts, employing OCL, any dialect of temporal logic, or a mix of both is usually impracticable. In this paper, we propose two visual languages for specifying requirements, Story Decision Diagrams for structural properties and Timed Story Scenario Diagrams for scenario specifications that integrate structural and temporal aspects. Based on UML Object Diagrams, our approach is capable of specifying both detailed static properties and requirements concerning structural dynamics. Combining structure, first order and temporal logic, it is more expressive than existing visual constraint and scenario languages. Based on the formal semantics we define, it is furthermore possible to turn a specification into a powerful behavioral monitor, enabling the verification of dynamic structural properties of models at run-time or in a model checker.}
}