Model Checking and Code Generation for UML State Machines and Collaborations

摘要: The “Unified Modeling Language” (UML [1]) is generally accepted as the de facto standard notation for analysis and design of object-oriented software systems. It provides diagrams description static, dynamic, architectural aspects systems at different levels detail. In particular, dynamic system behavior can be specified with help interaction (i.e., collaboration or sequence) that describe single runs. A more operational view provided by UML state machines, a variant Statechart introduced Harel [2], are associated instances classes. deliberately encourages use redundant descriptions same system, example during phases development. This redundancy generates an obvious opportunity verification validation techniques to ensure consistency these descriptions. Moreover, formal methods most beneficial when applied abstract We ongoing project develop set tools, tentatively called HUGO, where model checking technology relate machines diagrams. Considering machine “model” “property”, used run diagram indeed realised interacting machines. some cases, absence errors expressed impossibility realise certain “erroneous” interactions. As typical applications checking, we concentrate on control part models largely from data manipulations. While such reveal in designs, coding later implementation stages may still occur. Since specify object’s full detail, propose generate code directly model. Ideally, generation model, raising confidence correctness resulting system.