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.

Dang D.-H., Truong A.-H., Gogolla M.

79.pdf    Gửi cho bạn bè

Từ khóa : Behavioral semantics; Computational tree logic; Design models; Formal foundation; Graph transformation rules; Levels of abstraction; Model checker; Object Constraint Language; Software development; Transition system; Triple-Graph-Grammars; UML activity diagrams; Use case model; Formal languages; Graph theory; Software design; Synchronization; Model checking