Automated Encapsulation of UML Activities for Incremental Development and Verification

With their revision ill the UML 2.x standard, activities have heed extended with streaming parameters. This facilitates a reuse-oriented specification style, in which dedicated functions call he contributed by self-contained activities as building blocks: Using streaming parameters; activities call tie composed together ill a quite powerful manner. since streaming parameters relay also pass information while activities are executing. However, to compose them correctly, We must know ill which sequence an activity may emit or accept these streaming parameters. Therefore, we propose special UML state machines that, specify the externally visible behavior of activities. Further; we develop all algorithm to construct these state machines automatically for ail activity based on model checking. Using these behavioral contracts, activities can then be composed without looking at their internal details. Moreover, the contracts Can he used during system verification to reduce the complexity of the analysis.