Frame conditions in the automatic validation and verification of UML/OCL models: A symbolic formulation of modifies only statements. (December 2018)

• Record Type: Journal Article
• Authors: Przigoda, Nils; Niemann, Philipp; Filho, Jonas Gomes; Wille, Robert; Drechsler, Rolf
• Is Part Of: Computer languages, systems & structures. Volume 54(2018)
• Page Start: 512
• Page End: 527
• Publication Date: 2018-12
• Subjects: UML/OCL models -- Verification and validation -- Behavioral model aspects -- Symbolic formulation -- SAT/SMT; 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.2017.11.002
• Languages: English
• ISSNs: 1477-8424

Abstract

Highlights: A comprehensive and discussion of the pros and cons of the different approaches to deal with frame conditions in behavioral verification of UML/OCL models. A description of conceptual ideas how to integrate frame conditions given by modifies only statements into a symbolic formulation as well as a precise SMT-LIB realization. An evaluation of the actual implementation including a comparison with other approaches. Abstract: Validation and verification of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades—except for UML/OCL where corresponding approaches have been investigated only recently. Among these, the so-called modifies only statements constitute a very promising concept which is complementary to all other approaches. More precisely, instead of allowing arbitrary modifications in principle and prohibiting certain undesired behavior, the statements explicitly describe what is allowed to change. However, this approach to frame conditions has not been considered so far in any of the numerous approaches for the automatic validation and verification of the behavior in UML/OCL models that have been proposed in the last years. Most of these approaches rely on a symbolic formulation of all possible system states and transitions between them. Therefore, in this paper we explain how modifies only statements can be integrated into an existing symbolic formulation. Based on this, we evaluate the applicability of the presented concept and compare it to previous implementations of frame conditions.