Design models Formal foundation Behavioral semantics Computational tree logic Graph transformation rules
Issue Date:
2010
Publisher:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Citation:
Volume: 6252 LNCS, Page : 97-111
Abstract:
In software development a system is often viewed by various models at different levels of
abstraction. It is very difficult to maintain the consistency between them for both structural and behavioral
semantics. This paper focuses on a formal foundation for presenting scenarios and reasoning the
synchronization between them. We represent such a synchronization using a transition system, where a state
is viewed as a triple graph presenting the connection of current scenarios, and a transition is defined as a
triple graph transformation rule. As a result, the conformance property can be represented as a
Computational Tree Logic (CTL) formula and checked by model checkers. We define the transition system
using our extension of UML activity diagrams together with Triple Graph Grammars (TGGs) incorporating
Object Constraint Language (OCL). We illustrate the approach with a case study of the relation between a
use case model and a design model. The work is realized using the USE tool. ?? 2010 Springer-Verlag
Berlin Heidelberg.
