Intra- and interdiagram consistency checking of behavioral multiview models. (December 2015)

• Record Type: Journal Article
• Authors: Kaufmann, Petra; Kronegger, Martin; Pfandler, Andreas; Seidl, Martina; Widl, Magdalena
• Is Part Of: Computer languages, systems & structures. Volume 44:Part A(2015)
• Page Start: 72
• Page End: 88
• Publication Date: 2015-12
• Subjects: Multiview modeling -- Unified modeling language -- Consistency checking -- SAT encodings; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2015.08.003
• Languages: English
• ISSNs: 1477-8424

Abstract

Abstract: Multiview modeling languages like UML are a very powerful tool to deal with the ever increasing complexity of modern software systems. By splitting the description of a system into different views—the diagrams in the case of UML—system properties relevant for a certain development activity are highlighted while other properties are hidden. This multiview approach has many advantages for the human modeler, but at the same time it is very susceptible to various kinds of defects that may be introduced during the development process. Besides defects which relate only to one view, it can also happen that two different views, which are correct if considered independently, contain inconsistent information when combined. Such inconsistencies between different views usually indicate a defect in the model and can be critical if they propagate up to the executable system. In this paper, we present an approach to formally verify the reachability of a global state of a set of communicating UML state machines, i.e., we present a solution for an intradiagram consistency checking problem. We then extend this approach to solve an interdiagram consistency checking problem. In particular, we verify whether the message exchange modeled in a UML sequence diagram conforms to a set of communicating state machines. For solving both kinds of problems, we proceed as follows. As a first step, we formalize the semantics of UML state machines and of UML sequence diagrams. In the second step, we build upon this formal semantics and encode both verification tasks as decision problems of propositional logic (SAT) allowing the use of efficient SAT technology. We integrate both approaches in a graphical modeling environment, enabling modelers to use formal verification techniques without any special background knowledge. We experimentally evaluate the scalability of our approach. Abstract : Highlights: Formalization of the semantics of a modeling language similar to UML. Consistency checking via SAT encodings. Direct integration of verification in modeling environment.