Publications of the University of Bremen Database Systems Group

[Burgueno et al., 2017]
Loli Burgueno, Frank Hilken, Antonio Vallecillo, and Martin Gogolla. Testing Transformation Models Using Classifying Terms. In Esther Guerra and Mark van den Brand, editors, Proc. 10th Int. Conf. Model Transformation (ICMT 2017), pages 69-85. Springer, LNCS 10374, 2017.
Testing the correctness of the specication of a model transformation can be as hard as testing the model transformation itself. Besides, this test has to wait until at least one implementation is available. In this paper we explore the use of tracts and classifying terms to test the correctness of a model transformation specication (a transformation model) on its own, independently from any implementation. We have validated the approach using two experiments and report on the problems and achievements found concerning conceptual and tooling aspects.
(16 pages, PDF: 374kb via HTTP)


[Gabmeyer et al., 2017]
Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl, Martin Gogolla, and Gerti Kappel. A Feature-Based Classification of Formal Verification Techniques for Software Models. Software and Systems Modeling, 2017. DOI: 10.1007/s10270-017-0591-z, Online 2017-03-27.
Software models are the core development artifact in model-based engineering (MBE). The MBE paradigm promotes the use of software models to describe structure and behavior of the system under development and proposes the automatic generation of executable code from the models. Thus, defects in the models most likely propagate to executable code. To detect defects already at the modeling level, many approaches propose to use formal verification techniques to ensure the correctness of these models. These approaches are the subject of this survey. We review the state-of-the-art of formal verification techniques for software models and provide a feature-based classification that allows us to categorize and compare the different approaches.
(26 pages, PDF: 310kb via HTTP)


[Gogolla et al., 2017a]
Martin Gogolla, Frank Hilken, Khanh-Hoang Doan, and Nisha Desai. Checking UML and OCL Model Behavior with Filmstripping and Classifying Terms. In Sebastian Gabmeyer and Einar Broch Johnsen, editors, Proc. 11th Int. Conf. Tests and Proofs (TAP 2017), pages 119-128. Springer, LNCS 10375, 2017.
This tool paper discusses how model behavior expressed in a UML and OCL model can be analysed with filmstrips and classifying terms in the tool USE. Classifying terms are a means for systematic construction of test cases. In the case of behavior models, these test cases correspond to testing the model with different sequence diagrams. We explain how behavior analysis can be carried out in the tool. We discuss lessons learnt from the case study and how conceptual and technical support can be improved.
(10 pages, PDF: 467kb via HTTP)


[Gogolla et al., 2017b]
Martin Gogolla, Frank Hilken, Philipp Niemann, and Robert Wille. Formulating Model Verification Tasks Prover-Independently as UML Diagrams. In Anthony Anjorin and Huascar Espinoza, editors, Proc. 13th European Conf. Modeling Foundations and Application (ECMFA 2017), pages 232-247. Springer, LNCS 10376, 2017.
The success of Model-Driven Engineering (MDE) relies on the quality of the employed models. Thus, quality assurance through validation and verification has a tradition within MDE. But model verification is typically done in the context of specialized approaches and provers. Therefore, verification tasks are expressed from the viewpoint of the chosen prover and approach requiring particular expertise and background knowledge. This contribution suggests to take a new view on verification tasks that is independent from the employed approach and prover. We propose to formulate verifications tasks in terms of the used modeling language itself, e.g. with UML and OCL. As prototypical example tasks we show how (a) questions concerning model consistency can be expressed with UML object diagrams and (b) issues regarding state reachability can be defined with UML sequence diagrams.
(16 pages, PDF: 498kb via HTTP)


[Gogolla et al., 2017c]
Martin Gogolla, Antonio Vallecillo, Loli Burgueno, and Frank Hilken. Employing Classifying Terms for Testing Model Transformations. In Jan Jürjens and Kurt Schneider, editors, Proc. Software Engineering (2017), pages 91-92. GI, LNI 267, 2017.
Our contribution proposes a new technique for developing test cases for UML and OCL models, based on an approach that automatically constructs object models for class models enriched by OCL constraints. By guiding the construction process through so-called classifying terms, the built test cases in form of object models are classified into equivalence classes. Classifying terms are general OCL terms on a class model that calculate a characteristic value for each object model. Each equivalence class is then defined by the set of object models with identical characteristic values and with one canonical representative object model. By inspecting these object models, a developer can explore properties of the class model and its constraints.
(2 pages, PDF: 399kb via HTTP)


[Balaban et al., 2016]
Mira Balaban, Phillipa Bennett, Khanh-Hoang Doan, Geri Georg, Martin Gogolla, Igal Khitron, and Michael Kifer. A Comparison of Textual Modeling Languages: OCL, Alloy, FOML. In Achim D. Brucker, Jordi Cabot, and Adolfo Sanchez-Barbudo Herrera, editors, Proc. Workshop OCL and Textual Modelling (2016), pages 57-72. CEUR WS Proceedings 1756, 2016.
Textual modeling languages are used in model-driven engineering for a variety of purposes. Among the most important purposes are querying a model and formulating restrictions like state invariants or operation pre- and postconditions. This paper compares three such languages. OCL augments UML as a precise language that provides constraint and object query expressions that cannot otherwise be expressed by a diagrammatic notation. Alloy is a simple but expressive logic based on the notion of relations. FOML is a logic rule language that supports object modeling, analysis, and inference. The paper shows typical models in each of the three languages and discusses similarities of and differences between the languages.
(16 pages, PDF: 472kb via HTTP)


[Bill et al., 2016]
Robert Bill, Martin Gogolla, and Manuel Wimmer. On Leveraging UML/OCL for Model Synchronization. In Tanja Mayerhofer, Alfonso Pierantonio, Bernhard Schaetz, and Dalila Tamzalit, editors, Proc. Workshop Models and Evolution (2016), pages 20-29. CEUR WS Proceedings 1706, 2016.
Modelling complex system often results in different but overlapping modelling artifacts which evolve independently. Thus, inconsistencies may arise which lead to unintended effects on the modelled system. To mitigate this situation, model synchronization is seen as a recurring and crucial maintenance task which requires to restore consistency between multiple models using the most suitable changes. Currently, different languages and tools are used for inter-model consistency management than for intra-model consistency where UML/ OCL is an accepted solution. Consequently, the result of synchronizing models solely based on inter-model constraints might result into inappropriately evolved models w.r.t. intra-model constraints. In this paper, we present a synchronization model formalized in UML/OCL which covers explicit consistency and change models including costs and which considers both, inter-model and intra-model constraints at the same time. Instances of this synchronization model represent successful synchronization scenarios. In particular, models can be synchronized, also taking into account their predecessor versions, by finding a constraint violation-free extension of a partial model including those instances which may be optimized for minimal cost. We prototypically implemented this approach using a model finder to automatically retrieve synchronized models and the change operations to compute them by completing the partial model.
(10 pages, PDF: 1463kb via HTTP)


[Brucker et al., 2016]
Achim D. Brucker, Jordi Cabot, Gwendal Daniel, Martin Gogolla, Adolfo Sanchez-Barbudo Herrera, Frank Hilken, Frederic Tuong, Edward D. Willink, and Burkhart Wolff. Recent Developments in OCL and Textual Modelling. In Achim D. Brucker, Jordi Cabot, and Adolfo Sanchez-Barbudo Herrera, editors, Proc. Workshop OCL and Textual Modelling (2016), pages 157-165. CEUR WS Proceedings 1756, 2016.
The panel session of the 16th OCL workshop featured a lightning talk session for discussing recent developments and open questions in the area of OCL and textual modelling. During this session, the OCL community discussed, stimulated through short presentations by OCL experts, tool support, potential future extensions, and suggested initiatives to make the textual modelling community even more successful. This collaborative paper, to which each OCL expert contributed one section, summarises the discussions as well as describes the recent developments and open questions presented in the lightning talks.
(9 pages, PDF: 816kb via HTTP)


[Burgueno et al., 2016]
Loli Burgueno, Frank Hilken, Antonio Vallecillo, and Martin Gogolla. Generating Effective Test Suites for Model Transformations using Classifying Terms. In Huseyin Ergin, Richard F. Paige, Eugene Syriani, Steffen Zschaler, and Moussa Amrani, editors, Proc. Workshop Verification of Model Transformation (VOLT 2016), pages 48-57. CEUR WS Proceedings 1693, 2016.
Generating sample models for testing a model transformation is no easy task. This paper explores the use of classifying terms and stratified sampling for developing richer test cases for model transformations. Classifying terms are used to define the equivalence classes that characterize the relevant subgroups for the test cases. From each equivalence class of object models, several representative models are chosen depending on the required sample size. We compare our results with test suites developed using random sampling, and conclude that by using an ordered and stratified approach the coverage and effectiveness of the test suite can be significantly improved.
(10 pages, PDF: 232kb via HTTP)


[Doan et al., 2016]
Khanh-Hoang Doan, Martin Gogolla, and Frank Hilken. Towards a Developer-Oriented Process for Verifying Behavioral Properties in UML and OCL Models. In Paolo Milazzo, Daniel Varro, and Manuel Wimmer, editors, Proc. STAF 2016 Workshops, Workshop Human-Oriented Formal Methods, pages 207-220. Springer, LNCS 9946, 2016.
Validation and verification of models in the software development design phase have a great potential for general quality improvement within software engineering. A system modeled with UML and OCL can be checked thoroughly before performing further development steps. Verifying not only static but also dynamic aspects of the model will reduce the cost of software development. In this paper, we introduce an approach for automatic behavioral property verification. An initial UML and OCL model will be enriched by frame conditions and then transformed into a (so-called) filmstrip model in which behavioral characteristics can be checked. The final step is to verify a property, which can be added to the filmstrip model in form of an OCL invariant. In order to make the process developer-friendly, UML diagrams can be employed for various purposes, in particular for formulating the verification task and the verification result.
(15 pages, PDF: 513kb via HTTP)


[Gogolla and Cabot, 2016]
Martin Gogolla and Jordi Cabot. Continuing a Benchmark for UML and OCL Design and Analysis Tools. In Paolo Milazzo, Daniel Varro, and Manuel Wimmer, editors, Proc. STAF 2016 Workshops, Workshop Model-Driven Engineering, Logic and Optimization (MELO 2016), pages 289-302. Springer, LNCS 9946, 2016.
UML and OCL are frequently employed languages in model-based engineering. OCL is supported by a variety of design and analysis tools having different scopes, aims and technological corner stones. The spectrum ranges from treating issues concerning formal proof techniques to testing approaches, from validation to verification, and from logic programming and rewriting to SATbased technology. This paper presents steps towards a well-founded benchmark for assessing UML and OCL validation and verification techniques. It puts forward a set of UML and OCL models together with particular questions centered around OCL and the notions consistency, independence, consequences, and reachability. Furthermore aspects of integer arithmetic and aggregations functions (in the spirit of SQL functions as COUNT or SUM) are discussed. The claim of the paper is not to present a complete benchmark. It is intended to continue the development of further UML and OCL models and accompanying questions within the modeling community having the aim to obtain an overall accepted benchmark.
(13 pages, PDF: 323kb via HTTP)


[Gogolla and Hilken, 2016]
Martin Gogolla and Frank Hilken. Model Validation and Verification Options in a Contemporary UML and OCL Analysis Tool. In Andreas Oberweis and Ralf Reussner, editors, Proc. Modellierung (MODELLIERUNG'2016), pages 203-218. GI, LNI 254, 2016.
Modern systems and their architectures are getting more complex than ever. Development strategies, like model-driven engineering (MDE), help to abstract architectures and provide a promising way to deal with the complexity. Thus, the importance for the underlying models to be correct arises. Today's validation and verification tools should support the developer in generating test cases and provide good concepts for fault detection. In this contribution, we introduce and structure essential use cases for model exploration, validation and verification that help developers find faults in model descriptions. Along with the use cases, we demonstrate the model validator of the USE tool, a modern instance finder for UML and OCL models based on an implementation of relational logic and present the results and findings from the tool.
(16 pages, PDF: 329kb via HTTP)


[Gogolla and Vallecillo, 2016]
Martin Gogolla and Antonio Vallecillo. Views on UML Interactions as Spreadsheet Queries. In Paolo Milazzo, Daniel Varro, and Manuel Wimmer, editors, Proc. STAF 2016 Workshops, Workshop Software Engineering Methods in Spreadsheets (SEMS 2016), pages 394-400. Springer, LNCS 9946, 2016.
This paper explores the use of table-based representation for artifacts occurring in model-driven development as opposed to graph-based representation. As an example for table-based representation of models, we explain how views on object interaction that are traditionally represented as UML sequence or communication diagrams can be realized by spreadsheet queries.
(6 pages, PDF: 654kb via HTTP)


[Hamann et al., 2016]
Lars Hamann, Martin Gogolla, and Nisha Desai. On the Support of Qualified Associations in OCL. In Achim D. Brucker, Jordi Cabot, and Adolfo Sanchez-Barbudo Herrera, editors, Proc. Workshop OCL and Textual Modelling (2016), pages 3-15. CEUR WS Proceedings 1756, 2016.
Associations are the glue that keeps items in object-oriented systems together. In UML qualified associations are used to express additional information about access to connected objects. From an implementation point of view, qualified associations can be used to define access to multi-dimensional data structures like arrays. From a conceptual point of view, they can be looked at as being ternary associations with particular OCL constraints expressing the multiplicities. Qualified associations are only partly described in the OCL standard, for example, it is not clear how to access all qualifier values for a qualified object. This paper takes up such questions and makes proposals for the support of qualified associations in the context of OCL.
(14 pages, PDF: 885kb via HTTP)


[Hilken and Gogolla, 2016a]
Frank Hilken and Martin Gogolla. User Assistance Characteristics of the USE Model Checking Tool. In Catherine Dubois, Paolo Masci, and Dominique Mery, editors, Proc. Workshop Formal Integrated Development Environments (FIDE 2016), pages 91-97. EPTCS 240, 2016.
The Unified Modeling Language (UML) is a widely used general purpose modeling language. Together with the Object Constraint Language (OCL), formal models can be described by defining the structure and behavior with UML and additional OCL constraints. In the development process for formal models, it is important to make sure that these models are (a) correct, i.e. consistent and complete, and (b) testable in the sense that the developer is able to interactively check model properties. The USE tool (UML-based Specification Environment) allows both characteristics to be studied. We demonstrate how the tool supports modelers to analyze, validate and verify UML and OCL models via the use of several graphical means that assist the modeler in interpreting and visualizing formal model descriptions. In particular, we discuss how the so-called USE model validator plugin is integrated into the USE environment in order to allow non domain experts to use it and construct object models that help to verify properties like model consistency.
(15 pages, PDF: 665kb via HTTP)


[Hilken and Gogolla, 2016b]
Frank Hilken and Martin Gogolla. Verifying Linear Temporal Logic Properties in UML/OCL Class Diagrams Using Filmstripping. In Paris Kitsos, editor, Proc. Digital System Design (DSD'2016), pages 708-713. IEEE, 2016.
Testing system behavior in real world applications often requires analyzing properties over multiple system states to ensure that operations do not interfere with each other in ways that are not desired. In UML class diagrams, behavior is specified using operations with pre- and postconditions, which alone are not sufficient to formulate temporal properties spanning multiple system states and, thus, require additional description means. For this purpose, multiple extensions of OCL with linear temporal logic (LTL) exist, which provide a formalism to describe temporal properties. Using so-called filmstrip models, this paper provides formal semantics for OCL enhanced by LTL through a translation into standard OCL on the basis of class diagrams and enables verifying these temporal properties using existing model checking tools.
(8 pages, PDF: 218kb via HTTP)


[Hilken et al., 2016a]
Frank Hilken, Martin Gogolla, Loli Burgueno, and Antonio Vallecillo. Testing models and model transformations using classifying terms. Software and Systems Modeling, 2016. DOI: 10.1007/s10270-016-0568-3, Online 2016-12-09.
This paper proposes the use of equivalence partitioning techniques for testing models and model transformations. In particular, we introduce the concept of classifying terms, which are general OCL terms on a class model enriched with OCL constraints. Classifying terms permit defining equivalence classes, in particular for partitioning the source and target model spaces of the transformation, defining for each class a set of equivalent models with regard to the transformation. Using these classes, a model validator tool is able to automatically construct object models for each class, which constitute relevant test cases for the transformation. We show how this approach of guiding the construction of test cases in an orderly, systematic and efficient manner can be effectively used in combination with Tracts for testing both directional and bidirectional model transformations and for analyzing their behavior.
(27 pages, PDF: 2943kb via HTTP)


[Hilken et al., 2016b]
Frank Hilken, Philipp Niemann, Martin Gogolla, and Robert Wille. Towards a Catalog of Structural and Behavioral Verification Tasks for UML/OCL Models. In Andreas Oberweis and Ralf Reussner, editors, Proc. Modellierung (MODELLIERUNG'2016), pages 115-122. GI, LNI 254, 2016.
Verification tasks for UML and OCL models can be classified into structural and behavioral tasks. For both task categories a variety of partly automatic solving approaches exist. But up to now, different interpretations of central notions as, for example, `consistency' or `reachability' can be found in current approaches and tools. This paper is designed to clarify central verification notions and to establish a collection of typical verification tasks that are common to multiple approaches and tools. In addition, the verification tasks are categorized with the aim of creating a central catalog of tasks, providing a common understanding of the terms used in model verifications.
(8 pages, PDF: 225kb via HTTP)


[Hilken et al., 2016c]
Frank Hilken, Marcel Schuster, Karsten Sohr, and Martin Gogolla. Integrating UML/OCL Derived Properties into Validation and Verification Processes. In Achim D. Brucker, Jordi Cabot, and Adolfo Sanchez-Barbudo Herrera, editors, Proc. Workshop OCL and Textual Modelling (2016), pages 89-104. CEUR WS Proceedings 1756, 2016.
UML and OCL are rich languages offering a multitude of modeling elements. They provide modelers with simple and effective tools to express and visualize models, but their complex semantics are a great challenge for validation and verification processes, which are often limited by their underlying logic. On the basis of a network topology example model, describing lower physical and logical network levels, we demonstrate applications of derived attributes and associations that help checking network security aspects. This includes finding inconsistencies in an existing network, directing to potential configuration errors and property evaluation, e.g. reachability between components within the network. In addition, a transformation of derived properties into relational logic is presented to enable the use of a modern instance finder for further verification tasks and generation of valid networks configurations.
(16 pages, PDF: 524kb via HTTP)


[Niemann et al., 2016]
Philipp Niemann, Frank Hilken, Martin Gogolla, and Robert Wille. Extracting Frame Conditions from Operation Contracts. In Jens Knoop and Uwe Zdun, editors, Proc. Fachtagung Software Engineering (SE 2016), pages 89-90. LNI 252, 2016.
In behavioral modeling, operation contracts defined by pre- and postconditions describe the effects on model properties (i.e., model elements such as attributes, links, etc.) that are enforced by an operation. However, it is usually omitted which model properties should not be modified. Defining so-called frame conditions can fill this gap. But, thus far, these have to be defined manually - a time-consuming task. In this work, we propose a methodology which aims to support the modeler in the definition of the frame conditions by extracting suggestions based on an automatic analysis of operation contracts provided in OCL. More precisely, the proposed approach performs a structural analysis of pre- and postconditions together with invariants in order to categorize which class and object properties are clearly `variable' or `unaffected' - and which are `ambiguous', i.e. indeed require a more thorough inspection. The developed concepts are implemented as a prototype and evaluated by means of several example models known from the literature.
(2 pages, PDF: 40kb via HTTP)


[Przigoda et al., 2016]
Nils Przigoda, Frank Hilken, Judith Peters, Robert Wille, Martin Gogolla, and Rolf Drechsler. Integrating an SMT-Based ModelFinder into USE. In Michalis Famelis, Daniel Ratiu, and Gehan M. K. Selim, editors, Proc. Workshop Model-Driven Engineering, Verification and Validation (MoDeVVa 2016), pages 40-45. CEUR WS Proceedings 1713, 2016.
The validation and verification of models becomes increasingly important as the complexity and overall costs of later development stages increase. Although, a variety of tools exists for this purpose, the majority are academic - used as a proof of concept for the theory behind them. Thus, implementations are mostly applicable to subsets of model verification tasks only. In order to execute all necessary verification tasks, the model under verification has to be manually prepared for each tool - usually involving several modeling languages and techniques. The manual work requires expert knowledge and is a source for errors. Simplifying this process is a desired aspect and poses new challenges to tool developers. We demonstrate how a common framework can be used to provide access to multiple model checking techniques by integrating an SMT-based ModelFinder including a high level interface to its functionality. Afterwards, the benefits are discussed comparing the new technique with the existing tool coverage in the framework.
(6 pages, PDF: 157kb via HTTP)


[Sedlmeier and Gogolla, 2016]
Matthias Sedlmeier and Martin Gogolla. Towards Flexible Model Analysis and Constraint Development: A Small Demo Based on Large Real-Life Data. In Dimitris Kolovos, Davide di Ruscio, Nicholas Matragkas, Jesus Sanchez Cuadrado, Istvan Rath, and Massimo Tisi, editors, Proc. Workshop Scalable Model Driven Engineering (BigMDE 2016), pages 1-10. CEUR Proceedings 1652, 2016.
This contribution discusses the handling of a larger model on an abstract level employing the standardized modeling languages UML and OCL and an accompanying tool. We represent real-world data in form of a large object model and perform data analysis, verification, and validation tasks on the modeling level in order to obtain feedback about the original data. The tool allows to explore larger object diagrams interactively in a flexible way through a combination of visual and textual techniques. Furthermore, model invariants can be created in a versatile fashion by iteratively considering relevant object diagram fractions and evolving OCL expressions.
(10 pages, PDF: 509kb via HTTP)


[Chechik et al., 2015]
Marsha Chechik, Geri Georg, Martin Gogolla, Jean-Marc Jezequel, Bernhard Rumpe, and Martin Schindler. In Memory of Robert B. France, Co-Founder and Editor-in-Chief of SoSyM from 1999 to 2015. Software and Systems Modeling, 14(2):525-532, 2015.
The SoSyM team has been devastated to learn about the passing of Prof. Robert B. France, on the evening of Sunday, February 15th, 2015. His passing was painless, after a battle against cancer. He was 54 years old.
(8 pages, PDF: 1058kb via HTTP)


[Gogolla, 2015a]
Martin Gogolla. An Approach to Employ Modeling in a Traditional Computer Science Curriculum or: Why Posing Essentials of the Object Constraint Language without Objects and Constraints? In Tony Clark and Arnon Sturm, editors, Proc. 11th MODELS Educators' Symposium (EduSymp 2015), http://ceur-ws.org/, 2015. CEUR Proceedings.
This paper has two purposes: first, it discusses one approach that shows how modeling and in particular information systems modeling techniques are employed within a traditional computer science curriculum, and second, it explains and recapitulates essential concepts of a contemporary modeling language in a conventional style without stressing modern concepts. In the second part the paper focuses on the Object Constraint Language (OCL) without using objects and constraints. We use this as an example to explain how to summarize taught concepts in a good way. Experience on teaching modeling is constantly gained in three lectures on a basic, advanced, and specialized level, and roughly speaking, the three lectures introduce and concentrate on (1) syntax, (2) semantics, and (3) metamodeling of modeling techniques.
(6 pages, PDF: 196kb via HTTP)


[Gogolla, 2015b]
Martin Gogolla. Experimenting with Multi-Level Models in a Two-Level Modeling Tool. In Colin Atkinson, Georg Grossmann, Thomas Kühne, and Juan de Lara, editors, Proc. 2nd Int. Workshop on Multi-Level Modelling (MULTI'2015), pages 3-11, http://ceur-ws.org/Vol-1505/, 2015. CEUR Proceedings, Vol. 1505.
This paper discusses two ways to establish the connection between two levels in a multi-level model. The first approach uses normal associations and generalizations under the assumption that the multi levels are represented in one UML and OCL model. The second approach views a middle level model both as a type model and as an instance model and introduces operations to navigate between the type and instance level. The paper reports on some experiments that have been carried out.
(9 pages, PDF: 273kb via HTTP)


[Gogolla and Hilken, 2015]
Martin Gogolla and Frank Hilken. UML and OCL Transformation Model Analysis: Checking Invariant Independence. In Moussa Amrani, Eugene Syriani, and Manuel Wimmer, editors, Proc. 4th Int. Workshop on Verification of Model Transformation (VOLT'2015), http://ceur-ws.org/, 2015. CEUR Proceedings.
This paper proposes to analyze UML and OCL models using an approach on the basis of a solver for relational logic. In the approach, UML and OCL models describe system structures formally with UML class diagrams and OCL class invariants, and system behavior is determined by UML state charts and OCL pre- and postconditions for operations and transitions. Test cases in form of object diagrams are constructed and employed for property inspection. With the approach one can prove model properties like model constraint independence for the structural model part. Thus crucial model properties can be analyzed on the modeling level without the need for implementing the model. All feedback given to the developer is stated in terms of the used modeling language, UML and OCL.
(8 pages, PDF: 290kb via HTTP)


[Gogolla et al., 2015a]
Martin Gogolla, Lars Hamann, Frank Hilken, and Matthias Sedlmeier. Checking UML and OCL Model Consistency: An Experience Report on a Middle-Sized Case Study. In Jasmin Blanchette and Nikolai Kosmatov, editors, Proc. 9th Int. Conf. Tests and Proofs (TAP 2015), pages 129-136. Springer, LNCS 9154, 2015. LNCS paper (8 pages) and addendum (28 pages).
This contribution reports on a middle-sized case study in which the consistency of a UML and OCL class model is checked. The class model restrictions are expressed by UML multiplicity constraints and explicit, non-trivial OCL invariants. Our approach automatically constructs a valid system state that shows that the model can be instantiated and thus proves consistency, i.e., shows that the invariants together with the multiplicity constraints are not contradictory.
(36 pages, PDF: 241kb via HTTP)


[Gogolla et al., 2015b]
Martin Gogolla, Lars Hamann, Frank Hilken, and Matthias Sedlmeier. Modeling Behavior with Interaction Diagrams in a UML and OCL Tool. In Ella Roubtsova, Ashley McNeile, Ekkart Kindler, and Christian Gerth, editors, Behavior Modeling: Foundations and Applications, Int. Workshops BM-FA 2009-2014, pages 31-58. Springer, LNCS 6368, 2015.
This paper discusses system modeling with UML behavior diagrams. We consider statecharts and both kinds of interaction diagrams, i.e., sequence and communication diagrams. We present new implementation features in a UML and OCL modeling tool: (1) Sequence diagram lifelines are extended with states from statecharts, and (2) communication diagrams are introduced as an alternative to sequence diagrams. We assess the introduced features and propose selection mechanisms which should be available in both kinds of interaction diagrams. We emphasize the role that OCL can play for such selection mechanisms.
(28 pages, PDF: 407kb via HTTP)


[Gogolla et al., 2015c]
Martin Gogolla, Antonio Vallecillo, Loli Burgueno, and Frank Hilken. Employing Classifying Terms for Testing Model Transformations. In Jordi Cabot and Alexander Egyed, editors, Proc. 18th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2015), pages 312-321. ACM, 2015.
This contribution proposes a new technique for developing test cases for UML and OCL models. The technique is based on an approach that automatically constructs object models for class models enriched by OCL constraints. By guiding the construction process through so-called classifying terms, the built test cases in form of object models are classified into equivalence classes. A classifying term can be an arbitrary OCL term on the class model that calculates for an object model a characteristic value. From each equivalence class of object models with identical characteristic values one representative is chosen. The constructed test cases behave significantly different with regard to the selected classifying term. By building few diverse object models, properties of the UML and OCL model can be explored effectively. The technique is applied for automatically constructing relevant source model test cases for model transformations between a source and target metamodel.
(10 pages, PDF: 937kb via HTTP)


[Hamann and Gogolla, 2015]
Lars Hamann and Martin Gogolla. Endogene Metamodellierung der Semantik von neueren UML2 Sprachmitteln. In Uwe Aßmann, Birgit Demuth, Thorsten Spitta, Georg Püschel, and Ronny Kaiser, editors, Proc. Software Engineering (2015), pages 31-32. GI, LNI 239, 2015.
Seit dem Aufkommen der Unified Modeling Language (UML) wurden unterschiedliche Ansätze vorgestellt diese formal zu spezifizieren. Eine wohldefinierte formale Semantik der UML führt unter anderem zu einer höheren Interoperabilität zwischen verschiedenen Modellierungswerkzeugen, da Intepretationsspielräume verringert werden. Die hier zusammengefasste Arbeit beschreibt einen endogenen Ansatz zur Metamodellierung der Semantik von zentralen UML Elementen.
(2 pages, PDF: 62kb via HTTP)


[Hamann et al., 2015]
Lars Hamann, Martin Gogolla, and Karsten Sohr. Monitoring Database Access Constraints with an RBAC Metamodel: A Feasibility Study. In Frank Piessens, Juan Caballero, and Nataliia Bielova, editors, Proc. 7th Int. Conf. Engineering Secure Software and Systems (ESSOS 2015), pages 211-226. Springer, LNCS 8978, 2015.
Role-based access control (RBAC) is widely used in organizations for access management. While basic RBAC concepts are present in modern systems, such as operating systems or database management systems, more advanced concepts like history-based separation of duty are not. In this work, we present an approach that validates advanced organizational RBAC policies using a model-based approach against the technical realization applied within a database. This allows a security officer to examine the correct implementation possibly across multiple applications of more powerful policies on the database level. We achieve this by monitoring the current state of a database in a UML/OCL validation tool. We assess the applicability of the approach by a non-trivial feasibility study.
(16 pages, PDF: 427kb via HTTP)


[Hilken et al., 2015a]
Frank Hilken, Loli Burgueno, Martin Gogolla, and Antonio Vallecillo. Iterative Development of Transformation Models by Using Classifying Terms. In Juergen Dingel, Sahar Kokaly, Levi Lecio, Rick Salay, and Hans Vangheluwe, editors, Proc. Int. Workshop on Analysis of Model Transformations (AMT'2015), pages 1-6, http://ceur-ws.org/Vol-1500/, 2015. CEUR Proceedings, Vol. 1500.
In this paper we propose an iterative process for the correct specification of model transformations, i.e., for developing correct transformation models. This permits checking the correctness of a model transformation specification before any implementation is available. The proposal is based on the use of classifying terms for partitioning the input space and for simplifying the testing process.
(6 pages, PDF: 172kb via HTTP)


[Hilken et al., 2015b]
Frank Hilken, Philipp Niemann, Martin Gogolla, and Robert Wille. From UML/OCL to Base Models: Transformation Concepts for Generic Validation and Verification. In Dimitris Kolovos and Manuel Wimmer, editors, Proc. 8th Int. Conf. Model Transformation (ICMT 2015), pages 1-17. Springer, LNCS 9152, 2015.
Modeling languages such as UML and OCL find more and more application in the early stages of today's system design. Validation and verification, i.e. checking the correctness of the respective models, gains interest. Since these languages offer various description means and a huge set of constructs, existing approaches for this purpose only support a restricted subset of constructs and often focus on dedicated description means as well as verification tasks. To overcome this, we follow the idea of using model transformations to unify different description means to a base model. In the course of these transformation, complex language constructs are expressed by means of a small subset of so-called core elements in order to interface with a wide range of verification engines with complementary strengths and weaknesses. In this paper, we provide a detailed introduction of the proposed base model and its core elements as well as corresponding model transformations.
(16 pages, PDF: 505kb via HTTP)


[Niemann et al., 2015a]
Philipp Niemann, Frank Hilken, Martin Gogolla, and Robert Wille. Assisted Generation of Frame Conditions for Formal Models. In Wolfgang Nebel and David Atienza, editors, Proc. Design, Automation and Test in Europe (DATE'2015), pages 309-312. ACM, 2015.
Modeling languages such as UML or SysML allow for the validation and verification of the structure and the behavior of designs even in the absence of a specific implementation. However, formal models inherit a severe drawback: Most of them hardly provide a comprehensive and determinate description of transitions from one system state to another. This problem can be addressed by additionally specifying so-called frame conditions. However, only naive workarounds based on trivial heuristics or completely relying on a manual creation have been proposed for their generation thus far. In this work, we aim for a solution which neither leaves the burden of generating frame conditions entirely on the designer (avoiding the introduction of another time-consuming and expensive design step) nor is completely automatic (which, due to ambiguities, is not possible anyway). For this purpose, a systematic design methodology for the assisted generation of frame conditions is proposed.
(4 pages, PDF: 138kb via HTTP)


[Niemann et al., 2015b]
Philipp Niemann, Frank Hilken, Martin Gogolla, and Robert Wille. Extracting Frame Conditions from Operation Contracts. In Jordi Cabot and Alexander Egyed, editors, Proc. 18th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2015), pages 266-275. ACM, 2015.
In behavioral modeling, operation contracts defined by pre- and postconditions describe the effects on model properties (i.e., model elements such as attributes, links, etc.) that are enforced by an operation. However, it is usually omitted which model properties should not be modified. Defining so-called frame conditions can fill this gap. But, thus far, these have to be defined manually - a time-consuming task. In this work, we propose a methodology which aims to support the modeler in the definition of the frame conditions by extracting suggestions based on an automatic analysis of operation contracts provided in OCL. More precisely, the proposed approach performs a structural analysis of pre- and postconditions together with invariants in order to categorize which class and object properties are clearly `variable' or `unaffected' - and which are `ambiguous', i.e. indeed require a more thorough inspection. The developed concepts are implemented as a prototype and evaluated by means of several example models known from the literature.
(10 pages, PDF: 277kb via HTTP)


[Sedlmeier and Gogolla, 2015]
Matthias Sedlmeier and Martin Gogolla. Model Driven ActiveRecord with yEd. In Tatjana Welzer, Hannu Jaakkola, Bernhard Thalheim, Yasushi Kiyoki, and Naofumi Yoshida, editors, Proc. Int. 25th Int. Conf. Information Modelling and Knowledge Bases (EJC'2015), pages 65-76. IOS Press, Amsterdam, 2015.
Since its release in 2004, Ruby on Rails has evolved into a widely used full stack model-view-controller (MVC) framework. But despite the fact, that Rails (short for Ruby on Rails) is also used for developing enterprise-scale applications like Github or scientific tools like QTREDS, there is no official support for graphical modelling. This paper introduces a proposal to fill this gap by suggesting a model driven approach using the free yEd diagram editor as well as a specifically developed transformation tool and ER dialect. The implementation is based on the Rails data abstraction layer ActiveRecord and its provided domain specific languages.
(36 pages, PDF: 565kb via HTTP)


[Amrani et al., 2014]
Moussa Amrani, Eugene Syriani, Manuel Wimmer, Robert Bill, Martin Gogolla, Frank Hermann, and Kevin Lano. Report on the Third Workshop on Verification of Model Transformations. In Moussa Amrani, Eugene Syriani, and Manuel Wimmer, editors, Proc. 3rd Int. Workshop on Verification of Model Transformation (VOLT'2014), pages 1-9, http://ceur-ws.org/, 2014. CEUR Proceedings, Vol. 1325.
This report is a summary of the Third International Workshop on the Verification Of modeL Transformation (VOLT 2014) held at the STAF 2014 conference. The workshop brought together researchers from model-driven engineering, in particular from model transformation language engineering and modelbased verification. The major aims of VOLT 2014 were to identify motivations, problems, and requirements for model transformation verification as well as to present different proposals supporting different kinds of model transformations and verification techniques.
(7 pages, PDF: 142kb via HTTP)


[Brucker et al., 2014a]
Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, and Burkhart Wolff. Panel Discussion: Proposals for Improving OCL. In Achim D. Brucker, Carolina Dania, Geri Georg, and Martin Gogolla, editors, Proc. Int. Workshop on OCL (OCLWS'2014), pages 83-99, http://ceur-ws.org/Vol-1285/, 2014. CEUR Proceedings, Vol. 1285.
During the panel session at the OCL workshop, the OCL community discussed, stimulated by short presentations by OCL experts, potential future extensions and improvements of the OCL. As such, this panel discussion continued the discussion that started at the OCL meeting in Aachen in 2013 and on which we reported in the proceedings of the last year's OCL workshop. This collaborative paper, to which each OCL expert contributed one section, summarises the panel discussion as well as describes the suggestions for further improvements in more detail.
(17 pages, PDF: 380kb via HTTP)


[Brucker et al., 2014b]
Achim D. Brucker, Carolina Dania, Geri Georg, and Martin Gogolla, editors. Proc. MODELS'2014 OCL Workshop, http://ceur-ws.org/Vol-1285/, 2014. CEUR Workshop Proceedings, Vol. 1285. Satellite Events at the MODELS'2014 Conference.
The proceedings contain the accepted contributions for the OCL Workshop at the MODELS'2014 conference.

[Büttner and Gogolla, 2014]
Fabian Büttner and Martin Gogolla. On OCL-Based Imperative Languages. Science of Computer Programming, 92:162-178, 2014.
The Object Constraint Language (OCL) is a well-accepted ingredient in model-driven engineering and accompanying modeling languages such as UML (Unified Modeling Language) and EMF (Eclipse Modeling Framework) that support object-oriented software development. Among various possibilities, OCL offers the formulation of class invariants and operation contracts in form of pre- and postconditions, and side-effect free query operations. Much research has been done on OCL and various mature implementations are available for it. OCL is also used as the foundation for several modeling-specific programming and transformation languages. However, an intrusive way of embedding OCL into these language hampers us when we want to benefit from the existing achievements for OCL. In response to this shortcoming, we propose the language SOIL (Simple OCL-like Imperative Language), which we implemented in the UML and OCL modeling tool USE to amend its declarative model validation features. The expression sub-language of SOIL is identical to OCL. SOIL adds imperative constructs for programming in the domain of models. Thus by employing OCL and SOIL, it is possible to describe any operation in a declarative way and in an operational way on the modeling level without going into the details of a conventional programming language. In contrast to other similar approaches, the embedding of OCL into SOIL is done in a careful, non-intrusive way so that purity of OCL is preserved.
(22 pages, PDF: 451kb via HTTP)


[Büttner et al., 2014]
Fabian Büttner, Ullrich Bartels, Lars Hamann, Oliver Hofrichter, Mirco Kuhlmann, Martin Gogolla, Lutz Rabe, Frank Steimke, Yorck Rabenstein, and Alina Stosiek. Model-Driven Standardization of Public Authority Data Interchange. Science of Computer Programming, 89:162-175, 2014.
In the past decade, several electronic data exchange processes between public authorities have been established by the German public administration. In the context of various locally operating systems and numerous suppliers of software for public authorities, it is crucial that these interfaces are open and precisely and uniformly defined, in order to foster free competition and interoperability. A community of such projects and specifications for various public administration domains has arisen from an early adopter project in the domain of data interchange between the 5,400 German municipal citizen registers. A central coordination office provides a framework for these projects that is put into operation by a unified model-driven method, supported by tools and components, involving UML profiles, model validation, and model-to-text transformations into several technical domains. We report how this model-driven approach has already proven to be effective in a number of projects, and how it could contribute to the development of standardized e-government specifications in various ways.
(17 pages, PDF: 381kb via HTTP)


[Cheng et al., 2014]
Betty H.C. Cheng, Kerstin I. Eder, Martin Gogolla, Lars Grunske, Marin Litoiu, Hausi A. Müller, Patrizio Pelliccione, Anna Perini, Nauman A. Qureshi, Bernhard Rumpe, Daniel Schneider, Frank Trollmann, and Norha M. Villegas. Using Models at Runtime to Address Assurance for Self-Adaptive Systems. In Nelly Bencomo, Robert B. France, Betty H. C. Cheng, and Uwe Aßmann, editors, Models@run.time - Foundations, Applications, and Roadmaps, pages 101-136. Springer, Berlin, LNCS 8378, 2014.
Self-adaptive software systems modify their behaviour at runtime in response to changes in the system or its environment. The fulfilment of the system requirements and reachability of the system goals needs to be guaranteed even in the presence of adaptations. Thus, a key challenge for self-adaptive software systems is assurance. Traditionally, confidence in the correctness of a system is gained during system development. Evidence to support assurance is collected based on a variety of activities and processes performed at development time. In the presence of self-adaptation, however, some of the assurance tasks need to be performed at runtime. This calls for continuous assurance throughout the software life cycle. One of the most promising avenues of research in this area is to use models at runtime as a foundation for developing runtime assurance techniques. This chapter focuses on investigating the use of models at runtime for assurance of self-adaptive software systems. It defines what we understand by a model at runtime, specifically for the purpose of assurance, and puts this definition into the context of existing work. We then outline selected research challenges. The chapter concludes with an exploration of selected application areas where models at runtime could contribute a considerable value proposition compared to existing techniques.
(36 pages, PDF: 750kb via HTTP)


[Gogolla et al., 2014a]
Martin Gogolla, Lars Hamann, and Frank Hilken. Checking Transformation Model Properties with a UML and OCL Model Validator. In Moussa Amrani, Eugene Syriani, and Manuel Wimmer, editors, Proc. 3rd Int. Workshop on Verification of Model Transformation (VOLT'2014), pages 16-25, http://ceur-ws.org/, 2014. CEUR Proceedings, Vol. 1325.
This paper studies model transformations in the form of transformation models connecting source and target metamodels. We propose to analyse transformation models with a UML and OCL tool on the basis of an implementation of relational logic on top of Kodkod. Within this approach it is feasible to check for transformation model consistency in different flavors. Certain properties implied by the transformation model, e.g. whether a particular property is preserved by the transformation, can be inspected as well.
(25 pages, PDF: 362kb via HTTP)


[Gogolla et al., 2014b]
Martin Gogolla, Lars Hamann, and Frank Hilken. On Static and Dynamic Analysis of UML and OCL Transformation Models. In Jürgen Dingel, Juan de Lara, Levi Lucio, and Hans Vangheluwe, editors, Proc. Int. Workshop on Analysis of Model Transformations (AMT'2014), pages 24-33, http://ceur-ws.org/Vol-1277/, 2014. CEUR Proceedings, Vol. 1277.
This contribution discusses model transformations in the form of transformation models that connect a source and a target metamodel. The transformation model is statically analyzed within a UML and OCL tool by giving each constraint an individual representation in the underlying class diagram by highlighting the employed model elements. We also discuss how to analyze transformation models dynamically on the basis of a model validator translating UML and OCL into relational logic. One can specify, for example, the transformation source and let the tool compute automatically the transformation target on the basis of the transformation model without the need for implementing the transformation. Properties like injectivity of the transformation can be checked through the construction of example transformation pairs. The paper uses the well-known transformation between Entity-Relationship schemata and relational database schemata for illustrating the underlying ideas.
(10 pages, PDF: 243kb via HTTP)


[Gogolla et al., 2014c]
Martin Gogolla, Lars Hamann, Frank Hilken, Mirco Kuhlmann, and Robert B. France. From Application Models to Filmstrip Models: An Approach to Automatic Validation of Model Dynamics. In Hans-Georg Fill, Dimitris Karagiannis, and Ulrich Reimer, editors, Proc. Modellierung (MODELLIERUNG'2014), pages 273-288. GI, LNI 225, 2014.
Efficient model validation and verification techniques are strong in the analysis of systems describing static structures, for example, UML class diagrams and OCL invariants. However, general UML and OCL models can involve dynamic aspects in form of OCL pre- and postconditions for operations. This paper describes the automatic transformation of a UML and OCL model with invariants and pre- and postconditions into an equivalent model with only invariants. We call the first model (with pre- and postconditions) the application model and the second model (with invariants only) the filmstrip model, because a sequence of system states in the application model becomes a single system state in the filmstrip model. This single system state can be thought of as being a filmstrip presenting snapshots from the application model with different logical time stamps. Pre- and postconditions from the application model become invariants in the filmstrip model. Providing a proper context, the text of the pre- and postconditions can be used in the filmstrip model nearly unchanged. The filmstrip model can be employed for automatically constructing dynamic test scenarios and for checking temporal properties.
(16 pages, PDF: 393kb via HTTP)


[Gogolla et al., 2014d]
Martin Gogolla, Lars Hamann, Frank Hilken, Matthias Sedlmeier, and Quang Dung Nguyen. Behavior Modeling with Interaction Diagrams in a UML and OCL Tool. In Ella Roubtsova, Christian Gerth, Ekkart Kindler, and Ashley McNeile, editors, Proc. 6th Workshop Behaviour Modelling - Foundations and Applications (BMFA'2014). ACM Digital Library, Vol. 2630768, 2014.
This contribution discusses system modeling with UML behavior diagrams. We consider statecharts and both kinds of interaction diagrams, i.e., sequence and communication diagrams. We present new implementation features in a UML and OCL modeling tool: (1) Sequence diagram lifelines are extended with states from statecharts, and (2) communication diagrams are introduced as an alternative to sequence diagrams. We assess the introduced features and propose a systematic set of features which should be available in both kinds of interaction diagrams. We emphasize the role that OCL can play for such a feature set.
(12 pages, PDF: 284kb via HTTP)


[Gogolla et al., 2014e]
Martin Gogolla, Matthias Sedlmeier, Lars Hamann, and Frank Hilken. On Metamodel Superstructures Employing UML Generalization Features. In Colin Atkinson, Georg Grossmann, Thomas Kühne, and Juan de Lara, editors, Proc. Int. Workshop on Multi-Level Modelling (MULTI'2014), pages 13-22, http://ceur-ws.org/Vol-1286/, 2014. CEUR Proceedings, Vol. 1286.
We employ UML generalization features in order to describe multi-level metamodels and their connections. The basic idea is to represent several metamodel levels in one UML and OCL model and to connect the metamodels with (what we call) a superstructure. The advantage of having various levels in one model lies in the uniform handling of all levels and in the availability of OCL for constraining models and navigating between them. We establish the connection between the metamodel levels by typing links that represent the instance-of relationship. These typing links are derived from associations that are defined on an abstraction of the metamodel classes and that are restricted by redefines and union constraints in order to achieve level-conformant typing. The abstraction of the metamodel classes together with the connecting associations and generalizations constitutes the superstructure.
(10 pages, PDF: 312kb via HTTP)


[Hamann et al., 2014a]
Lars Hamann, Martin Gogolla, and Oliver Hofrichter. Zur Integration von Struktur- und Verhaltensmodellierung mit OCL. In Wilhelm Hasselbring and Nils Christian Ehmke, editors, Proc. Software Engineering (2014), pages 75-76. GI, LNI 227, 2014.
Dieser Beitrag beschreibt ein werkzeuggestütztes Vorgehen zum Validieren von in der Unified Modeling Language (UML) spezifizierten Modellen. Herkömmliche Werkzeuge in diesem Kontext verwenden UML-Klassendiagramme in Verbindung mit textuellen Einschränkungen, die in der Object Constraint Language (OCL) definiert sind. Eher unbeachtet sind weitergehende Modellierungselemente wie zum Beispiel Zustandsautomaten, die zwar von der UML bereitgestellt werden, aber in OCL-basierten Validierungswerkzeugen bisher kaum Einzug gefunden haben. Der vorliegende Beitrag zeigt, basierend auf einem etablierten UML/OCL-Werkzeug, das international in der Praxis sowie zu Forschungsprojekten und in der Lehre eingesetzt wird, wie die in der UML vorhandenen Protokolzustandsautomaten (Protocol State Machines; PSMs) die Modellierungsmöglichkeiten erweitern.
(2 pages, PDF: 57kb via HTTP)


[Hamann et al., 2014b]
Lars Hamann, Frank Hilken, and Martin Gogolla. Collected Experience and Thoughts on Long Term Development of an Open Source MDE Tool. In Francis Bordelau, Jürgen Dingel, Sebastien Gerard, and Sebastian Voss, editors, Proc. Int. Workshop on Open Source Software for Model Driven Engineering (OSS4MDE'2014), pages 42-52, http://ceur-ws.org/Vol-1290/, 2014. CEUR Proceedings, Vol. 1290.
During 14 years of developing an open source model driven engineering tool at a university we collected some dos and don'ts for such projects, which we are going to describe in this paper. For example, the mentoring of students and afterwards the integration of their results need special treatments, to be able to keep a product of high quality. Beside such quality related issues, we also report on our experience with industrial cooperations. To get an idea about the amount of work that has been put into our tool, we review and visualize its history.
(10 pages, PDF: 1720kb via HTTP)


[Hilken et al., 2014a]
Frank Hilken, Lars Hamann, and Martin Gogolla. Transformation of UML and OCL Models into Filmstrip Models. In Davide Di Ruscio and Dániel Varró, editors, Proc. 7th Int. Conf. Model Transformation (ICMT 2014), pages 170-185. Springer, LNCS 8568, 2014.
This contribution presents an automatic transformation from UML and OCL models into enriched UML and OCL models, so-called filmstrip models, that embody more information when employing OCL while maintaining the same functionality as the original model. The approach uses a combination of object and sequence diagrams that allows for a wide range of possible OCL constraints about sequences of operation calls and their temporal properties. The modeler does not need to account for such properties while creating the original model. Errors found by constraints for the filmstrip model can easily be related back to the original model, as the elements of the filmstrip model are synchronized with the original model and the backwards calculation is generally simple. The approach is implemented in a UML and OCL modeling tool.
(16 pages, PDF: 438kb via HTTP)


[Hilken et al., 2014b]
Frank Hilken, Philipp Niemann, Martin Gogolla, and Robert Wille. Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models. In Martina Seidl and Nikolai Tillmann, editors, Proc. 8th Int. Conf. Tests and Proofs (TAP 2014), pages 99-116. Springer, LNCS 8570, 2014.
Guaranteeing the essential properties of a system early in the design process is an important as well as challenging task. Modeling languages such as the UML allow for a formal description of structure and behavior by employing OCL class invariants and operation pre- and postconditions. This enables the verification of a system specification prior to implementation. For this purpose, first approaches have recently been put forward. In particular solutions relying on the deductive power of constraint solvers are promising. Here, complementary approaches of how to formulate and transform respective UML and OCL verification tasks into corresponding solver tasks have been proposed. We consider two verification approaches for UML and OCL behavioral models and compare their methods and the workflows with each other. By this, a better understanding of the advantages and disadvantages of these verification methods is achieved.
(18 pages, PDF: 352kb via HTTP)


[Hilken et al., 2014c]
Frank Hilken, Philipp Niemann, Robert Wille, and Martin Gogolla. Towards a Base Model for UML and OCL Verification. In Frédéric Boulanger, Michalis Famelis, and Daniel Ratiu, editors, Proc. 11th Int. Workshop on Model Driven Engineering, Verification and Validation Workshop (MODEVVA'2014), pages 59-68, http://ceur-ws.org/Vol-1235/, 2014. CEUR Proceedings, Vol. 1235.
Modelling languages such as UML and OCL are more and more used in early stages of system design. These languages offer a huge set of constructs. As a consequence, existing verification engines only support a restricted subset of them. In this work, we propose an approach using model transformations to unify different description means within a so called base model. In the course of this transformation, complex language constructs are expressed with a small subset of so-called core elements. This simplification enables to interface with a wide range of verification engines with complementary strengths and weaknesses. Our aim is that, guided by a structural analysis of the base model, the developer can choose the most promising verification engine.
(10 pages, PDF: 283kb via HTTP)


[Sedlmeier and Gogolla, 2014]
Matthias Sedlmeier and Martin Gogolla. Design and Prototypical Implementation of an Integrated Graph-Based Conceptual Data Model. In Bernhard Thalheim, Hannu Jaakkola, Yasushi Kiyoki, and Naofumi Yoshida, editors, Proc. Int. 24th Int. Conf. Information Modelling and Knowledge Bases (EJC'2014), pages 376-395. IOS Press, Amsterdam, 2014.
The paper introduces a new, comprehensive integrated conceptual data model in a precise way. Central language features cover core modeling concepts as classification, membership, inheritance, interfaces, structured types, aliasing, aggregation, composition, constraints, clustering and relationships. Schema states are thought of as being realized as graphs with appropriate navigation options. A prototypical graph database implementation and accompanying examples are discussed.
(20 pages, PDF: 1195kb via HTTP)


[Brucker et al., 2013]
Achim D. Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D. Willink, and Burkhart Wolff. Report on the Aachen OCL Meeting. In Jordi Cabot, Martin Gogolla, István Ráth, and Edward D. Willink, editors, Proc. Int. Workshop on OCL (OCLWS'2013), pages 103-111, http://ceur-ws.org/Vol-1092/, 2013. CEUR Proceedings, Vol. 1092.
As a continuation of the OCL workshop during the MODELS 2013 conference in October 2013, a number of OCL experts decided to meet in November 2013 in Aachen for two days to discuss possible short term improvements of OCL for an upcoming OMG meeting and to envision possible future long-term developments of the language. This paper is a sort of ``minutes of the meeting'' and intended to quickly inform the OCL community about the discussion topics.
(9 pages, PDF: 534kb via HTTP)


[Cabot et al., 2013]
Jordi Cabot, Martin Gogolla, István Ráth, and Edward D. Willink, editors. Proc. MODELS'2013 OCL Workshop, http://ceur-ws.org/Vol-1092/, 2013. CEUR Workshop Proceedings, Vol. 1092. Satellite Events at the MODELS'2013 Conference.
The proceedings contain the accepted contributions for the OCL Workshop at the MODELS'2013 conference.

[Clark et al., 2013]
Tony Clark, Robert B. France, Martin Gogolla, and Bran Selic. Meta-Modeling Model-Based Engineering Tools (Dagstuhl Seminar 13182). Dagstuhl Reports, 3(4):188-226, 2013.
Model-based engineering (MBE) is a software development approach in which abstraction via modeling is used as the primary mechanism for managing the complexity of software-based systems. An effective approach to software development must be supported by effective technologies (i.e., languages, methods, processes, tools). The wide range of development tasks that effective MBE approaches must support leads to two possible tooling scenarios. In the first scenario a federated collection of tools is used to support system development. Each tool in the collection provides specialized services. Tool interoperability and consistency of information across the tools are major concerns in this scenario. These concerns are typically addressed using transformations and exposed tool interfaces. Defining and evolving the transformations and interfaces requires detailed low-level knowledge of the tools and thus leads to complex tooling environments that are difficult to configure, learn, use, and evolve. In the second scenario, a single tool is used to support the complete modeling lifecycle. This avoids the inter-tool transformation and consistency problems, but the resulting multi-featured tool is a monolithic entity that is costly to develop and evolve. Furthermore, the large number of non-trivial features can make learning and using such tools difficult. Successful uptake of MDE in industry requires supporting tools to be, at least, useful and usable. From a tool developer's perspective, there is also a need to significantly reduce the cost and effort required to develop and evolve complex MBE tools. This seminar brings together experts in the areas of MBE, meta-modeling, tool development, and human-computer interactions to map out a research agenda that lays a foundation for the development of effective MBE tools. Such a foundation will need to support not only interoperability of tools or tool features, but also the implementation of high quality MBE tools. The long-term objective is to foster a research community that will work on a foundation that can be expressed in the form of standard tool (meta-)models that capture and leverage high quality reusable MBE tool development experience.
(40 pages, PDF: 1336kb via HTTP)


[Dubois et al., 2013]
Catherine Dubois, Michalis Famelis, Martin Gogolla, Leonel Nobrega, Ileana Ober, Martina Seidl, and Markus Völter. Research Questions for Validation and Verification in the Context of Model-Based Engineering. In Frederic Boulanger, Michalis Famelis, and Daniel Ratiu, editors, Proc. 10th Int. Workshop on Model Driven Engineering, Verification and Validation (MODEVVA'2013), pages 67-76, http://ceur-ws.org/Vol-1069/, 2013. CEUR Proceedings, Vol. 1069.
In model-based engineering (MBE), the abstraction power of models is used to deal with the ever increasing complexity of modern software systems. As models play a central role in MBE-based development processes, for the adoption of MBE in practical projects it becomes indispensable to introduce rigorous methods for ensuring the correctness of the models. Consequently, much effort has been spent on developing and applying validation and verification (V&V) techniques for models. However, there are still many open challenges. In this paper, we shortly review the status quo of V&V techniques in MBE and derive a catalogue of open questions whose answers would contribute to successfully putting MBE into practice.
(10 pages, PDF: 241kb via HTTP)


[Gogolla, 2013a]
Martin Gogolla. Employing the Object Constraint Language in Model-Based Engineering. In Pieter Van Gorp, Tom Ritter, and Louise Rose, editors, Proc. 9th European Conf. Modelling Foundations and Applications (ECMFA 2013), pages 1-2. Springer, Berlin, LNCS 7949, 2013. Invited talk.
MBE (Model-Based Engineering) proposes to develop software by taking advantage of models, in contrast to traditional code-centric development approaches. If models play a central role in development, model properties must be formulated and checked early on the modeling level, not late on the implementation level. We discuss how to validate and verify model properties in the context of modeling languages like the UML (Unified Modeling Language) combined with textual restrictions formulated in the OCL (Object Constraint Language).
(2 pages, PDF: 39kb via HTTP)


[Gogolla, 2013b]
Martin Gogolla, editor. Proc. MODELS'2013 Doctoral Symposium, http://ceur-ws.org/Vol-1071/, 2013. CEUR Workshop Proceedings, Vol. 1071. Satellite Events at the MODELS'2013 Conference.
The proceedings contain the accepted contributions for the Doctoral Symposium at the MODELS'2013 conference.

[Gogolla et al., 2013]
Martin Gogolla, Fabian Büttner, and Jordi Cabot. Initiating a Benchmark for UML and OCL Analysis Tools. In Margus Veanes and Luca Vigano, editors, Proc. 7th Int. Conf. Tests and Proofs (TAP 2013), pages 115-132. Springer, Berlin, LNCS 7942, 2013. PDF contains LNCS conference paper (18 pp) plus additional material (30 pp).
The Object Constraint Language (OCL) is becoming more and more popular for model-based engineering, in particular for the development of models and model transformations. OCL is supported by a variety of analysis tools having different scopes, aims and technological corner stones. The spectrum ranges from treating issues concerning formal proof techniques to testing approaches, from validation to verification, and from logic programming and rewriting to SAT-based technologies. This paper is a first step towards a well-founded benchmark for assessing validation and verification techniques on UML and OCL models. The paper puts forward a set of UML and OCL models together with particular questions for these models roughly characterized by the notions consistency, independence, consequences, and reachability. The paper sketches how these questions are handled by two OCL tools, USE and EMFtoCSP. The claim of the paper is not to present a complete benchmark right now. The paper is intended to initiate the development of further UML and OCL models and accompanying questions within the UML and OCL community. The OCL community is invited to check the presented UML and OCL models with their approaches and tools and to contribute further models and questions which emphasize the possibilities offered by their own tools.
(48 pages, PDF: 818kb via HTTP)


[Hamann and Gogolla, 2013]
Lars Hamann and Martin Gogolla. Endogenous Metamodeling Semantics for Structural UML2 Concepts. In Ana Moreira, Bernhard Schätz, Jeff Gray, Antonio Vallecillo, and Peter J. Clarke, editors, Proc. 16th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2013), pages 488-504. Springer, Berlin, LNCS 8107, 2013.
A lot of work has been done in order to put the Unified Modeling Language (UML) on a formal basis by translating concepts into various formal languages, e.g., set theory or graph transformation. While the abstract UML syntax is defined by using an endogenous approach, i. e., UML describes its abstract syntax using UML, this approach is rarely used for its semantics. This paper shows how to apply an endogenous approach called metamodeling semantics for central parts of the UML standard. To this end, we enrich existing UML language elements with constraints specified in the Object Constraint Language (OCL) in order to describe a semantic domain model. The UML specification explicitly states that complete runtime semantics is not included in the standard because it would be a major amount of work. However, we believe that certain central concepts, like the ones used in the UML standard and in particular property features as subsets, union and derived, need to be explicitly modeled to enforce a common understanding. Using such an endogenous approach enables the validation and verification of the UML standard by using off-the-shelf UML and OCL tools.
(17 pages, PDF: 587kb via HTTP)


[Hofrichter et al., 2013]
Oliver Hofrichter, Martin Gogolla, and Karsten Sohr. UML/OCL based Design and Analysis of Role-Based Access Control Policies. In Balbir Barn, Tony Clark, Robert France, Ulrich Frank, Vinay Kulkarni, and Dan Turk, editors, Proc. Int. Workshop Towards the Model Driven Organization (AMINO 2013), pages 33-42, http://ceur-ws.org/Vol-1102/, 2013. CEUR Proceedings, Vol. 1102.
Access control plays an important part in IT systems these days. Specifically Role-Based Access Control (RBAC) has been widely adopted in practice. One of the major challenges within the introduction of RBAC into an organization is the policy definition. Modeling technologies provide support by allowing to design and to validate a policy. In this work we apply a UML and OCL based domain-specific language (DSL) to design and to analyze the access control of the conference management system EasyChair. For the first time EasyChair is formally described in connection with RBAC. Our activities are located on three levels:(a) the re-engineering of the system's access control policy is located at the policy level, (b) the framework level summarizes activities concerning the RBAC metamodel (e.g. enhancements), and (c) at the configuration level, we configure a concrete policy using the conference management system options. As a result, both a DSL developed in previous work is checked for the need of enhancements, and the re-enginered EasyChair access control policy is analyzed. For validation purposes a frequently used UML/OCL validation tool is utilized.
(10 pages, PDF: 328kb via HTTP)


[Kuhlmann et al., 2013]
Mirco Kuhlmann, Karsten Sohr, and Martin Gogolla. Employing UML and OCL for Designing and Analyzing Role-Based Access Control. Mathematical Structures in Computer Science, 23(4):796-833, 2013.
Stringent security requirements of organizations like banks or hospitals frequently adopt role-based access control (RBAC) principles to represent and simplify their internal permission management. While representing a fundamental advanced RBAC concept enabling precise restrictions on access rights, authorization constraints increase the complexity of the resulting security policies so that tool support for comfortable creation and adequate validation is required. One contribution of our work is a new approach to developing and analyzing RBAC policies using a UML-based domain-specic language (DSL) for modeling RBAC concepts which allows hiding the mathematical structures of the underlying authorization constraints implemented in OCL. The presented DSL is highly configurable and extendable with respect to new concepts and classes of authorization constraints, and allows the developer to validate RBAC policies in an effective way. The handling of dynamic (i.e., time-dependent) constraints, their visual representation through the RBAC DSL, and their analysis form another part of our contribution. The approach is supported by a UML and OCL validation tool.
(36 pages, PDF: 776kb via HTTP)


[Mustafa, 2013]
Tanveer Mustafa. Static Security Analysis of Java Applications with an Approach Based on Design by Contract. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2013.
In recent years, Design by Contract (DBC) and related tool support have shown promise, which has some practical impact to statically analyze applications with respect to security. Specifically, the Java Modeling Language (JML), which is close to Java's syntax, can be adopted by the software developers to formulate and verify security requirements against applications. In this thesis, we discuss whether DBC and related tool support can bring advantage towards statically analyzing the real-world security-critical applications. We applied the DBC approach to a role-based authorization API. Based on our experience, and a further learning curve to understand the working of static checking in general, we came up with an extended DBC-based analysis approach for security. Here, we combined static checking with program slicing, which is a software abstraction technique. In particular, we learned that DBC is well suited for checking the correct usage of Security APIs by their respective applications. We have successfully applied this extended approach to two real-world security case studies. In the first case study, we analyzed the access control policy of Android system services which provide security-critical functionality. In the second case study, we outlined how our approach can be used in the context of the Java Enterprise Edition (JEE). Last but not the least, we argue that since many Security APIs such as OWASP Enterprise Security API (ESAPI), Java Trusted Software Stack to access security hardware (jTSS) and Java Secure Socket Extension (JSSE) are usually complex, they are often incorrectly used or interpreted by the application developers. Therefore, in this context, our approach can be seen as a general method for checking whether applications use Security APIs in a way such that the security requirements of the application are fulfilled.

[Wille et al., 2013]
Robert Wille, Martin Gogolla, Mathias Soeken, Mirco Kuhlmann, and Rolf Drechsler. Towards a Generic Verification Methodology for System Models. In Proc. Design, Automation and Test in Europe (DATE'2013), pages 1193-1196. European Design and Automation Association (EDAA), 2013.
The use of modeling languages such as UML or SysML enables to formally specify and verify the behavior of digital systems already in the absence of a specific implementation. However, for each modeling method and verification task usually a separate verification solution has to be applied today. In this paper, a methodology is envisioned that aims at stopping this ``inflation'' of different verification approaches and instead employs a generic methodology. For this purpose, a given specification as well as the verification shall be transformed into a basic model which itself is specified by means of a generic modeling language. Then, a range of automatic reasoning engines shall uniformly be applied to perform the actual verification. A feasibility study demonstrates the applicability of the envisioned approach.
(4 pages, PDF: 148kb via HTTP)


[Balaban et al., 2012]
Mira Balaban, Jordi Cabot, Martin Gogolla, and Claas Wilke. Workshop on OCL and Textual Modeling: OCL 2012. In Mira Balaban, Jordi Cabot, Martin Gogolla, and Claas Wilke, editors, Proc. 12th Int. Workshop Object Constraint Language (OCL 2012), pages 5-6. ACM Digital Library, 2012.
At the MoDELS 2012 conference, the ``OCL and Textual Modeling'' workshop is a forum where researchers and practitioners interested in building models using OCL or other kinds of textual languages can directly interact, report advances, share results, identify tools for language development, and discuss appropriate standards. The workshop encouraged discussions for achieving synergy from different modeling language concepts and modeling language use. The close interaction enabled researchers and practitioners to identify common interests and options for potential cooperation.
(2 pages, PDF: 42kb via HTTP)


[Brüning et al., 2012]
Jens Brüning, Martin Gogolla, Lars Hamann, and Mirco Kuhlmann. Evaluating and Debugging OCL Expressions in UML Models. In Achim D. Brucker and Jacques Julliand, editors, Proc. 6th Int. Conf. Tests and Proofs (TAP 2012), pages 156-162. Springer, Berlin, LNCS 7305, 2012.
This paper discusses the relationship between tests and proofs with focus on a tool for UML and OCL models. Tests are thought of as UML object diagrams and theorems or properties which are to be checked are represented as OCL constraints, i.e., class invariants or operation pre- and postconditions. The paper shows for the UML and OCL tool USE (UML-based Specification Environment) how to trace and debug the validity of an expected theorem (an OCL constraint) within a given test case (a state model in the form of a UML object diagram).
(7 pages, PDF: 158kb via HTTP)


[Büttner et al., 2012]
Fabian Büttner, Marina Egea, Jordi Cabot, and Martin Gogolla. Verification of ATL Transformations Using Transformation Models and Model Finders. In Kokichi Futatsugi and Shaoying Liu, editors, Proc. 14th Int. Conf. Formal Engineering Methods (ICFEM 2012), pages 198-213. Springer, Berlin, LNCS 7635, 2012.
In MDE models constitute pivotal elements of the software to be built. If models are specified well, transformations can be employed for different purposes, e.g., to produce final code. However, it is important that models produced by a transformation from valid input models are valid, too, where validity refers to the metamodel constraints, often written in OCL. Transformation models are a way to describe this Hoare-style notion of partial correctness of model transformations using only metamodels and constraints. In this paper, we provide an automatic translation of declarative, rule-based ATL transformations into such transformation models, providing an intuitive and versatile encoding of ATL into OCL that can be used for the analysis of various properties of transformations. We furthermore show how existing model verifiers (satisfiability checkers) for OCL-annotated metamodels can be applied for the verification of the translated ATL transformations, providing evidence for the effectiveness of our approach in practice.
(16 pages, PDF: 342kb via HTTP)


[Cabot and Gogolla, 2012]
Jordi Cabot and Martin Gogolla. Object Constraint Language (OCL): A Definitive Guide. In Marco Bernardo, Vittorio Cortellessa, and Alphonso Pierantonio, editors, Proc. 12th Int. School Formal Methods for the Design of Computer, Communication and Software Systems: Model-Driven Engineering, pages 58-90. Springer, Berlin, LNCS 7320, 2012.
The Object Constraint Language (OCL) started as a complement of the UML notation with the goal to overcome the limitations of UML (and in general, any graphical notation) in terms of precisely specifying detailed aspects of a system design. Since then, OCL has become a key component of any model-driven engineering (MDE) technique as the default language for expressing all kinds of (meta)model query, manipulation and specification requirements. Among many other applications, OCL is frequently used to express model transformations (as part of the source and target patterns of transformation rules), well-formedness rules (as part of the definition of new domain-specific languages), or code-generation templates (as a way to express the generation patterns and rules). This chapter pretends to provide a comprehensive view of this language, its many applications and available tool support as well as the latest research developments and open challenges around it.
(33 pages, PDF: 352kb via HTTP)


[Dang and Gogolla, 2012]
Duc-Hanh Dang and Martin Gogolla. An Approach for Quality Assurance of Model Transformations. In Kim Hung Le and Ngoc Binh Nguyen, editors, Proc. 4th Int. Conf. Knowledge and Systems Engineering (KSE 2012), pages 223-230. IEEE CPS, 2012.
Model transformation is an important building block for model-driven approaches. It puts forward a necessity as well as a challenge for validating and verifying transformations. This paper proposes a specification method and an OCL-based framework for model transformations. The approach is based on an integration of Triple Graph Grammars and the Object Constraint Language (OCL) as a formal foundation. The OCL-based transformation framework offers an on-the-fly verification of model transformations and means for transformation quality assurance.
(8 pages, PDF: 367kb via HTTP)


[Gogolla and Vallecillo, 2012]
Martin Gogolla and Antonio Vallecillo. On Explaining Modeling Principles with Modeling Examples: A Classification Catalog. In Dan Chiorean and Benoit Combemale, editors, Proc. 8th MODELS Educators' Symposium (EduSymp 2012), pages 28-31. ACM Digital Library, 2012.
Examples are of central concern in teaching modeling. Typically, the general principles and concepts that have to be communicated are explained in terms of smaller or larger modeling examples with the hope that the examples cover the central issues of the principles and concepts well. The paper discusses a classification catalogue for examples along various criteria like syntax, semantics, pragmatics, complexity or evolution. The aim of the paper is to encourage the teaching with examples exhausting the possible spectrum of example use.
(4 pages, PDF: 172kb via HTTP)


[Hamann et al., 2012a]
Lars Hamann, Fabian Büttner, Mirco Kuhlmann, and Martin Gogolla. Optimierte Suche von Modellinstanzen für UML/OCL-Beschreibungen in USE. In Elmar J. Sinz and Andy Schürr, editors, Proc. Modellierung (MODELLIERUNG'2012), pages 155-170. Springer, LNI 201, 2012.
Konzeptuelle Modelle sind ein wichtiges Element modellgetriebener Softwareentwicklung, sowohl in der Beschreibung von Systemen als auch in der Metamodellierung domänenspezifischer Sprachen. Zu ihrer Beschreibung haben sich UML und OCL (und angelehnte Sprachen) als ein de facto Standard durchgesetzt. Validierung und Verifikation der Modelle sind hierbei wichtige Instrumente zur Sicherstellung der Modellqualität. Die Sprache ASSL (A Snapshot Sequence Language) bietet die Möglichkeit durch imperative Programmierung auf Modellebene und Backtracking konforme Instanzen systematisch zu erzeugen. Der White-Box-Ansatz ASSL ergänzt Black-Box-Ansätze, welche die Modellinstanziierung durch Abbildung auf (bspw.) ein Problem der relationalen Logik lösen. Dieser Beitrag beschreibt, wie die durch ASSL-Programme aufgespannten Suchräume durch Ausnutzung der Modellabdeckung der OCL-Constraints und der Modellstruktur erheblich verkleinert werden können und gibt einen Ausblick darauf, wie bestehende Black-Box-Ansätze in ASSL integriert werden können, um innerhalb eines imperativen Rahmens Teilinstanziierungen deklarativ beschreiben zu können.
(16 pages, PDF: 294kb via HTTP)


[Hamann et al., 2012b]
Lars Hamann, Martin Gogolla, and Daniel Honsel. Towards Supporting Multiple Execution Environments for UML/OCL Models at Runtime. In Nelly Bencomo, Gordon Blair, Sebastian Götz, Brice Morin, and Bernhard Rumpe, editors, Proc. 7th Int. Workshop Models at Runtime (MRT 2012), pages 46-51. ACM Digital Library, 2012.
Our approach allows the developer to verify whether a model corresponds to a concrete implementation in terms of the JVM (Java Virtual Machine) by validating assumptions about model structure and behavior. In previous work, we focused on (a) the validation of static model properties by monitoring invariants, (b) basic dynamic properties by specifying pre- and postconditions of an operation and (c) employment of protocol state machines for validating advanced dynamic properties. This paper discusses the generalization of the underlying architecture for the JVM to easily incorporate other runtime environments like the CLR (Common Language Runtime). This is realized by extracting common features like method calls and identifying relevant interception points.
(6 pages, PDF: 1141kb via HTTP)


[Hamann et al., 2012c]
Lars Hamann, Oliver Hofrichter, and Martin Gogolla. OCL-Based Runtime Monitoring of Applications with Protocol State Machines. In Antonio Vallecillo and Juha-Pekka Tolvanen, editors, Proc. 8th European Conf. Modelling Foundations and Applications (ECMFA 2012), pages 384-399. Springer, Berlin, LNCS 7349, 2012.
This paper presents an approach that enables users to monitor and verify the behavior of an application running on a virtual machine (like the Java virtual machine) at an abstract model level. Models for object-oriented implementations are often used as a foundation for formal verification approaches. Our work allows the developer to verify whether a model corresponds to a concrete implementation by validating assumptions about model structure and behavior. In previous work, we focused on (a) the validation of static model properties by monitoring invariants and (b) basic dynamic properties by specifying pre- and postconditions of an operation. In this paper, we extend our work in order to verify and validate advanced dynamic properties, i.e., properties of sequences of operation calls. This is achieved by integrating support for monitoring UML protocol state machines into our basic validation engine.
(16 pages, PDF: 429kb via HTTP)


[Hamann et al., 2012d]
Lars Hamann, Oliver Hofrichter, and Martin Gogolla. Towards Integrated Structure and Behavior Modeling with OCL. In Robert France, Juergen Kazmeier, Ruth Breu, and Colin Atkinson, editors, Proc. 15th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2012), pages 235-251. Springer, Berlin, LNCS 7590, 2012.
Precise modeling with UML and OCL traditionally focuses on structural model features like class invariants. OCL also allows the developer to handle behavioral aspects in form of operation pre- and postconditions. However, behavioral UML models like statecharts have rarely been integrated into UML and OCL modeling tools. This paper discusses an approach that combines precise structure and behavior modeling: Class diagrams together with class invariants restrict the model structure and protocol state machines constrain the model behavior. Protocol state machines can take advantage of OCL in form of OCL state invariants and OCL pre- and postconditions for state transitions. Protocol state machines can cover complete object life cycles in contrast to pre- and postconditions which only affect single operation calls. The paper reports on the chosen state machine features and their implementation in a UML and OCL validation and verification tool.
(17 pages, PDF: 266kb via HTTP)


[Hamann et al., 2012e]
Lars Hamann, Laszlo Vidacs, Martin Gogolla, and Mirco Kuhlmann. Abstract Runtime Monitoring with USE. In Tom Mens, Anthony Cleve, and Rudolf Ferenc, editors, Proc. European Conf. Software Maintenance and Reengineering (CSMR'2012), pages 549-552. IEEE, 2012.
We present a tool that permits developers to monitor and verify assumptions at an abstract level about an application running on a virtual machine. On the implementation level, a so-called platform aligned model (PAM) described in the UML (Unified Modeling Language) and enriched by OCL (Object Constraint Language) requirements is used to formalize these assumptions. Our solution allows a developer to concentrate on verifying core parts of an implementation while ignoring major parts of peripheral technical details. In order to easily detect a PAM which characterizes the central requirements, we propose a semi-automatic approach. First, a complete program model is generated by analyzing the source code. Afterwards, this model is reduced by the user to central classes and associations. This reduced model is enriched by the assumptions about the expected behavior of the system. The monitor connects to the running system at a particular point in time and builds up an abstract snapshot, i.e., an instance of the PAM, which corresponds to the current state. When the application is further executed this snapshot is synchronized by listening to changes in the running system. During monitoring the stated assumptions are validated and possible violations are reported to the user.
(4 pages, PDF: 964kb via HTTP)


[Hofrichter et al., 2012]
Oliver Hofrichter, Lars Hamann, Martin Gogolla, and Frank Steimke. The Secret Life of OCL Constraints. In Mira Balaban, Jordi Cabot, Martin Gogolla, and Claas Wilke, editors, Proc. 12th Int. Workshop Object Constraint Language (OCL 2012), pages 63-64. ACM Digital Library, 2012.
This paper reports on the use of OCL constraints in a German e-government project and focuses on the identication of diverse manifestations of invariants. Beyond invariants' formal content three other manifestations are identied: (a) feedback by a tool based on the processed invariants, (b) the invariant's textual explanation as a basis for a modeler who uses the invariants and (c) implicit assumptions for a model transformation resulting from the invariants.
(2 pages, PDF: 201kb via HTTP)


[Kuhlmann and Gogolla, 2012a]
Mirco Kuhlmann and Martin Gogolla. From UML and OCL to Relational Logic and Back. In Robert France, Juergen Kazmeier, Ruth Breu, and Colin Atkinson, editors, Proc. 15th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2012), pages 415-431. Springer, Berlin, LNCS 7590, 2012.
Languages like UML and OCL are used to precisely model systems. Complex UML and OCL models therefore represent a crucial part of model driven development, as they formally specify the main system properties. Consequently, creating complete and correct models is a critical concern. For this purpose, we provide a lightweight model validation method based on efficient SAT solving techniques. In this paper, we present a transformation from UML class diagram and OCL concepts into relational logic. Relational logic in turn represents the source for advanced SAT-based model instance finders like Kodkod. This paper focuses on a natural transformation approach which aims to exploit the features of relational logic as directly as possible through straitening the handling of main UML and OCL features. This approach allows us to explicitly benefit from the efficient handling of relational logic in Kodkod and to interpret found results backwards in terms of UML and OCL.
(17 pages, PDF: 316kb via HTTP)


[Kuhlmann and Gogolla, 2012b]
Mirco Kuhlmann and Martin Gogolla. Strengthening SAT-Based Validation of UML/OCL Models by Representing Collections as Relations. In Antonio Vallecillo and Juha-Pekka Tolvanen, editors, Proc. 8th European Conf. Modelling Foundations and Applications (ECMFA 2012), pages 32-48. Springer, Berlin, LNCS 7349, 2012.
Collections, i.e., sets, bags, ordered sets and sequences, play a central role in UML and OCL models. Essential OCL operations like role navigation, object selection by stating properties and the first order logic universal and existential quantifiers base upon or result in collections. In this paper, we show a uniform representation of flat and nested, but typed OCL collections as well as strings in form of flat, untyped relations, i.e., sets of tuples, respecting the OCL particularities for nesting, undefinedness and emptiness. Transforming collections and strings into relations is particularly needed in the context of automatic model validation on the basis of a UML and OCL model transformation into relational logic.
(17 pages, PDF: 338kb via HTTP)


[Kuhlmann et al., 2012]
Mirco Kuhlmann, Lars Hamann, Martin Gogolla, and Fabian Büttner. A Benchmark for OCL Engine Accuracy, Determinateness, and Efficiency. Software and Systems Modeling, 11(2):165-182, 2012. DOI 10.1007/s10270-010-0174-8.
Since several years, the Object Constraint Language (OCL) is a central component in modeling and transformation languages like the Unified Modeling Language, the Meta Object Facility, and Query View Transformation. Consequently, approaches MDE (Model-Driven Engineering) depend on this language. OCL is present not only in areas influenced by the OMG but also in the Eclipse Modeling Framework (EMF). Thus the quality of OCL and its realization in tools seems to be crucial for the success of model-driven development. Surprisingly, up to now a benchmark for OCL to measure quality properties has not been proposed. This paper puts forward in the first part the concepts of a comprehensive OCL benchmark. Our benchmark covers (1) OCL engine accuracy (e.g., for the handling of the undefined value, the use of variables and the implementation of OCL standard operations), (2) OCL engine determinateness properties (e.g., for the collection operations `any' and `flatten'), and (3) OCL engine efficiency (for data type and user-defined operations). In the second part, this paper empirically evaluates the proposed benchmark concepts by examining several OCL tools. The paper clarifies a number of differences in handling particular language features and under specifications in the OCL standard.
(17 pages, PDF: 292kb via HTTP)


[Sohr et al., 2012]
Karsten Sohr, Mirco Kuhlmann, Martin Gogolla, Hongxin Hu, and Gail-Joon Ahn. Comprehensive Two-Level Analysis of Role-Based Delegation and Revocation Policies with UML and OCL. Information and Software Technology, 54(12):1396-1417, 2012.
Role-based access control (RBAC) has become the de facto standard for access management in various large-scale organizations. Often role-based policies must implement organizational rules to satisfy compliance or authorization requirements, e.g., the principle of separation of duty (SoD). To provide business continuity, organizations should also support the delegation of access rights and roles, respectively. This, however, makes access control more complex and error-prone, in particular, when delegation concepts interplay with SoD rules. A systematic way to specify and validate access control policies consisting of organizational rules such as SoD as well as delegation and revocation rules shall be developed. A domain-specific language for RBAC as well as delegation concepts shall be made available. In this paper, we present an approach to the precise specification and validation of role-based policies based on UML and OCL. We significantly extend our earlier work, which proposed a UML-based domain-specific language for RBAC, by supporting delegation and revocation concepts. We show the appropriateness of our approach by applying it to a banking application. In particular, we give three scenarios for validating the interplay between SoD rules and delegation/revocation. To the best of our knowledge, this is the first attempt to formalize advanced RBAC concepts, such as history-based SoD as well as various delegation and revocation schemes, with UML and OCL. With the rich tool support of UML, we believe our work can be employed to validate and implement real-world role-based policies.
(54 pages, PDF: 801kb via HTTP)


[Vallecillo and Gogolla, 2012]
Antonio Vallecillo and Martin Gogolla. Typing Model Transformations Using Tracts. In Zhenjiang Hu and Juan de Lara, editors, Proc. 5th Int. Conf. Model Transformation (ICMT 2012), pages 56-71. Springer, Berlin, LNCS 7307, 2012.
As the complexity of MDE artefacts grows, there is an increasing need to rely on precise and abstract mechanisms that allow system architects to reason about the systems they design, and to test their individual components. In particular, assigning types to models and model transformations is needed for realizing many key MDE activities. This paper presents a light-weight approach to type model transformations using tracts. Advantages and limitations of the proposal are discussed, as well as the applicability of the proposal in several settings.
(16 pages, PDF: 307kb via HTTP)


[Vallecillo et al., 2012]
Antonio Vallecillo, Martin Gogolla, Loli Burgueno, Manuel Wimmer, and Lars Hamann. Formal Specification and Testing of Model Transformations. In Marco Bernardo, Vittorio Cortellessa, and Alphonso Pierantonio, editors, Proc. 12th Int. School Formal Methods for the Design of Computer, Communication and Software Systems: Model-Driven Engineering, pages 399-437. Springer, Berlin, LNCS 7320, 2012.
In this paper we present some of the key issues involved in model transformation specification and testing, discuss and classify some of the existing approaches, and introduce the concept of Tract, a generalization of model transformation contracts. We show how Tracts can be used for model transformation specification and black-box testing, and the kinds of analyses they allow. Some representative examples are used to illustrate this approach.
(39 pages, PDF: 774kb via HTTP)


[Brüning and Gogolla, 2011]
Jens Brüning and Martin Gogolla. UML Metamodel-based Workflow Modeling and Execution. In Lea Kutvonen and Pontus Johnson, editors, Proc. Enterprise Distributed Object Computing (EDOC'2011), pages 97-106. IEEE, 2011.
In this paper, we present a UML metamodel-based approach for creating and executing workflow models. The workflow modeling language is introduced through its abstract syntax, and an evaluation shows how this language supports known workflow patterns. Some patterns can be expressed easier compared to established languages like EPCs or BPMN. Organizational and data aspects in workflow models can be described on the basis of the presented metamodel. The workflow models can be instantiated and executed with a tool realizing parts of the UML action semantics. At an early stage of design, our workflow models can be evaluated by testing scenarios with the used tool in combination with the developed workflow plug in. Employing the tool, dynamic aspects of the workflow process models together with data and organizational aspects can be evaluated. During execution of the workflow scenarios, the workflow models can be adaptively changed, and data can be captured and evaluated by formulating process mining queries with UML's OCL (Object Constraint Language).
(10 pages, gzipped PostScript: 462kb via HTTP, uncompressed PostScript: 1274kb via HTTP, PDF: 329kb via HTTP)


[Brüning et al., 2011]
Jens Brüning, Lars Hamann, and Andreas Wolff. Extending ASSL: Making UML Metamodel-based Workflows Executable. In Jordi Cabot, Robert Clariso, Martin Gogolla, and Burkhart Wolff, editors, Proc. Workshop OCL and Textual Modelling (OCL'2011). ECEASST, Electronic Communications, journal.ub.tu-berlin.de/eceasst/issue/view/56, 2011.
ASSL is a language that enables UML developers to test and certify UML and OCL models. Snapshots of system states are semi-automatically created and main parts of the UML action semantics is implemented by the language. Its interpreter is the well-known UML modeling tool USE. The article proposes a number of language extensions to ASSL. These include (sub-) procedure calls and pre- and postcondition checks on entering and exiting of operations using OCL. The paper motivates the need for these extensions as well as their usage and development along the problem of metamodel-based execution of workflow models. Executable workflow models, driven by ASSL procedures, are introduced in detail to present the usage of ASSL and our extensions.
(13 pages, gzipped PostScript: 442kb via HTTP, uncompressed PostScript: 1559kb via HTTP, PDF: 228kb via HTTP)


[Büttner and Gogolla, 2011]
Fabian Büttner and Martin Gogolla. Modular Embedding of the Object Constraint Language into a Programming Language. In Adenilso Simao and Carrol Morgan, editors, Proc. 14th Brazilian Symposium on Formal Methods (SBMF'2011), pages 124-139. Springer, Berlin, LNCS 7021, 2011.
The Object Constraint Language (OCL) is a well-accepted ingredient in model-driven engineering and accompanying modeling languages like UML (Unified Modeling Language) or EMF (Eclipse Modeling Framework) which support object-oriented software development. Among various possibilities, OCL offers the formulation of state invariants and operation contracts in form of pre- and postconditions. With OCL, side effect free query operations can be implemented. However, for operations changing the system state an implementation cannot be given within OCL. In order to fill this gap, this paper proposes the language SOIL (Simple OCL-like Imperative Language). The expression sub-language of SOIL is identical to OCL. SOIL adds well-known, traditional imperative constructs. Thus by employing OCL and SOIL, it is possible to describe any operation in a declarative way and in an operational way on the modeling level without going into the details of a conventional programming language. In contrast to other similar approaches, the embedding of OCL into SOIL is done in a new, careful way so that elementary properties in OCL are preserved (for example, commutativity of logical conjunction). The paper discusses the central principles behind this conservative embedding of OCL into SOIL. SOIL has a sound formal semantics and is implemented in the UML and OCL tool USE (UML-based Specification Environment).
(16 pages, gzipped PostScript: 297kb via HTTP, uncompressed PostScript: 733kb via HTTP, PDF: 165kb via HTTP)


[Büttner et al., 2011]
Fabian Büttner, Jordi Cabot, and Martin Gogolla. On Validation of ATL Transformation Rules By Transformation Models. In Harald Cichos, Frederic Fondement, Levi Lucio, and Stephan Weissleder, editors, Proc. Workshop on Model-Driven Engineering, Verification, and Validation (MODEVVA'2011). ACM, 2011.
Model-to-model transformations constitute an important ingredient in model-driven engineering. As real world transformations are complex, systematic approaches are required to ensure their correctness. The ATLAS Transformation Language (ATL) is a mature transformation language which has been successfully applied in several areas. However, the executable nature of ATL is a barrier for the validation of transformations. In contrast, transformation models provide an integrated structural description of the source and target metamodels and the transformation between them. While not being executable, transformation models are wellsuited for analysis and verification of transformation properties. In this paper, we discuss (a) how ATL transformations can be translated into equivalent transformation models and (b) illustrate how these surrogates can be employed to validate properties of the original transformation.
(8 pages, gzipped PostScript: 355kb via HTTP, uncompressed PostScript: 1731kb via HTTP, PDF: 283kb via HTTP)


[Cabot et al., 2011]
Jordi Cabot, Robert Clariso, Martin Gogolla, and Burkhart Wolff, editors. Preface for Proc. 11th International Workshop on OCL and Textual Modelling, http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/archive, 2011. Electronic Communications of the EASST, Vol. 44. Satellite Events at the TOOLS'2011 Conference.
This preface reports on the 11th workshop on OCL and Textual Modelling held at the TOOLS Federated Conferences in 2011. The workshop focused on the current state of OCL (standard, tool support, adoption, ...) and the application of textual modelling to different domains. The workshop included presentations together with a discussion session.

[Chimiak-Opoka et al., 2011]
Joanna Dobroslawa Chimiak-Opoka, Birgit Demuth, Andreas Awenius, Dan Chiorean, Sebastien Gabel, Lars Hamann, and Edward Willink. OCL Tools Report based on the IDE4OCL Feature Model. In Jordi Cabot, Robert Clariso, Martin Gogolla, and Burkhart Wolff, editors, Proc. Workshop OCL and Textual Modelling (OCL'2011). ECEASST, Electronic Communications, journal.ub.tu-berlin.de/eceasst/issue/view/56, 2011.
Previously we have developed the idea of an Integrated Development Environment for OCL (IDE4OCL). Based on the OCL community's feedback we have also designed and published an IDE4OCL feature model. Here we present a report on selected OCL tools developed by the authors and their teams. Each author gives an overview of their OCL tool, provides a top level architecture, and gives an evaluation of the tool features in a web framework. The framework can also be used by other potential OCL users and tool developers. For users it may serve as an aid to choose a suitable tool for their OCL use scenarios. For tool developers it provides a comparative view for further development of the OCL tools. Our plans are to maintain the collected data and extend this web framework by further OCL tools. Additionally, we would like to encourage sharing of OCL development resources.
(19 pages, PDF: 344kb via HTTP)


[Duran et al., 2011]
Francisco Duran, Martin Gogolla, and Manuel Roldan. Tracing Properties of UML and OCL Models with Maude. In Francisco Duran and Vlad Rusu, editors, Proc. Workshop Algebraic Methods in Model-based Software Engineering (AMMSE'2011), pages 81-97. Electronic Proceedings in Theoretical Computer Science, EPTCS 56, 2011.
The starting point of this paper is a system described in form of a UML class diagram where system states are characterized by OCL invariants and system transitions are defined by OCL pre- and postconditions. The aim of our approach is to assist the developer in learning about the consequences of the described system states and transitions and about the formal implications of the properties that are explicitly given. We propose to draw conclusions about the stated constraints by translating the UML and OCL model into the algebraic specification language and system Maude, which is based on rewrite logic. We will concentrate in this paper on employing Maude's capabilities for state search. Maude's state search offers the possibility to describe a start configuration of the system and then explore all configurations reachable by rewriting. The search can be adjusted by formulating requirements for the allowed states and the allowed transitions.
(19 pages, gzipped PostScript: 2746kb via HTTP, uncompressed PostScript: 23146kb via HTTP, PDF: 331kb via HTTP)


[Gogolla, 2011a]
Martin Gogolla. Direction Neutral Language Transformation with Metamodels. Dagstuhl Reports, 1(1):57-57, 2011. Dagstuhl Seminar 11031: Bidirectional Transformations bx. Organized by Zhenjiang Hu, Andy Schürr, Perdita Stevens, James Terwilliger. Long version: http://www.dagstuhl.de/mat/Files/11/11031/11031.GogollaMartin1.Paper.pdf.
The aim of this work is to sketch a general metamodel-based frame for describing potentially bidirectional transformations between software languages. We propose to describe a single language with a metamodel consisting of a UML class diagram with classes, attributes and associations and accompanying OCL constraints. A language description is separated into a syntax and a semantics part. The allowed object diagrams of the syntax part correspond to the syntactically allowed words of the language. The semantics can associate with every word of the language certain semantical objects. However, only finite fractions of the semantics can be handled in metamodel tools. Having two languages described by their metamodels, a transformation between them is established by another metamodel, a transformation model. The transformation model can associate a syntax object from one language with a syntax object from the other language in a direction neutral way and opens the possibility for bidirectionality. Analogously, semantical objects can be connected. Transformation properties like `equivalence' or `embedding' can and must be expressed with constraints. Thus, the approach describes syntax and semantics of the languages, their transformation and their properties in a uniform way by means of metamodels.
(14 pages, gzipped PostScript: 192kb via HTTP, uncompressed PostScript: 2076kb via HTTP, PDF: 141kb via HTTP)


[Gogolla, 2011b]
Martin Gogolla. Runtime Monitoring of Java Bytecode with UML and OCL Models. Dagstuhl Reports, 1(11):107-107, 2011. Dagstuhl Seminar 11481: Models@run.time. Organized by Uwe Aßmann, Nelly Bencomo, Betty H.C. Cheng, Robert B. France.
Implementations of object-oriented software usually contain a lot of technical classes. Thus, the central parts of an application, e.g., the business rules, may be hidden among peripheral functionality like user-interface classes or classes managing persistence. Our approach makes use of modern virtual machines and allows the developer to profile an application in order to achieve an abstract monitoring and quality assurance of central application components during runtime. We represent virtual machine bytecode in form of a so-called platform-aligned model (PAM) comprising OCL invariants and pre- and postconditions. We show a prototype implementation as an extension of the UML and OCL tool USE.

[Gogolla, 2011c]
Martin Gogolla. UML and OCL in Conceptual Modeling. In David W. Embley and Bernhard Thalheim, editors, Handbook of Conceptual Modeling: Theory, Practice, and Research Challenges, pages 85-122. Springer, Berlin, 2011.
The development of the Entity-Relationship (ER) model is one of the cornerstones for conceptual modeling of information systems. The Unified Modeling Language (UML) and the Object Constraint Language (OCL) take up central ideas from the ER model and put them into a broad software development context by proposing various graphical sublanguages and diagrams for specialized software development tasks and by adding more precision through textual constraints. The first section of this contribution will introduce the correspondence between basic ER modeling concepts and their UML counterparts. The next part will explain how more advanced conceptual modeling concepts can be formulated in UML. In the following section we will use OCL for features not expressible in diagrammatic form. Then we turn to the description of Relational databases with UML. Before we conclude, we will show how to metamodel conceptual modeling features with UML itself and discuss further relevant work from the literature.
(43 pages, PDF: 382kb via HTTP)


[Gogolla and Vallecillo, 2011]
Martin Gogolla and Antonio Vallecillo. Tractable Model Transformation Testing. In Robert France, Jochen M. Küster, Behzad Bordbar, and Richard F. Paige, editors, Proc. 7th Int. Conf. Modelling Foundations and Applications (ECMFA'2011), pages 221-235. Springer, Berlin, LNCS 6698, 2011.
Model transformation (MT) testing is gaining interest as the size and complexity of MTs grows. In general it is very difficult and expensive (time and computational complexity-wise) to validate in full the correctness of a MT. This paper presents a cost effective MT testing approach based on the concept of Tract, which is a generalization of the concept of Model Transformation Contract. A Tract defines a set of constraints on the source and target metamodels, a set of source-target constraints, and a tract test suite, i.e., a collection of source models satisfying the source constraints. We automatically generate input test suite models, which are then transformed into output models by the transformation under test, and the results checked with the USE tool (UML-based Specification Environment) against the constraints defined for the transformation. We show the different kinds of tests that can be conducted over a MT using this automated process, and the kinds of problems it can help uncovering.
(15 pages, gzipped PostScript: 381kb via HTTP, uncompressed PostScript: 2476kb via HTTP)


[Gogolla and Wolff, 2011]
Martin Gogolla and Burkhart Wolff, editors. Proc. 5th Int. Conf. Tests and Proofs (TAP'2011). Springer, Berlin, LNCS 6706, 2011.
This book contains the papers accepted for the 5th International Conference on Tests and Proofs (TAP'2011).

[Gogolla et al., 2011]
Martin Gogolla, Lars Hamann, Jie Xu, and Jun Zhang. Exploring (Meta-)Model Snapshots by Combining Visual and Textual Techniques. In Fabio Gadducci and Leonardo Mariani, editors, Proc. Workshop Graph Transformation and Visual Modeling Techniques (GTVMT'2011). ECEASST, Electronic Communications, journal.ub.tu-berlin.de/eceasst/issue/view/53, 2011.
One central task in software development by means of graph-based techniques is to inspect and to query the underlying graph. Important issues are, for example, to detect general graph properties like connectivity, to explore more special features like the applicability of left-hand side rules in graph transformations, or to validate snapshots of evolving systems by checking properties in an on-the-fly way. We propose a new approach combining visual and textual techniques for exploring graphs. We emphasize a particular aspect of the underlying graph by showing or hiding nodes and edges. We offer three different ways to explore (meta-)model snapshots which may be combined: (1) selection by object identity and class membership, (2) selection by OCL expression, and (3) selection by path length. One main motivation for our work is to access large or complicated graphs in a systematic way. We evaluate our approach by different middle-sized scenarios. Our evaluation shows that the approach works for large graphs with about 1000 nodes and 2000 edges and for graphs which instantiate metamodels representing software engineering artifacts.
(14 pages, gzipped PostScript: 858kb via HTTP, uncompressed PostScript: 11489kb via HTTP)


[Hamann et al., 2011]
Lars Hamann, Martin Gogolla, and Mirco Kuhlmann. OCL-Based Runtime Monitoring of JVM Hosted Applications. In Jordi Cabot, Robert Clariso, Martin Gogolla, and Burkhart Wolff, editors, Proc. Workshop OCL and Textual Modelling (OCL'2011). ECEASST, Electronic Communications, journal.ub.tu-berlin.de/eceasst/issue/view/56, 2011.
In this paper we present an approach that enables users to monitor and verify the behavior of an application running on a virtual machine at the model level. Concrete implementations of object-oriented software usually contain a lot of technical classes. Thus, the central parts of an application, e.g., the business rules, may be hidden among peripheral functionality like user-interface classes or classes managing persistency. Our approach makes use of modern virtual machines and allows the devloper to profile an application in order to achieve an abstract monitoring and verification of central application components. We represent virtual machine bytecode in form of a so-called platform-aligned model (PAM) comprising OCL invariants and pre- and postconditions. In contrast to related work, our approach uses the original source or bytecode of the monitored application as it stands and does not require any changes. We show a prototype implementation as an extension of the UML and OCL tool USE. Also, we investigate the impact of our approach to the execution time of a monitored system.
(21 pages, gzipped PostScript: 5598kb via HTTP, uncompressed PostScript: 39553kb via HTTP, PDF: 2242kb via HTTP)


[Kuhlmann et al., 2011a]
Mirco Kuhlmann, Lars Hamann, and Martin Gogolla. Extensive Validation of OCL Models by Integrating SAT Solving into USE. In Judith Bishop and Antonio Vallecillo, editors, Proc. 49th Int. Conf. Objects, Models, Components, and Patterns (TOOLS'2011), pages 289-305. Springer, Berlin, LNCS 6705, 2011.
The Object Constraint Language (OCL) substantially enriches modeling languages like UML, MOF or EMF with respect to formulating meaningful model properties. In model-centric approaches, an accurately defined model is a requisite for further use. During development of a model, continuous validation of properties and feedback to developers is required, since many design flaws can then be directly discovered and corrected. For this purpose, lightweight validation approaches which allow developers to perform automatic model analysis are particularly helpful. We provide a new method for efficiently searching for model instances. The existence or non-existence of model instances with certain properties allows significant conclusions about model properties. Our approach is based on the translation of UML and OCL concepts into relational logic and its realization with SAT solvers. We explain various use cases of our proposal, for example, completion of partly defined model instances so that particular properties hold in the completed model instances. Our proposal is realized by integrating a model validator as a plugin into the UML and OCL tool USE.
(17 pages, gzipped PostScript: 4669kb via HTTP, uncompressed PostScript: 32144kb via HTTP)


[Kuhlmann et al., 2011b]
Mirco Kuhlmann, Karsten Sohr, and Martin Gogolla. Comprehensive Two-Level Analysis of Static and Dynamic RBAC Constraints with UML and OCL . In Jongmoon Baik, Fabio Massacci, and Mohammad Zulkernine, editors, Proc. Secure Software Integration and Reliability Improvement (SSIRI'2011), pages 108-117. IEEE, 2011.
Organizations with stringent security requirements like banks or hospitals frequently adopt role-based access control (RBAC) principles to simplify their internal permission management. Authorization constraints represent a fundamental advanced RBAC concept enabling precise restrictions on access rights. Thereby, the complexity of the resulting security policies increases so that tool support for comfortable creation and adequate validation is required. We propose a new approach to developing and analyzing RBAC policies using UML for modeling RBAC core concepts and OCL to realize authorization constraints. Dynamic (i. e., time-dependent) constraints, their visual representation in UML and their analysis are of special interest. The approach results in a domain-specific language for RBAC which is highly configurable and extendable with respect to new RBAC concepts and classes of authorization constraints and allows the developer to validate RBAC policies in an effective way. The approach is supported by a UML and OCL validation tool.
(10 pages, gzipped PostScript: 433kb via HTTP, uncompressed PostScript: 1232kb via HTTP)


[Bezivin et al., 2010]
Jean Bezivin, Robert France, Martin Gogolla, Oystein Haugen, Gabriele Taentzer, and Daniel Varro. Teaching Modeling: Why, When, What? In Sudipto Ghosh, editor, Workshops and Symposia at 12th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2009), pages 55-62. Springer, Berlin, LNCS 6002, 2010.
This paper reports on a panel discussion held during the Educators' Symposium at MODELS'2009. It shortly explains the context provided for the discussion and outlines the statements made by the panelists. The panelists were asked to make their statements along a number of topics relevant to teaching modeling like: Notation, Semantics, Programming, Tooling, Suitability, Metamodeling.
(8 pages, gzipped PostScript: 76kb via HTTP, uncompressed PostScript: 156kb via HTTP)


[Brüning et al., 2010]
Jens Brüning, Martin Gogolla, and Peter Forbrig. Modeling and Formally Checking Workflow Properties Using UML and OCL. In Peter Forbrig and Horst Günther, editors, Proc. 9th Int. Conf. Perspectives in Business Informatics Research (BIR'2010), pages 130-145. Springer, Berlin, LNBIP 64, 2010.
In this paper, a new metamodel for workflows is described by using UML. The underlying UML class diagram is formally extended with OCL pre- and postconditions for operations and OCL invariants for system states. The metamodel allows the developer to specify processes, activities in processes and temporal relations between them. Known workflow patterns are formally captured in the metamodel and sophisticated temporal relations between activities can be expressed easily. Development of workflow models is explained as well as process instantiation and process execution on the basis of a tool realizing parts of the UML action semantics. Prototypical process execution and animation allows the designer to discover properties of the designed processes and activities in early phases of the development without the need for building a full implementation.
(16 pages, gzipped PostScript: 542kb via HTTP, uncompressed PostScript: 1915kb via HTTP)


[Büttner, 2010]
Fabian Büttner. Reusing OCL in the Definition of Imperative Languages. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2010.
The Object Constraint Language (OCL) has proven to be a valuable ingredient for the specification of UML modesl engineering. This paradigm puts forward a necessity as well as a challenge of a formal foundation for presenting precisely models and supporting automatic model manipulations. This thesis focuses on a model-driven approach in which metamodeling and model transformation are seen as the core of the approach. On the one hand, metamodeling, which is a means for defining modeling languages, aims to precisely present models for specific purposes. On the other hand, model transformation is a robust approach for (1) transforming models from one language into another language, (2) tackling the challenge how to choose a right level of abstraction, and to relate levels of abstraction with each other, and (3) supporting software evolution and maintenance. We propose an integration of two light-weight formal methods, the Object Constraint Language (OCL) and Triple Graph Grammars (TGGs), in order to form a core foundation for the model-driven approach. TGGs incorporating OCL allow us to explain relationships between models in precise way. On this foundation, we develop a textual language in order to describe transformations and to realize transformations. From such a declarative description of transformations, we propose employing OCL in order to derive operational scenarios for model transformation. This results in an OCL-based framework for model transformation. This framework offers means for transformation quality assurance such as verifying model transformations in an on-the-fly way, checking well-formedness of models, and maintaining model consistency. We explore case studies showing the practical applicability of our approach. Especially, TGGs incorporating OCL allow us to describe the operation semantics of use cases in a precise way. This approach on the one hand can be broaden in order to describe the operational semantics of modeling languages. On the other hand, it allows us to generate scenarios as test cases, to validate system behavior, and to check the conformance between use case models and design models. This supports basic constructions of an. It allows to formulate logical propositions for models that typically cannot be expressed in the visual modeling paradigms of UML. A similar textual ingredient is required for the imperative specification of behavior in certain applications of UML, most prominently Executable UML models and model transformation. There is no such imperative language in the UML standard, but there are several candidates for such a language that are based on OCL for expressions. One of them is ImperativeOCL, which is part of the OMG Query, Views, Transformations (QVT) standard. However, the embedding of OCL into several of these languages is what we call a non-modular embedding. Such a non-modular embedding results in problems w.r.t. to language semantics and/or sets up obstacles for the reuse of existing OCL tools and instruments. In our work we therefore define requirements for a modular embedding of OCL into an imperative language. We introduce our language SOIL (Simple OCL-based Imperative Language) which embeds OCL in a modular way. We provide an informal description of SOIL as well as a formal definition of the language syntax and semantics, and prove its consistency and type safety. We describe applications of our approach in two fields: first, the extension of the UML-based Specification Environment (USE) by an imperative language and, second, the development of the model transformation tool XGenerator2 that has been successfully applied in several eGovernment projects. Our work makes three major contributions. First, we provide a critical review of the embedding of OCL into existing programming languages. Second, we provide a simple but already useful OCL-based imperative language with a sound and formal semantics that can be implemented out of the box using existing OCL engines. Third, our work contributes a general guideline for a safe embedding of OCL into other languages.

[Büttner et al., 2010]
Fabian Büttner, Martin Gogolla, Lars Hamann, Mirco Kuhlmann, and Arne Lindow. On Better Understanding OCL Collections *or* An OCL Ordered Set is not an OCL Set. In Sudipto Ghosh, editor, Workshops and Symposia at 12th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2009), pages 276-290. Springer, Berlin, LNCS 6002, 2010.
Modeling languages like UML or EMF support textual constraints written in OCL. OCL allows the developer to use various collection kinds for objects and values. OCL 1.4 knows sequences, sets, and bags, while OCL 2.0 adds ordered sets. We argue that this addition in the OCL standard was not carried out in a careful way and worsened conceptional problems that were already present previously. We discuss a new way of establishing the connection between the various collection kinds on the basis of explicitly highlighting and characterizing fundamental collection properties.
(15 pages, gzipped PostScript: 287kb via HTTP, uncompressed PostScript: 8140kb via HTTP)


[Cabot et al., 2010a]
Jordi Cabot, Joanna Chimiak-Opoka, Martin Gogolla, Frederic Jouault, and Alexander Knapp. Ninth International Workshop on The Pragmatics of OCL and other textual specification languages. In Sudipto Ghosh, editor, Workshops and Symposia at 12th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2009), pages 256-260. Springer, Berlin, LNCS 6002, 2010.
This paper reports on the 9th OCL workshop held at the MODELS conference in 2009. The workshop focused on the challeges of using OCL in a variety of new scenarios (e.g., model verification and validation, code generation, test-driven development, transformations) and application domains (e.g., domain-specific languages, web semantics) in which OCL is now being used due to the increasing popularity of model-driven development processes and the important role OCL play in them. The workshop included sessions with paper presentations and a final round discussion.
(5 pages, gzipped PostScript: 74kb via HTTP, uncompressed PostScript: 157kb via HTTP)


[Cabot et al., 2010b]
Jordi Cabot, Tony Clark, Manuel Clavel, and Martin Gogolla. Tenth International Workshop on OCL and Textual Modelling. In Jürgen Dingel and Arnor Solberg, editors, Workshops and Symposia at 13th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2010), pages 329-333. Springer, Berlin, LNCS 6627, 2010.
This paper reports on the 10th OCL Workshop held at the MODELS conference in 2010. The workshop's motivation was to bring together researchers and practitioners in textual modelling standards, such as OCL, to report advances in the field, to share results, to identify common areas and potential for integration, and to identify common tools for developing textual modelling languages, with a view to advancing the state-of-the art. The workshop included sessions with paper presentations and a final discussion session.

[Dang et al., 2010a]
Duc-Hanh Dang, Anh-Hoang Truong, and Martin Gogolla. Checking the Conformance between Models Based on Scenario Synchronization. Journal of Universal Computer Science, 16(17):2293-2312, 2010.
Narrowing the wide conceptual gap between problem and implementation domains is considered a significant factor within software engineering. Currently, such a relation is often obtained using mappings between metamodels for a structural semantics. This paper proposes an approach based on the integration of Triple Graph Grammars (TGGs) and the Object Constraint Language (OCL) in order to explain a behavioral relation between models at different levels of abstraction. Triple rules incorporating OCL allow us to synchronize execution scenarios of a system at two levels. In this way we obtain an integrated operational semantics of the models as well as the possibility for conformance verification between them. We illustrate our approach with a case study for the relation between use case and design models.
(20 pages, gzipped PostScript: 1149kb via HTTP, uncompressed PostScript: 14447kb via HTTP)


[Dang et al., 2010b]
Duc-Hanh Dang, Anh-Hoang Truong, and Martin Gogolla. On Scenario Synchronization. In Ahmed Bouajjani and Wei-Ngan Chin, editors, Proc. 8th Int. Symp. Automated Technology for Verification and Analysis (ATVA'2010), pages 97-111. Springer, Berlin, LNCS 6252, 2010.
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.
(15 pages, gzipped PostScript: 356kb via HTTP, uncompressed PostScript: 795kb via HTTP, PDF: 479kb via HTTP)


[France and Gogolla, 2010]
Robert France and Martin Gogolla. Essentials of the 5th Educators' Symposium at MODELS 2009. In Sudipto Ghosh, editor, Workshops and Symposia at 12th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2009), pages 36-39. Springer, Berlin, LNCS 6002, 2010.
This paper reports on the Educators' Symposium held at the MODELS 2009 conference. It shortly explains motivation of the symposium, shows the accepted papers of the symposium and mentions the people who have contributed.
(4 pages, gzipped PostScript: 64kb via HTTP, uncompressed PostScript: 129kb via HTTP)


[Gogolla et al., 2010]
Martin Gogolla, Lars Hamann, and Mirco Kuhlmann. Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases. In Gordon Fraser and Angelo Gargantini, editors, Proc. 4th Int. Conf. Test and Proof (TAP'2010), pages 38-54. Springer, Berlin, LNCS 6143, 2010.
Within model-driven development, class invariants play a central role. An essential property of a collection of invariants is the independence of each single invariant, i.e., the invariant at hand cannot be deduced from the other invariants. The paper explains with three example models the details of an approach for automatically proving and representing invariant independence on the basis of a script constructing large test cases for the underlying model. Analysis of invariant independence is visualized by means of several diagrams like a `test configuration and result' diagram, an `invariant dependence detail' diagram, and an `invariant dependence overview' diagram. The paper also discusses how to build the test case construction script in a systematic way. The test case construction script is written by the model developer, but a general construction frame for the script is outlined.
(17 pages, gzipped PostScript: 321kb via HTTP, uncompressed PostScript: 6366kb via HTTP)


[Hamann and Gogolla, 2010]
Lars Hamann and Martin Gogolla. Improving Model Quality by Validating Constraints with Model Unit Tests. In Levi Lucio, Elisangela Vieira, and Stephan Weissleder, editors, Proc. Workshop on Model-Driven Engineering, Verification, and Validation (MODEVVA'2010), pages 49-55. IEEE, 2010.
(6 pages, PDF: 204kb via HTTP)

[Hamann et al., 2010]
Lars Hamann, Martin Gogolla, and Mirco Kuhlmann. Zur Validierung von Kompositionsstrukturen in UML mit USE. In Gregor Engels, Dimitris Karagiannis, and Heinrich C. Mayr, editors, Proc. Modellierung (MODELLIERUNG'2010), pages 169-177. Gesellschaft für Informatik, LNI P-161, 2010.
In der Softwareentwicklung rücken Modelle zunehmend in den Focus des Entwicklungsprozesses. Dadurch steigen auch die Anforderungen an deren Qualität. Mit dem an der Universität Bremen entwickelten UML/OCL-Werkzeug USE können bereits bestimmte Qualitätsaspekte von Modellen analysiert werden. Dieser Artikel beschreibt neue Modellierungselemente der UML 2 und zeigt, welchen Beitrag eine Weiterentwicklung von USE auf dem Weg zu einer integrierten Semantik der UML 2 Kompositionsstrukturen leisten kann.
(9 pages, gzipped PostScript: 118kb via HTTP, uncompressed PostScript: 3470kb via HTTP)


[Soeken et al., 2010]
Mathias Soeken, Robert Wille, Mirco Kuhlmann, Martin Gogolla, and Rolf Drechsler. Verifying UML/OCL Models Using Boolean Satisfiability. In Wolfgang Müller, editor, Proc. Design, Automation and Test in Europe (DATE'2010). IEEE, 2010.
Nowadays, modeling languages like UML are essential in the design of complex software systems and also start to enter the domain of hardware and hardware/software codesign. Due to shortening time-to-market demands, first-time-right requirements have thereby to be satisfied. In this paper, we propose an approach that makes use of Boolean satisfiability for verifying UML/OCL models. We describe how the respective components of a verification problem, namely system states of a UML model, OCL constraints, and the actual verification task, can be encoded and afterwards automatically solved using an off-the-shelf SAT solver. Experiments show that our approach can solve verification tasks significantly faster than previous methods while still supporting a large variety of UML/OCL constructs.
(4 pages, gzipped PostScript: 88kb via HTTP, uncompressed PostScript: 226kb via HTTP)


[Tratt and Gogolla, 2010]
Laurence Tratt and Martin Gogolla, editors. Proc. 3rd Int. Conf. on Model Transformation (ICMT'2010). Springer, Berlin, LNCS 6142, 2010.
This book contains the papers accepted for the 3rd International Conference on Model Transformation (ICMT'2010).

[Büttner and Kuhlmann, 2009]
Fabian Büttner and Mirco Kuhlmann. Shortcomings of the Embedding of OCL into QVT ImperativeOCL. In Michel R.V. Chaudron, editor, Workshops and Symposia at 11th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2008), pages 263-272. Springer, Berlin, LNCS 5421, 2009.
MOF QVT introduces ImperativeOCL as an imperative language for operational descriptions of model transformations (QVT operational mappings). ImperativeOCL extends conventional OCL by expressions with side-effects. A couple of semantical problems arise from the way OCL is embedded into ImperativeOCL - imperative expressions are modelled as a subtype of OCL expressions. This paper points out these semantical problems and proposes a change to the operational mappings language of QVT that resolves these problems, following an approach that reuses OCL by composition rather than by inheritance in the abstract syntax of ImperativeOCL. The proposed change reduces the complexity of the imperative language, removes undefinedness, and leaves OCL conformant to its original definition.
(10 pages, gzipped PostScript: 550kb via HTTP, uncompressed PostScript: 10798kb via HTTP)


[Cabot et al., 2009]
Jordi Cabot, Martin Gogolla, and Pieter Van Gorp. Eighth International Workshop on OCL Concepts and Tools. In Michel R.V. Chaudron, editor, Workshops and Symposia at 11th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2008), pages 257-262. Springer, Berlin, LNCS 5421, 2009.
This paper reports on the 8th OCL workshop held at the MODELS conference in 2008. The workshop focussed on how to evaluate, compare and select the right OCL tools for a given purpose and how to deal with the expressiveness and complexity of OCL. The workshop included sessions with paper presentations as well as a special tool demo session.
(6 pages, gzipped PostScript: 118kb via HTTP, uncompressed PostScript: 286kb via HTTP)


[Dang, 2009]
Duc-Hanh Dang. On Integrating Triple Graph Grammars and OCL for Model-Driven Development. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2009.
Software systems become more and more complex. Despite significant advances in code-centric technologies such as advanced programming languages and integrated development environments (IDEs), developing complex software systems is still a laborious task. Model-centric software development has emerged as a promising paradigm, indicating a shift from ``code-centric'' to ``model-centric'' engineering. This paradigm puts forward a necessity as well as a challenge of a formal foundation for presenting precisely models and supporting automatic model manipulations. This thesis focuses on a model-driven approach in which metamodeling and model transformation are seen as the core of the approach. On the one hand, metamodeling, which is a means for defining modeling languages, aims to precisely present models for specific purposes. On the other hand, model transformation is a robust approach for (1) transforming models from one language into another language, (2) tackling the challenge how to choose a right level of abstraction, and to relate levels of abstraction with each other, and (3) supporting software evolution and maintenance. We propose an integration of two light-weight formal methods, the Object Constraint Language (OCL) and Triple Graph Grammars (TGGs), in order to form a core foundation for the model-driven approach. TGGs incorporating OCL allow us to explain relationships between models in precise way. On this foundation, we develop a textual language in order to describe transformations and to realize transformations. From such a declarative description of transformations, we propose employing OCL in order to derive operational scenarios for model transformation. This results in an OCL-based framework for model transformation. This framework offers means for transformation quality assurance such as verifying model transformations in an on-the-fly way, checking well-formedness of models, and maintaining model consistency. We explore case studies showing the practical applicability of our approach. Especially, TGGs incorporating OCL allow us to describe the operation semantics of use cases in a precise way. This approach on the one hand can be broaden in order to describe the operational semantics of modeling languages. On the other hand, it allows us to generate scenarios as test cases, to validate system behavior, and to check the conformance between use case models and design models. This supports basic constructions of an automatic and semi-automatic design.

[Dang and Gogolla, 2009a]
Duc-Hanh Dang and Martin Gogolla. On Integrating OCL and Triple Graph Grammars. In Michel R.V. Chaudron, editor, Workshops and Symposia at 11th Int. Conf. Model Driven Engineering Languages and Systems (MODELS'2008), pages 124-137. Springer, Berlin, LNCS 5421, 2009.
Triple Graph Grammars (TGGs) tend to be a promising approach for explaining relationships between models in general, and model co-evolution and model consistency within model-driven development in particular. Declarative TGG descriptions can be translated into operational scenarios for model integration, model synchronization, and model transformation. To realize such scenarios, restrictions formulated with the Object Constraint Language (OCL) are an important factor. How to integrate TGGs and OCL is a topic of ongoing research activities. There are strong similarities between the result of such an integration and the Queries, Views and Transformations (QVT) standard of the Object Management Group (OMG). We propose a language for this integration: One part of this language has a one-one mapping to TGGs and the remaining part covers OCL concepts. The language is realized in our tool UML-based Specification Environment (USE) by taking two views on operations derived from TGG rules: Declarative OCL pre- and postconditions are employed as operation contracts, and imperative command sequences are taken as an operational realization. USE offers full OCL support for restricting models and metamodels with invariants, for checking pre- and postconditions of operations as well as for validating and animating transformation operations. Our approach covers a complete realization of TGGs incorporating OCL within our tool USE.
(13 pages, gzipped PostScript: 5555kb via HTTP, uncompressed PostScript: 21481kb via HTTP)


[Dang and Gogolla, 2009b]
Duc-Hanh Dang and Martin Gogolla. Precise Model-Driven Transformations Based on Graphs and Metamodels. In Dang Van Hung and Padmanabhan Krishnan, editors, Proc. 7th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM 2009), pages 307-316. IEEE, 2009.
Presenting precisely models and supporting automatic manipulation of models are at the heart of model-centric software development. A formal foundation for these tasks is a necessity as well as a challenge. We present a model-driven approach based on the integration of two light-weight formal methods, the Object Constraint Language (OCL) and Triple Graph Grammars (TGGs). OCL together with metamodeling allows us to present precisely models. With TGGs we can carry out model manipulations, especially model transformations. We focus on explaining the tool which realizes our approach. This tool is developed as an extension of the UML-based Specification Environment (USE), which offers full OCL support. A case study showing the transformation between statecharts and extended hierarchical automata explains our approach.
(10 pages, gzipped PostScript: 497kb via HTTP, uncompressed PostScript: 2639kb via HTTP)


[France and Gogolla, 2009]
Robert France and Martin Gogolla. Educators' Symposium at MODELS 2009. In Andy Schürr and Bran Selic, editors, Proc. 11th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2008), pages 753-754. Springer, Berlin, LNCS 5795, 2009.
The Educator's Symposium at the MODELS conference, the premier conference devoted to the topic of model-driven engineering of software-based systems, is intended as a forum in which educators and trainers can meet to discuss pedagogy, use of technology in the classroom, and share their experience pertaining to teaching modeling techniques and model-driven development.
(2 pages, gzipped PostScript: 33kb via HTTP, uncompressed PostScript: 76kb via HTTP)


[Gogolla, 2009a]
Martin Gogolla. Object Constraint Language. In Ling Liu and M. Tamer Öszu, editors, Encyclopedia of Database Systems, pages 1927-1929. Springer, Berlin, 2009.
The Unified Modeling Language (UML) includes a textual language called Object Constraint Language (OCL). OCL allows users to navigate in class diagrams, to formulate queries, and to restrict class diagrams with integrity constraints. Roughly speaking from a practical prespective, the OCL may be viewed as an object-oriented version of the Structured Query Language (SQL) originally developed for the Relational data model. Roughly speaking from a theoretical perspective, OCL may be viewed as a variant of first-order predicate logic with quantifiers on finite domains only. OCL has a well-defined syntax and semantics.

[Gogolla, 2009b]
Martin Gogolla. Towards Model Validation and Verification with SAT Techniques. In Bernd Becker, Valeria Bertacoo, Rolf Drechsler, and Masahiro Fujita, editors, Algorithms and Applications for Next Generation SAT Solvers. IBFI, Schloss Dagstuhl, Germany, 2009. Dagstuhl Seminar Proceedings 09461. 11 pages.
After sketching how system development and the UML (Unified Modeling Language) and the OCL (Object Constraint Language) are related, validation and verification with the tool USE (UML-based Specification Environment) is demonstrated. As a more efficient alternative for verification tasks, two approaches using SAT-based techniques are put forward: First, a direct encoding of UML and OCL with Boolean variables and propositional formulas, and second, an encoding employing an intermediate, higher-level language (KODKOD, stongly connected to ALLOY). A number of further, presently not realized verification and validation tasks and the transformation of higher-level modeling concepts into simple UML/OCL models, which are checkable with SAT-based techniques, are shortly discussed. Finally, the potential of SAT-based techniques for model development is again emphasized.
(11 pages, gzipped PostScript: 330kb via HTTP, uncompressed PostScript: 4877kb via HTTP)


[Gogolla, 2009c]
Martin Gogolla. Unified Modeling Language. In Ling Liu and M. Tamer Öszu, editors, Encyclopedia of Database Systems, pages 3232-3239. Springer, Berlin, 2009.
The Unified Modeling Language (UML) is a graphical language for visualizing, specifying, constructing, and documenting the artifacts of a software-intensive system. The UML offers a standard way to write a system's blueprints, including conceptual things such as business processes and system functions as well as concrete things such as programming language statements, database schemas, and reusable software components.

[Gogolla et al., 2009]
Martin Gogolla, Mirco Kuhlmann, and Lars Hamann. Consistency, Independence and Consequences in UML and OCL Models. In Catherine Dubois, editor, Proc. 3rd Int. Conf. Test and Proof (TAP'2009), pages 90-104. Springer, Berlin, LNCS 5668, 2009.
Properties in UML models are frequently formulated as OCL invariants or OCL pre- and postconditions. The UML-based Specification Environment (USE) supports validation and to a certain degree verification of such properties. USE allows the developer to prove the consistency and independence of invariants by building automatically generated test cases. USE also assists the developer in checking consequences and making deductions from invariants by automatically constructing a set of test cases in form of model scenarios. Suspected deductions are either falsified by a counter test case or are shown to be valid in a fixed finite search space.
(16 pages, gzipped PostScript: 206kb via HTTP, uncompressed PostScript: 2441kb via HTTP)


[Kuske et al., 2009]
Sabine Kuske, Martin Gogolla, Hans-Jörg Kreowski, and Paul Ziemann. Towards an Integrated Graph-Based Semantics for UML. Journal on Software and System Modeling, 8(3):403-422, 2009.
This paper shows how a central part of the Unified Modeling Language UML can be integrated into a single visual semanticmodel. It discusses UML models composed of class, object, state, sequence and collaboration diagrams and presents an integrated semantics of these models. As formal basis the theoretically well-founded area of graph transformation is employed which supports a visual and rule-based transformation of UML model states. For the translation of a UML model into a graph transformation system the operations in class diagrams and the transitions in state diagrams are associatedwith graph transformation rules that are then combined into one system in order to obtain a single coherent semantic description. Operation calls in sequence and collaboration diagrams can be associated with applications of graph transformation rules in the constructed graph transformation system so that valid sequence and collaboration diagrams correspond to derivations, i.e., to sequences of graph transformation rule applications. The main aim of this paper is to provide a formal framework that supports visual simulation of integrated UML specifications in which system states and state changes are modeled in a straighforward way.
(19 pages, gzipped PostScript: 6533kb via HTTP, uncompressed PostScript: 10475kb via HTTP, PDF: 489kb via HTTP)


[Akehurst et al., 2008]
Dave Akehurst, Martin Gogolla, and Steffen Zschaler, editors. Proc. OCL4ALL - Modelling Systems with OCL, http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/archive, 2008. Electronic Communications of the EASST, Vol. 9. Satellite Events at the MoDELS'2007 Conference.
The requirements that the modelling community wants to see supported by OCL now go far beyond its initial requirements. When OCL was conceived it was designed as a language for supporting precise modelling. The advent of the MDA (Model Driven Architecture) vision and the rapid acceptance of MDE (Model Driven Engineering) approaches emphasize new application domains (like Domain Specific Languages or Semantic Web). This increase in new modelling languages causes a need for new OCL-like languages for systems modelling, frequently developed as extensions to the original. As this year's special focus, the OCL workshop recognised that OCL is used as a basis for many text-based navigation languages. The workshop brought together the community that defines these extensions in order to consolidate the experiences, successes and failures involved in doing so. The workshop discussed the potential for redesigning or at least restructuring the OCL standard definition in order to better facilitate and support third-party extensions to the language. The workshop aimed to look specifically at how to apply the key software engineering principles of modularity and reuse to the definition of OCL. The workshop was organized as a part of the MoDELS 2007 Conference in Nashville, Tennesee, USA. It continued the series of OCL workshops held at previous UML/MoDELS conferences in York (2000), Toronto (2001), San Francisco (2003), Lisbon (2004), Montego Bay (2005) and Genova (2006). This EC-EASST volume contains improved papers of the papers already published on-line. The workshop organizers are grateful to authors for their effort to polish their papers. Last but not least, we are grateful to the members of the Program Committee, the additional referees, all participants of the workshop and to the EC-EASST editors for their support.

[Büttner et al., 2008]
Fabian Büttner, Mirco Kuhlmann, Martin Gogolla, Jens Dietrich, Frank Steimke, Andre Pankratz, Alina Stosiek, and Alexander Salomon. MDA Employed in a Joint eGovernment Strategy: An Experience Report. In Terry Bailey, editor, Proc. 3rd ECMDA Workshop ``From Code Centric To Model Centric Software Engineering'' (2008), http://www.esi.es/modelplex/c2m/program.php, 2008. European Software Institute.
DOL (Deutschland OnLine, Germany online) is a joint eGovernment strategy in Germany. Its objectives include the development of standards for electronic data exchange between public authorities. To achieve this goal, DOL projects are employing UML models, profiles, and tools: A cross-project conceptual model and a profile for common core components are used to harmonize the different domain specific models, and a further DOL specific UML profile has been developed to attach data transmission details to the domain specific models. The automated creation of data exchange specifications from these platform-specific models is realised by an MDA tool developed in DOL: The XGenerator allows the validation of UML models against applied profiles by checking OCL constraints, and the XGenerator supports a flexible, MDA based generation of XML Schema definitions, DocBook based documentation, and WSDL descriptions. This paper reports on how UML profiles and formal MDA techniques have been assembled into a reusable architecture for the development of data exchange specifications.
(13 pages, gzipped PostScript: 289kb via HTTP, uncompressed PostScript: 711kb via HTTP)


[Dang, 2008]
Duc-Hanh Dang. Triple Graph Grammars and OCL for Validating System Behavior. In Hartmut Ehrig, Reiko Heckel, Grzegorz Rozenberg, and Gabriele Taentzer, editors, Proc. 4th Int. Conf. Graph Transformations (ICGT'2008), pages 481-483. Springer, Berlin, LNCS 5214, 2008.
We propose an approach based on the integration of Triple Graph Grammars (TGGs) and the Object Constraint Language (OCL) for checking the conformance between use case and design models.
(3 pages, gzipped PostScript: 52kb via HTTP, uncompressed PostScript: 106kb via HTTP)


[Gogolla, 2008a]
Martin Gogolla. On Horizontal and Vertical Relationships between Models. In Uwe Aßmann, Jean Bézivin, Richard Paige, Bernhard Rumpe, and Douglas C. Schmidt, editors, Perspectives Workshop: Model Engineering of Complex Systems (MECS). IBFI, Schloss Dagstuhl, Germany, 2008. Dagstuhl Seminar Proceedings 08331. 4 pages.
Detecting, modeling and managing relationships between models are central tasks within model-driven engineering. By taking a simple view on software development, we distinguish in a vertical dimension between domain-specific models, core models, and executable models. A typical example for a vertical relationship is the refinement relationship beween a core model and an executable model. In the horizontal dimension, there may be several so-called property models which have the task to validate or verify particular properties of the core model. Software development coincides in our view with model development, and therefore finding the right models and their relationships is a crucial task.
(4 pages, gzipped PostScript: 107kb via HTTP, uncompressed PostScript: 1544kb via HTTP)


[Gogolla, 2008b]
Martin Gogolla. Teaching Touchy Transformations. In Michal Smialek, editor, MODELS Educators' Symposium (EDUSYMP'2008), pages 13-25. Warsaw University, ISBN 83-916444-8-0, 2008.
This paper reports on a teaching unit on model development and model transformation. One example model is first developed and considered as the source of various possible transformations. These transformations are explained implicitly afterwards by showing the different target models obtained by the transformations. The source model and the target models each emphasize a particular aspect, and an appropriate teaching method is chosen in order to communicate central ideas in a well-understandable way. The chosen teaching methods stress active student participation in the development of models and transformations.
(13 pages, gzipped PostScript: 167kb via HTTP, uncompressed PostScript: 2235kb via HTTP, PDF: 135kb via HTTP)


[Gogolla et al., 2008a]
Martin Gogolla, Fabian Büttner, and Duc-Hanh Dang. From Graph Transformation to OCL using USE. In Andy Schürr, Manfred Nagl, and Albert Zündorf, editors, Proc. 3rd Int. Workshop Applications of Graph Transformation with Industrial Relevance (AGTIVE '07), pages 585-586. Springer, Berlin, LNCS 5088, 2008.
With the tool USE, UML class diagrams with additional OCL constraints can be validated and properties can be formally checked. Constraints may be class invariants and operation pre- and postconditions. USE builds system states with object diagrams and expresses system evolution with operations employing basic state manipulations by creating and destroying objects (nodes) and links (edges) and by modifying attributes. A graph transformation system is expressed in USE by modeling the working graph with an object diagram and by expressing the graph transformation rules with operations modifying the working graph. These operations encapsulate an executable sequence of basic state manipulations and are additionally characterized by pre- and postconditions in which application conditions of the graph transformation rules can be expressed. The graph transformation rules are formulated in a special language permitting to describe left and right hand side of rules as well as their application conditions. This language is automatically translated into USE command sequences and OCL pre- and postconditions. The rules may be executed interactively through operation calls. The current working graph and its properties may be inspected on a graphical user interface and through evaluation of OCL expressions, e.g., for determining the rule redexes in the current working graph. Additionally, OCL invariants may be used to restrict the permitted working graphs.
(2 pages, gzipped PostScript: 104kb via HTTP, uncompressed PostScript: 1693kb via HTTP)


[Gogolla et al., 2008b]
Martin Gogolla, Fabian Büttner, and Mirco Kuhlmann. System Modeling with USE (UML-based Specification Environment). Genie Logiciel (French Software Engineering Journal), 85:57-58, 2008. ISSN 0295-6322.
The Unified Modeling Language (UML) is accepted today as an important standard for developing software. UML tools however provide little support for validating and checking models in early development phases. There is also nearly no substantial support for the Object Constraint Language (OCL). Therefore, our group works on an approach for the validation of UML models and OCL constraints based on animation and certification. The USE tool (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production. Our group also applies OCL and USE in concrete projects. OCL and USE are employed in DOL, a joint eGovernment strategy in Germany. The objectives of DOL include standardisation of electronic data exchange between public agencies. DOL is employing UML models, profiles, and tools: Reusable conceptual models are provided, the UN/CEFACT profile for CoreComponents is used to ensure correct derivation of models in concrete projects, and a further UML profile (the XOEV profile) has been developed to attach data transmission details to the conceptual models. The automated creation of data exchange specifications is supported by the MDA tool XGenerator: It allows the validation of UML models against their applied profiles using OCL constraints, and it supports a flexible, MDA-based generation of XML Schema definitions, DocBook-based documentation, and WSDL descriptions.
(3 pages, gzipped PostScript: 175kb via HTTP, uncompressed PostScript: 528kb via HTTP)


[Gogolla et al., 2008c]
Martin Gogolla, Mirco Kuhlmann, and Fabian Büttner. A Benchmark for OCL Engine Accuracy, Determinateness, and Efficiency. In Krzysztof Czarnecki, editor, Proc. 11th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2008), pages 446-459. Springer, Berlin, LNCS 5301, 2008.
The Object Constraint Language (OCL) is a central element in modeling and transformation languages like UML, MOF, and QVT. Consequently approaches for MDE (Model-Driven Engineering) depend on OCL. However, OCL is present not only in these areas influenced by the OMG but also in the Eclipse Modeling Framework (EMF). Thus the quality of OCL and its realization in tools seems to be crucial for the success of model-driven development. Surprisingly, up to now a benchmark for OCL to measure quality properties has not been proposed. This paper puts forward in the first part the concepts of a comprehensive OCL benchmark. Our benchmark covers (A) OCL engine accuracy (e.g., for the undefined value and the use of variables), (B) OCL engine determinateness properties (e.g., for the collection operations any and flatten), and (C) OCL engine efficiency (for data type and user-defined operations). In the second part, this paper empirically evaluates the proposed benchmark concepts by examining a number of OCL tools. The paper discusses several differences in handling particular OCL language features and underspecifications in the OCL standard.
(15 pages, gzipped PostScript: 160kb via HTTP, uncompressed PostScript: 423kb via HTTP)


[Kuhlmann and Gogolla, 2008a]
Mirco Kuhlmann and Martin Gogolla. Analyzing Semantic Properties of OCL Operations by Uncovering Interoperational Relationships. Electronic Communications of the EASST, http://eceasst.cs.tu-berlin.de/index.php/eceasst, 9, 2008. UML/MoDELS Workshop on OCL (OCL4ALL'2007), 17 Pages.
The OCL (Object Constraint Language) as part of the UML (Unified Modeling Language) is a rich language with different collection kinds (sets, multi-sets, sequences) and a large variety of operations defined thereon. Without negating the strong correlation between both fields we can say that these operations have their origin partly in logic (like the operations forAll and exists) and partly in computer science, in particular database systems (like the operation select). Some of these operations may be expressed in terms of other operations. This paper presents a systematic study of relationships which hold between OCL features like the mentioned operations. Apart from presenting the relationships between operations in a conceptual way, the relationships are described by a formal metamodel allowing systematic and computer supported access to the operation relationships by querying an underlying formal description.
(18 pages, gzipped PostScript: 744kb via HTTP, uncompressed PostScript: 4735kb via HTTP)


[Kuhlmann and Gogolla, 2008b]
Mirco Kuhlmann and Martin Gogolla. Modeling and Validating Mondex Scenarios Described in UML and OCL with USE. Formal Aspects of Computing, 20(1):79-100, 2008.
This paper describes the Mondex case study with UML class diagrams and restricting OCL constraints. The constraints have been formulated either as OCL class invariants or as OCL pre- and postconditions. The proposed two models include UML class diagrams and OCL constraints which have been checked by the UML and OCL tool USE (UML-based Specification Environment). USE allows validation of a model by testing it with scenarios. The Mondex case study has been validated by positive and negative test cases. The test cases allow the validity of the various constraints to be traced and checked. Validation results are presented as textual protocols or as UML sequence diagrams where starting, intermediate, and resulting system states are represented by UML object diagrams. UML sequence diagrams, UML object diagrams, and textual protocols are shown with varying degrees of detail for the attributes, constraints, and executed commands.
(25 pages, gzipped PostScript: 726kb via HTTP, uncompressed PostScript: 28464kb via HTTP)


[Mustafa et al., 2008]
Tanveer Mustafa, Karsten Sohr, Duc-Hanh Dang, Michael Drouineaud, and Stefan Kowski. Implementing Advanced RBAC Administration Functionality with USE. Electronic Communications of the EASST, http://eceasst.cs.tu-berlin.de/index.php/eceasst, 15, 2008. MoDELS Workshop on OCL (OCL Concepts and Tools 2008), 19 Pages.
Role-based access control (RBAC) is a powerful means for laying out and developing higher-level organizational policies such as separation of duty, and for simplifying the security management process. One of the important aspects of RBAC is authorization constraints that express such organizational policies. While RBAC has generated a great interest in the security community, organizations still seek a flexible and effective approach to impose role-based authorization constraints in their security-critical applications. In particular, today often only basic RBAC concepts have found their way into commercial RBAC products; specifically, authorization constraints are not widely supported. In this paper, we present an RBAC administration tool that can enforce certain kinds of role-based authorization constraints such as separation of duty constraints. The authorization constraint functionality is based upon the OCL validation tool USE. We also describe our practical experience that we gained on integrating OCL functionality into a prototype of an RBAC administration tool that shall be extended to a product in the future.
(19 pages, gzipped PostScript: 790kb via HTTP, uncompressed PostScript: 1980kb via HTTP)


[Sohr et al., 2008]
Karsten Sohr, Michael Drouineaud, Gail-Joon Ahn, and Martin Gogolla. Analysing and Managing Role-Based Access Control Policies. IEEE Transactions on Knowledge and Data Engineering, 20(7):924-939, 2008. Published online 13 March 2008. DOI 10.1109/TKDE.2008.28.
Today more and more security-relevant data is stored on computer systems; security-critical business processes are mapped to their digital counterparts. This situation applies to various domains such as health care industry, digital government, and financial service institutes requiring that different security requirements must be fulfilled. Authorisation constraints can help the policy architect design and express higher-level organisational rules. Although the importance of authorisation constraints has been addressed in the literature, there does not exist a systematic way to verify and validate authorisation constraints. In this paper, we specify both non-temporal and history-based authorisation constraints in the Object Constraint Language (OCL) and first-order linear temporal logic (LTL). Based upon these specifications, we attempt to formally verify role-based access control policies with the help of a theorem prover and to validate policies with the USE system, a validation tool for OCL constraints. We also describe an authorisation engine, which supports the enforcement of authorisation constraints.
(14 pages, gzipped PostScript: 5437kb via HTTP, uncompressed PostScript: 24166kb via HTTP, PDF: 475kb via HTTP)


[Varro et al., 2008]
Daniel Varro, Mark Asztalos, Denes Bisztray, Artur Boronat, Duc-Hanh Dang, Rubino Geiss, Joel Greenyer, Pieter Van Gorp, Ole Kniemeyer, Anantha Narayanan, Edgars Rencis, and Erhard Weinell. Transformation of UML Models to CSP: A Case Study for Graph Transformation Tools. In Andy Schürr, Manfred Nagl, and Albert Zündorf, editors, Proc. 3rd Int. Workshop Applications of Graph Transformation with Industrial Relevance (AGTIVE '07), pages 540-565. Springer, Berlin, LNCS 5088, 2008.
Graph transformation provides an intuitive mechanism for capturing model transformations. In the current paper, we investigate and compare various graph transformation tools using a compact practical model transformation case study carried out as part of the AGTIVE 2007 Tool Contest. The aim of this case study is to generate formal CSP processes from high-level UML activity diagrams, which enables to carry out mathematical analysis of the system under design.
(26 pages, gzipped PostScript: 1011kb via HTTP, uncompressed PostScript: 17896kb via HTTP, PDF: 645kb via HTTP)


[Akehurst et al., 2007]
Dave Akehurst, Martin Gogolla, and Steffen Zschaler. OCL4ALL - Modelling Systems with OCL. In Holger Giese, editor, Satellite Events at the MoDELS'2007 Conference, pages 176-181. Springer, Berlin, LNCS 5002, 2007.
This year's OCL workshop at the MODELS conference looked out to usages of OCL outside the direct context of UML or beyond the capabilities of standard OCL. It was a very interesting and successful workshop, which apart from the presentation of 10 papers a lively discussion on various topics surround current usage of OCL was held. Six main topics recurred throughout the discussions: (1) Means and uses of transformation to other languages, (2) Support for side-effects and executability, (3) Continuing need for OCL, (4) Providing extensions to the standard, (5) Platform independence of the language, (6) Formality of the language. This summary report presents the results of the workshop and the discussions.
(6 pages, gzipped PostScript: 79kb via HTTP, uncompressed PostScript: 157kb via HTTP)


[Dang, 2007]
Duc-Hanh Dang. Validation of System Behavior from an Integrated Semantics of Use Case and Design Models. In Claudia Pons, editor, Proc. Doctoral Symposium ACM/IEEE 10th Int. Conf. Model-Driven Engineering Languages and Systems, http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/, 2007. CEUR Workshop Proceedings, Vol. 262. 5 pages.
This paper summarizes an approach how to specify use cases and how to solve the problem of validating the conformance between the use case model and the design model. An integrated semantics of the two models is proposed. We employ UML- and OCL-based techniques as well as ideas from graph transformation. This research contributes to model transformation within the area of Model Driven Development (MDD).
(5 pages, gzipped PostScript: 86kb via HTTP, uncompressed PostScript: 181kb via HTTP)


[Gogolla, 2007]
Martin Gogolla. Model Development in the UML-based Specification Environment (USE). In Ed Brinksma, David Harel, Angelika Mader, Perdita Stevens, and Roel Wieringa, editors, Methods for Modelling Software Systems (MMOSS). IBFI, Schloss Dagstuhl, Germany, 2007. Dagstuhl Seminar Proceedings 06351. 3 pages.
The tool USE (UML-based Specification Environment) supports analysts, designers, and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production. USE has been developed since 1998 at the University of Bremen. This paper will shortly discuss to what extent and how USE relates to the selected questions and topics (like model quality or modelling method) raised for this seminar.
(3 pages, gzipped PostScript: 60kb via HTTP, uncompressed PostScript: 122kb via HTTP)


[Gogolla et al., 2007]
Martin Gogolla, Fabian Büttner, and Mark Richters. USE: A UML-Based Specification Environment for Validating UML and OCL. Science of Computer Programming, 69:27-34, 2007.
The Unified Modeling Language (UML) is accepted today as an important standard for developing software. UML tools however provide little support for validating and checking models in early development phases. There is also no substantial support for the Object Constraint Language (OCL). We present an approach for the validation of UML models and OCL constraints based on animation and certification. The USE tool (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production.
(12 pages, gzipped PostScript: 196kb via HTTP, uncompressed PostScript: 3118kb via HTTP, PDF: 365kb via HTTP)


[Bezivin et al., 2006]
Jean Bezivin, Fabian Büttner, Martin Gogolla, Frederic Jouault, Ivan Kurtev, and Arne Lindow. Model Transformations? Transformation Models! In Oscar Nierstrasz, Jon Whittle, David Harel, and Gianna Reggio, editors, Proc. 9th Int. Conf. Model Driven Engineering Languages and Systems (MoDELS'2006). Springer, Berlin, LNCS 4199, 2006.
Much of the current work on model transformations seems essentially operational and executable in nature. Executable descriptions are necessary from the point of view of implementation. But from a conceptual point of view, transformations can also be viewed as descriptive models by stating only the properties a transformation has to fulfill and by omitting execution details. This contribution discusses the view that model transformations can be abstracted as being transformation models. As a simple example for a transformation model, the well-known transformation from the Entity-Relationship model to the Relational model is shown. A transformation model in this contribution is nothing more than an ordinary, simple model, i.e., a UML/MOF class diagram together with OCL constraints. A transformation model may transport syntax and semantics of the described domain. The contribution thus covers two views on transformations: An operational model transformation view and a descriptive transformation model view.
(15 pages, gzipped PostScript: 330kb via HTTP, uncompressed PostScript: 7278kb via HTTP)


[Büttner and Bauerdick, 2006]
Fabian Büttner and Hanna Bauerdick. Realizing UML Model Transformations with USE. In Dan Chiorean, Birgit Demuth, Martin Gogolla, and Jos Warmer, editors, UML/MoDELS Workshop on OCL (OCLApps'2006), pages 96-110. Technical University of Dresden, Technical Report TUD-FI06, 2006.
The USE (UML-based Specification Environment) tool has been successfully applied for model validation in the past. In our current work, we are enriching the USE specification language with imperative elements. We employ this extension as an assembler to realize UML model (class diagram) transformations with USE in a flexible way: UML transformations are described using a custom abstract language based on object diagram-like patterns. These descriptions are automatically translated into the imperative USE extensions. Our approach aims to provide a flexible instrument to experiment with different transformations and transformation formalisms.
(16 pages, gzipped PostScript: 131kb via HTTP, uncompressed PostScript: 421kb via HTTP)


[Büttner and Gogolla, 2006]
Fabian Büttner and Martin Gogolla. Realizing Graph Transformations by Pre- and Postconditions and Command Sequences. In Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, and Gregorz Rozenberg, editors, Proc. 3rd Int. Conf. Graph Transformations (ICGT'2006), pages 398-412. Springer, Berlin, LNCS 4178, 2006.
This paper studies two realizations of graph transformations which are based on a UML class diagram. The first realization achieves a representation in terms of descriptive pre- and postconditions. The second one yields an operationally executable command sequence in terms of basic commands for object and link creation, attribute modification, and object and link destruction. Our aim for realizing graph transformations in terms of target languages offering different views, i.e., descriptive or operational, is to take advantage of both views and to utilize the benefits which both views provide.
(15 pages, gzipped PostScript: 200kb via HTTP, uncompressed PostScript: 2004kb via HTTP)


[Chiorean et al., 2006a]
Dan Chiorean, Birgit Demuth, Martin Gogolla, and Jos Warmer. OCL for (Meta-)Models in Multiple Application Domains. In Thomas Kühne, editor, Satellite Events at the MoDELS'2006 Conference, pages 152-158. Springer, Berlin, LNCS 4364, 2006.
The workshop OCLApps 2006 was organized as a part of MoDELS/UML Conference in Genova, Italy. It continues the series of five OCL (Object Constraint Language) workshops held at previous UML/MoDELS conferences between 2000-2005. Similar to its predecessors, the workshop addressed both people from academia and industry. The advent of the MDA (Model Driven Architecture) vision and the rapid acceptance of MDE (Model Driven Engineering) approaches emphasize new application domains (like Semantic Web or Domain Specific Languages) and call for new OCL functionalities. In this context, the OCLApps 2006 Workshop, was conceived as a forum enabling researchers and industry experts to present and debate how the OCL could support these new requirements.
(6 pages, gzipped PostScript: 90kb via HTTP, uncompressed PostScript: 185kb via HTTP)


[Chiorean et al., 2006b]
Dan Chiorean, Birgit Demuth, Martin Gogolla, and Jos Warmer, editors. Proc. OCL for (Meta-)Models in Multiple Application Domains, http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/archive, 2006. Electronic Communications of the EASST, Vol. 5. Satellite Events at the MoDELS'2006 Conference.
Conceived as a formalism meant to support unambiguous and detailed modeling using UML (Unified Modeling Language), OCL (Object Constraint Language) needs adaptation to changes expressed in the modeling community. The requirements that the modelers want to see supported today by OCL go far beyond its initial requirements. The advent of the MDA (Model Driven Architecture) vision and the rapid acceptance of MDE (Model Driven Engineering) approaches emphasize new application domains (like Semantic Web or Domain Specific Languages) and call for new OCL functionalities. Apart from the requirements asked by application domains, technologies, visions and paradigms used in modeling, the formalisms and techniques currently used have to support development of large scale applications. Therefore, efficiency represents another important feature that tools supporting OCL must provide. The OCL is required to ensure a fine balance between the use of language in specifying models realized in early life-cycle phases and the rigor asked by the strong relationship with formal languages. Fixing ambiguities reported from the OCL specification without affecting the above mentioned balance is also important. Today, promoting OCL needs a conjoint support from both the research community and the industry. The main target of the OCLApps 2006 Workshop was to organize a debate forum joining people from research and industry able to present an updated state of the art in this domain, to contribute to the OCL dissemination and use. The workshop was organized as a part of MoDELS/UML 2006 Conference in Genova - Italy, continuing the series of OCL workshops held at previous UML/MoDELS conferences in: York (2000), Toronto (2001), San Francisco (2003), Lisbon (2004) and Montego Bay (2005).

[Hölscher et al., 2006]
Karsten Hölscher, Paul Ziemann, and Martin Gogolla. On Translating UML Models into Graph Transformation Systems. Journal of Visual Languages and Computing, 17(1):78-105, 2006.
In this paper we present a concept of a rigorous approach that provides a formal semantics for a fundamental subset of UML. This semantics is derived by translating a given UML model into a graph transformation system, allowing modelers to actually execute their UML model. The graph transformation system comprises graph transformation rules and a working graph which represents the current state of the modeled system. In order to support UML models which use OCL, we introduce a specific graph transformation approach that incorporates full OCL in the common UML fashion. The considered UML subset is defined by means of a metamodel similar to the UML 1.5 metamodel. The concept of a system state that represents the state of the system at a specific point in time during execution is likewise introduced by means of a metamodel. The simulated system run is performed by applying graph transformation rules on the working graph. The approach has been implemented in a research prototype which allows the modeler to execute the specified model and to validate the basic aspects of the model in an early software development phase.
(30 pages, gzipped PostScript: 528kb via HTTP, uncompressed PostScript: 4842kb via HTTP, PDF: 441kb via HTTP)


[Mwatawala et al., 2006]
Maulid W. Mwatawala, Arne Lindow, Martin Gogolla, and Marc De Meyer. Employing the Unified Modeling Language (UML) and Relational Modeling Concepts for the Development of a Schema for Fruit Flies. In Eyas El-Qawasmeh, editor, Proc. 4th Int. Multiconference on Computer Science and Information Technology (CSIT'2006). Applied Science University (ASU), Amman, Jordan, 2006.
This paper is about the analysis, conceptual design, and implementation of a fruit fly database containing information about fruit flies of Morogoro Tanzania, their description, host range, infestation levels in different fruits and the proposed management techniques. The analysis and design of the database is described with Unified Modeling Language, Entity Relationship diagrams, Extended Entity Relationship diagrams and tabular views of relational model. So this paper is an example of a practical and useful application of Information and Communication Technology in solving a pest problem in a developing country, whose economy is largely dependent on agriculture.
(12 pages, gzipped PostScript: 482kb via HTTP, uncompressed PostScript: 2505kb via HTTP)


[Vidacs et al., 2006]
Laszlo Vidacs, Martin Gogolla, and Rudolf Ferenc. From C++ Refactorings to Graph Transformations. In Jean-Marie Favre, Reiko Heckel, and Tom Mens, editors, Proc. ICGT'2006 Workshop Software Evolution and Transformation (SETRA'2006), pages 127-141. Electronic Communications of EASST (European Association of Software Science and Technology), 2006.
In this paper, we study a metamodel for the C++ programming language. We work out refactorings on the C++ metamodel and present the essentials as graph transformations. The refactorings are demonstrated in terms of the C++ source code and the C++ target code as well. Graph transformations allow to capture refactoring details on a conceptual and easy to understand, but also very precise level. Using this approach we managed to formalize two major aspects of refactorings: the structural changes and the preconditions.
(15 pages, gzipped PostScript: 1644kb via HTTP, uncompressed PostScript: 12636kb via HTTP)


[Baar et al., 2005]
Thomas Baar, Dan Chiorean, Alexandre Correa, Martin Gogolla, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, and Jos Warmer. Tool Support for OCL and Related Formalisms - Needs and Trends. In Jean-Michel Bruel, editor, Satellite Events at the MoDELS'2005 Conference, pages 1-9. Springer, Berlin, LNCS 3844, 2005.
The recent trend in software engineering to model-centered methodologies is an excellent opportunity for OCL to become a widely used specification language. If the focus of the development activities is shifted from implementation code to more abstract models then software developers need a formalism to provide a complete, unambiguous and consistent model at a very detailed level. OCL is currently the only language that can bring this level of detail to UML models. The purpose of the workshop was to identify future challenges for OCL and to discuss how OCL and its current tool support can be improved to meet these challenges. The workshop gathered numerous experts from academia and industry to report on success stories, to formulate wishes to the next generation of OCL tools, and to identify weaknesses in the language, which make OCL sometimes cumbersome to use. The workshop could also attract numerous people whose aim was to get an overview on the state of the art of OCL tool support and on how OCL can efficiently be applied in practice.
(9 pages, gzipped PostScript: 112kb via HTTP, uncompressed PostScript: 227kb via HTTP, PDF: 129kb via HTTP)


[Büttner, 2005]
Fabian Büttner. Transformation-Based Structure Model Evolution. In Jean-Michel Bruel, editor, Satellite Events at the MoDELS'2005 Conference, pages 339-340. Springer, Berlin, LNCS 3844, 2005.
This paper summarizes an approach to support evolution of software models by means of a transformation catalogue. These transformations treat UML class diagram models, OCL constraints, and existing states of the models in a coherent and consistent way. By implementing the catalogue in the UML tool USE, we effectively support developers in an iterative and incremental process for model development.
(5 pages, gzipped PostScript: 19kb via HTTP, uncompressed PostScript: 67kb via HTTP)


[Büttner et al., 2005]
Fabian Büttner, Hanna Bauerdick, and Martin Gogolla. Towards Transformation of Integrity Constraints and Database States. In Danielle C. Martin, editor, Proc. Dexa'2005 Workshop Logical Aspects and Applications of Integrity Constraints (LAAIC'2005), pages 823-828. IEEE, Los Alamitos, 2005.
This paper discusses integrity constraint evolution, from two perspectives: From the perspective of changing the constraint, and from the perspective of consequently changing an existing database state. The paper concentrates on structural models provided by UML class diagrams and OCL invariant constraints. We discuss how changes in association multiplicities can be extended to further integrity constraints attached to a class diagram and how these changes interact with given database states.
(6 pages, gzipped PostScript: 57kb via HTTP, uncompressed PostScript: 190kb via HTTP)


[Czarnecki et al., 2005]
Krzysztof Czarnecki, Jean-Marie Favre, Martin Gogolla, and Tom Mens. Essentials of the 4th UML/MoDELS Workshop in Software Model Engineering (WiSME'2005). In Jean-Michel Bruel, editor, Satellite Events at the MoDELS'2005 Conference, pages 151-159. Springer, Berlin, LNCS 3844, 2005.
Model-Driven Engineering is a form of generative engineering, by which all or at least central parts of a software application are generated from models. Model Driven Engineering should be seen as an integrative approach combining existing software engineering techniques (e.g., testing and refinement) and technical spaces (e.g., 'ModelWare', 'XmlWare') that have usually been studied in separation. The goal of the workshop is to improve common understanding of these techniques across technical spaces and create bridges and increase the synergies among the spaces. This year's WiSME workshop will concentrate on two complementing themes: Bridging Technical Spaces and Model-Driven Evolution. This paper reports on a workshop held at the 8th UML/MoDELS conference. It describes motivation and aims, organisational issues, and abstracts of the accepted papers.
(9 pages, gzipped PostScript: 39kb via HTTP, uncompressed PostScript: 95kb via HTTP)


[Ermel et al., 2005]
Claudia Ermel, Karsten Hölscher, Sabine Kuske, and Paul Ziemann. Animated Simulation of Integrated UML Behavioral Models Based on Graph Transformation. In IEEE, editor, Proc. IEEE Symposium Visual Languages and Human-Centric Computing (VL/HCC'05), pages 125-133, 2005.
This paper shows how integrated UML models combining class, object, use-case, collaboration and state diagrams can be animated in a domain-specific layout. The presented approach is based on graph transformation, i.e. UML model diagrams are translated to a graph transformation system and the behavior of the integrated model is simulated by applications of graph transformation rules. For model validation, users may prefer to see the behavior of selected model aspects as scenarios presented in the layout of the application domain. We propose to integrate animation views with the model.s graph transformation system. A prototypical validation system has been implemented recently supporting the automatic translation of a UML model into a graph transformation system, and the interactive execution and simulation of the model behavior. We sketch the tool interconnection to GenGED, a visual language environment which allows to enrich graph transformation systems for model simulation by features for animation.
(9 pages, gzipped PostScript: 374kb via HTTP, uncompressed PostScript: 948kb via HTTP, PDF: 206kb via HTTP)


[Gogolla, 2005a]
Martin Gogolla. Exploring ER and RE Syntax and Semantics with Metamodel Object Diagrams. In Peter J. Nürnberg, editor, ACM Int. Conf. Proceeding Series (Vol. 214), Proc. Metainformatics Symposium (MIS'2005). ACM Press, New York, 2005. ACM Digital Library, 12 pages.
This paper explains how a metamodel transformation between two well-known database models work: Entity-Relationship (ER) database schemas are transformed into Relational (RE) database schemas hand in hand with the transformation of ER states into Relational states. The schemas determine the syntax of the datamodels, and the set of associated states fix the semantics of the datamodels. Often, when database models are considered, one formally only treats syntactical aspects, i.e., schemas, and handles the semantics, i.e., states, merely informally. Our approach formally handles syntax and semantics of database models and their transformation within a single, uniform framework. The approach thus precisely describes properties of the datamodels and properties of the transformation. Our metamodel transformations do not simply convert ER schemas into Relational schemas, but they respect the semantics in a formal way and they can also be used the other way round in order to transfrom Relational schemas into ER ones. This opens the approach for re-engineering as well.
(12 pages, gzipped PostScript: 223kb via HTTP, uncompressed PostScript: 1000kb via HTTP)


[Gogolla, 2005b]
Martin Gogolla. Tales of ER and RE Syntax and Semantics. In James R. Cordy, Ralf Lämmel, and Andreas Winter, editors, Transformation Techniques in Software Engineering. IBFI, Schloss Dagstuhl, Germany, 2005. Dagstuhl Seminar Proceedings 05161. 51 pages.
This paper explains how four model transformations between database models work: (1) An ER (Entity-Relationship) database schema is transformed into a collection of ER database states, (2) a RE (Relational) database schema into a collection of RE database states, (3) an ER database schema into a RE database schema, and (4) a collection of ER database states into a collection of RE database states. These four separate transformations may be viewed as a single transformation between the ER datamodel and the RE datamodel. The schemas are regarded as determining the syntax of the datamodels, and the set of associated states is regarded as being the semantics of the datamodels, because the states associate meaning with the schemas. When one usually considers database models, one formally only treats syntactical aspects, i.e., schemas, and handles the semantics merely informally. Our approach allows to formally handle syntax and semantics of database models and their transformation within a single and uniform framework. The approach thus allows to precisely describe properties of the datamodels and properties of the transformation. The method behind our approach is to divide a language into a syntax and semantics part and to describe a transformation between two languages as a direction-neutral affair. Formal properties of the languages to be transformed and formal properties of the transformation are described uniformly. Transformation properties can be properties regarding syntax and semantics. The method can be applied not only to database languages but to transformations between common computer science languages.
(51 pages, gzipped PostScript: 339kb via HTTP, uncompressed PostScript: 1582kb via HTTP)


[Gogolla et al., 2005a]
Martin Gogolla, Jörn Bohling, and Mark Richters. Validating UML and OCL Models in USE by Automatic Snapshot Generation. Journal on Software and System Modeling, 4(4):386-398, 2005.
The paper studies the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model. We sketch the underlying language features and indicate how to give a formal interpretation for them.
(24 pages, gzipped PostScript: 249kb via HTTP, uncompressed PostScript: 731kb via HTTP)


[Gogolla et al., 2005b]
Martin Gogolla, Jean-Marie Favre, and Fabian Büttner. On Squeezing M0, M1, M2, and M3 into a Single Object Diagram. In Thomas Baar, Dan Chiorean, Alexandre Correa, Martin Gogolla, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, and Jos Warmer, editors, Proc. MoDELS'2005 Workshop Tool Support for OCL and Related Formalisms. In: Satellite Events at MoDELS'2005 Conference. Jean-Michel Bruel (Ed.). Springer, Berlin, LNCS 3844. Long Version: EPFL (Switzerland), Technical Report LGL-REPORT-2005-001, 2005.
We propose an approach for the integrated description of a metamodel and its formal relationship to its models and the model instantiations. The central idea is to use so-called layered graphs permitting to describe type graphs and instance graphs. A type graph can describe a collection of types and their relationships whereas an instance graph can represent instances belonging to the types and respecting the relationships required by the type graph. Type graphs and instance graphs are used iteratively, i.e., an instance graph on one layer can be regarded as a type graph of the next lower layer. Our approach models layered graphs with a UML class diagram, and operations and invariants are formally characterized with OCL and are validated with the USE tool. Metamodeling properties like strictness or well-typedness and features like potency can be formulated as OCL constraints and operations. We are providing easily understandable definitions for several metamodeling notions which are currently used in a loose way by modelers. Such properties and features can then be discussed on a rigorous, formal ground. This issue is also the main purpose of the paper, namely, to provide a basis for discussing metamodeling topics.
(14 pages, gzipped PostScript: 206kb via HTTP, uncompressed PostScript: 4894kb via HTTP)


[Sohr et al., 2005]
Karsten Sohr, Gail-Joon Ahn, Martin Gogolla, and Lars Migge. Specification and Validation of Authorization Constraints using UML and OCL. In Sabrina DeCapitani, Paul F. Syverson, and Dieter Gollmann, editors, Proc. 10th European Symp. Research in Computer Security (ESORICS'2005), pages 64-79. Springer, Berlin, LNCS 3679, 2005.
Authorisation constraints can help the policy architect design and express higher-level security policies for organisations such as financial institutes or governmental agencies. Although the importance of constraints has been addressed in the literature, there does not exist a systematic way to validate and test authorisation constraints. In this paper, we attempt to specify non-temporal constraints and historybased constraints in Object Constraint Language (OCL) which is a constraint specification language of Unified Modeling Language (UML) and describe how we can facilitate the USE tool to validate and test such policies. We also discuss the issues of identification of conflicting constraints and missing constraints.
(16 pages, gzipped PostScript: 791kb via HTTP, uncompressed PostScript: 6131kb via HTTP, PDF: 404kb via HTTP)


[Ziemann, 2005]
Paul Ziemann. An Integrated Operational Semantics for a UML Core Based on Graph Transformation. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2005.
Today, the Unified Modeling Language (UML) is widely accepted as a standard for modeling object-oriented software systems. However, its semantics is defined only in an informal way. In this thesis, we present an approach that gives a formal semantics to an important subset of UML.We cover substantial aspects of UML use case, class, object, statechart, and interaction diagrams. Additionally, full OCL is supported in the common UML fashion. The presented approach is based on the translation of a UML model into a graph transformation system consisting of graph transformation rules and a graph that represents the system state. By applying the rules on the graph, the evolution of the modeled system is simulated. To define a formal semantics, we first fix the considered subset of UML by means of a metamodel. This metamodel resembles the UML 1.5 metamodel of the OMG but is more compact. The metamodel approach is employed here with the UML community in mind that is used to this way of language definition. The concept of a system state that includes information of the system at a specific point in time during execution is likewise introduced by means of a metamodel. Aside from objects, attribute values and relationships between the objects, a system state includes processes that represent operations in execution. The actual execution is performed by applying graph transformation rules that refer to a process and modify the system state according to the semantics of the corresponding operation. This is either specified by means of an interaction diagram or is predefined. In the central part of this thesis, we describe in detail how the graph transformation rules for a given UML model are constructed. The approach is implemented in a tool that supports the user in simulating the execution of models before actually having implemented it. During the simulation, the current system state can always be checked with respect to OCL constraints. It can also be inspected with OCL queries. The modeler can check specific sequences of operation calls and gains insight into the modeled system. By analyzing the model in this way, errors can be located or the model can be validated to be correct. Therefore, this thesis contributes to the goal of improving the quality of software.

[Bauerdick et al., 2004]
Hanna Bauerdick, Martin Gogolla, and Fabian Gutsche. Detecting OCL Traps in the UML 2.0 Superstructure: An Experience Report. In Thomas Baar, Alfred Strohmeier, Ana Moreira, and Stephen J. Mellor, editors, Proc. 7th Int. Conf. Unified Modeling Language (UML'2004), pages 188-197. Springer, Berlin, LNCS 3273, 2004.
Currently, the OMG is developing a new version of the Unified Modeling Language (UML), UML 2.0, which involves major innovations in its metamodel. As for previous versions of the UML, the Object Constraint Language (OCL) is employed to give restrictions on the use of UML and for the formulation of additional operations. It seems that the OCL expressions in the current version of the UML 2.0 Superstructure have not been checked with a tool. In this paper we report on an experiment in checking and validating the well-formedness rules and operation definitions of the UML 2.0 Superstructure w.r.t. syntax and type checking by using our tool USE (UML-based Specification Environment). For this purpose we classify the errors detected by USE in appropriate error categories. We develop statistical information on error frequencies w.r.t. package location and error category. All errors detected by USE and their detailed description are made available in a separate EXCEL file.
(10 pages, gzipped PostScript: 52kb via HTTP, uncompressed PostScript: 131kb via HTTP)


[Bezivin et al., 2004]
Jean Bezivin, Thomas Baar, Tracy Gardner, Martin Gogolla, Reiner Hähnle, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, and Jos Warmer. OCL and Model Driven Engineering Workshop Report. In Nuno Jardim Nunes, Bran Selic, Alberto Rodrigues da Silva, and Ambrosio Toval Alvarez, editors, UML'2004 Modeling Languages and Applications. UML'2004 Satellite Activities. Revised Selected Papers, pages 67-75. Springer, Berlin, LNCS 3297, 2004.
This paper reports on a workshop held at the 7th UML conference. It describes motivation, objectives, abstracts of the presented papers, questions raised during discussion, and a workshop conclusion.
(9 pages, gzipped PostScript: 31kb via HTTP, uncompressed PostScript: 158kb via HTTP)


[Bisanz et al., 2004]
Stefan Bisanz, Paul Ziemann, and Arne Lindow. Integrated Specification, Validation and Verification with HybridUML and OCL Applied to the BART Case Study. In E. Schnieder and G. Tarnai, editors, Proc. Conf. Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT'2004), 2004.
This article proposes the integration of the HybridUML specification formalism and the USE approach for validation of invariant constraints and verification of system states. The benefit is an executable real-time simulation with an integrated verification/validation component, which combines the advantages of the previously separate approaches by providing an accurate, (partially) time-continuous model that can be checked for consistency between static invariants and dynamical behavior in terms of a complete UML model. The integration is illustrated by means of a train system specification -- the BART case study.
(13 pages, gzipped PostScript: 2325kb via HTTP, uncompressed PostScript: 5587kb via HTTP)


[Büttner and Gogolla, 2004a]
Fabian Büttner and Martin Gogolla. On Generalization and Overriding in UML 2.0. In Jean Bezivin, Thomas Baar, Tracy Gardner, Martin Gogolla, Reiner Hähnle, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, and Jos Warmer, editors, Proc. UML'2004 Workshop OCL and Model Driven Engineering, pages 69-69. In: UML - Modeling Languages and Applications. Nuno Jardim Nunes, Bran Selic, Alberto Rodrigues da Silva, Ambrosio Toval Alvarez (Eds). LNCS 3297, Springer Verlag. Long version: University of Kent, http://www.cs.kent.ac.uk/projects/ocl/oclmdewsuml04/, 2004.
In the upcoming Unified Modeling Language specification (UML 2.0), subclassing (i.e., generalization between classes) has a much more precise meaning with respect to overriding than it had in earlier UML versions. Although it is not expressed explicitly, UML 2.0 has a covariant overriding rule for methods, attributes, and associations. In this paper, we first precisely explain how overriding is defined in UML 2.0. We relate the UML approach to the way types are formalized in programming languages and we discuss which consequences arise when implementing UML models in programming languages. Second, weaknesses of the UML 2.0 metamodel and the textual explanations are addressed and solutions, which could be incorporated with minor efforts are proposed. Despite of these weaknesses we generally agree with the UML 2.0 way of overriding and provide supporting arguments for it.
(15 pages, gzipped PostScript: 155kb via HTTP, uncompressed PostScript: 362kb via HTTP)


[Büttner and Gogolla, 2004b]
Fabian Büttner and Martin Gogolla. Realizing UML Metamodel Transformations with AGG. In Reiko Heckel, editor, Proc. ETAPS Workshop Graph Transformation and Visual Modeling Techniques (GT-VMT'2004). Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, 2004.
In this paper, we work out equivalence transformations on the UML metamodel as concrete graph transformations implemented in the AGG tool. We consider two examples for manipulating the static structure of a UML model, namely the transformation of an association class into a ternary association and the transformation of a ternary association into three binary associations. We discuss technical details and pros and cons of the presented approach and shortly put out work into the context of the MDA.
(12 pages, gzipped PostScript: 560kb via HTTP, uncompressed PostScript: 8829kb via HTTP)


[Büttner et al., 2004]
Fabian Büttner, Oliver Radfelder, Arne Lindow, and Martin Gogolla. Digging into the Visitor Pattern. In Frank Maurer and Günther Ruhe, editors, Proc. IEEE 16th Int. Conf. Software Engineering and Knowlege Engineering (SEKE'2004). IEEE, Los Alamitos, 2004.
In this paper we present an alternative to the visitor pattern, dynamic dispatcher, that can be applied to extend existing software in a nonintrusive way, and which simulates covariant overriding of visit methods. It allows to express polymorphic operations through visitor classes in a more natural way than the original visitor pattern. Our solution dynamic dispatcher can be applied without touching existing domain classes. Therefore, it is especially useful to extend frameworks and libraries. We have implemented dynamic dispatcher as a small framework in Java and conducted performance measurements which show that the overhead should be acceptable in many real world scenarios.
(7 pages, gzipped PostScript: 48kb via HTTP, uncompressed PostScript: 168kb via HTTP)


[Gogolla, 2004a]
Martin Gogolla. (An Example for) Metamodeling Syntax and Semantics of Two Languages, their Transformation, and a Correctness Criterion. In Jean Bezivin and Reiko Heckel, editors, Proc. Dagstuhl Seminar on Language Engineering for Model-Driven Software Development. Schloss Dagstuhl Int. Conf. and Research Center for Computer Science, http://www.dagstuhl.de/04101/, 2004.
We study a metamodel for the Entity Relationship (ER) and the Relational data model. We do this by describing the syntax of the ER data model by introducing classes for ER schemata, entities, and relationships. We also describe the semantics of the ER data model by introducing classes for ER states, instances, and links. The connection between syntax and semantics is established by associations explaining that syntactical objects are interpreted by corresponding semantical objects. Analogously we do this for the Relational data model. Finally, we give a metamodel for the transformation of ER schemata into Relational database schemata. By characterizing the syntax and semantics of the languages to be transformed and also the transformation itself within the same (meta-)modeling language we are able to include equivalence criteria on the syntactical and on the semantical level for the transformation. In particular, we show that the semantical equivalence criterion requires that the ER states and the corresponding Relational states bear the same information.
(10 pages, gzipped PostScript: 134kb via HTTP, uncompressed PostScript: 877kb via HTTP)


[Gogolla, 2004b]
Martin Gogolla. Benefits and Problems of Formal Methods. In Albert Llamosi and Alfred Strohmeier, editors, Proc. 9th Int. Conf. Reliable Software Technologies Ada-Europe (RST'2004), pages 1-15. Springer, Berlin, LNCS 3063, 2004.
Formal methods for software development have been discussed for decades. This paper will try to explain when and under what circumstances formal methods and languages in general and the Object Constraint Language (OCL) in particular can be employed in a beneficial way. The success of using a formal approach is highly influenced by the expectations and pre-requisite knowledge of the developers, the role the formal support in the development process is given, and of course by the used tools.
(15 pages, gzipped PostScript: 83kb via HTTP, uncompressed PostScript: 288kb via HTTP)


[Gogolla and Ziemann, 2004]
Martin Gogolla and Paul Ziemann. Checking BART Test Scenarios with UML's Object Constraint Language. In Fabrice Kordon and Michel Lemoine, editors, Formal Methods for Embedded Distributed Systems - How to master the complexity, pages 133-170. Kluwer, 2004.
The Object Constraint Language (OCL) is part of the Unified Modelling Language (UML). Within software engineering, UML is regarded today as an important step towards development of high-quality object-oriented systems. OCL allows to sharpen UML diagrams through invariants and pre- and postconditions. This chapter explains the functionality of the UML Specification Environment USE, which allows to validate and verify UML and OCL descriptions. The paper shows that central safety properties of the BART system can be expressed with OCL. Test cases embodying central aspects of the BART system can be formulated within the USE system. It can be shown that the safety properties are satisfied by the test cases examined.
(38 pages, gzipped PostScript: 193kb via HTTP, uncompressed PostScript: 1089kb via HTTP)


[Gogolla et al., 2004a]
Martin Gogolla, Mark Richters, Jörn Bohling, Arne Lindow, Fabian Büttner, and Paul Ziemann. Werkzeugunterstützung für die Validierung von UML- und OCL-Modellen durch automatische Snapshot-Generierung. In Bernhard Rumpe and Wolfgang Hesse, editors, Proc. Modellierung'2004, pages 281-282. Gesellschaft für Informatik, LNI P-45, 2004.
Diese Arbeit gibt einen kurzen, aktuellen Überblick zu Bremischen Aktivitäten im Bereich Werkzeugunterstützung für UML und OCL.
(2 pages, gzipped PostScript: 11kb via HTTP, uncompressed PostScript: 25kb via HTTP)


[Gogolla et al., 2004b]
Martin Gogolla, Paul Sammut, and Jon Whittle. Essentials of the 3rd UML Workshop in Software Model Engineering (WiSME'2004). In Nuno Jardim Nunes, Bran Selic, Alberto Rodrigues da Silva, and Ambrosio Toval Alvarez, editors, UML'2004 Modeling Languages and Applications. UML'2004 Satellite Activities. Revised Selected Papers, pages 43-51. Springer, Berlin, LNCS 3297, 2004.
This paper reports on a workshop held at the 7th UML conference. It describes motivation and aims, organisational issues, abstracts of the accepted papers, and questions raised during discussion.
(10 pages, gzipped PostScript: 42kb via HTTP, uncompressed PostScript: 102kb via HTTP)


[Krieg-Brückner et al., 2004]
Bernd Krieg-Brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, and George Russell. Semantic Interrelation of Documents via an Ontology. In Gregor Engels and Silke Seehusen, editors, Proc. 2. Deutsche e-Learning Fachtagung Informatik (DeLFI'2004), pages 271-282. Gesellschaft für Informatik, LNI P-52, 2004.
This paper describes how to use an ontology for extensive semantic interrelation of documents in order to achieve sustainable development, i.e. continuous long-term usability of the contents. The ontology is structured via packages (corresponding to whole documents). Packages are related by import such that semantic interrelation becomes possible not only within a document but also between different documents. Coherence and consistency are enhanced by change management in a repository, including version control and configuration management. Semantic interrelation is realized by particular LaTeX commands for the declaration and definition of classes, objects and relations, and references to them, such that they can be used in standard LaTeX documents, in particular, with a new LaTeX style for educational material (slides, handouts, annotated courses, assignments, and so on).

[Lindow and Gogolla, 2004]
Arne Lindow and Martin Gogolla. Eine multimediale Erweiterung eines UML-Tools für Lehrzwecke. In Gregor Engels and Silke Seehusen, editors, Proc. 2. Deutsche e-Learning Fachtagung Informatik (DeLFI'2004), pages 393-394. Gesellschaft für Informatik, LNI P-52, 2004.
In this paper we discuss possible extensions for an UML/OCL tool so far used in the area of formal methods to expand it to an educational teaching and learning system. So we will show a way to develop USE from a well known tool for practical work in the area of formal methods into an educational multimedia teaching and learning environment, which can be used in lectures and for the creation of lecture material. We clarify, how authors could benefit of a new import-function for the standard interchange format of UML-models. We show how we think, authors of multimedia material for lectures can benefit of easy to create graphical or animated presentations of UML models or new diagram combinations. We suggest an extension for a learner model, which can help the students easily access examples of concepts of UML, which they want to learn. A new annotation mechanism for presentation is suggested and an easy to understand, very detailed visualization of the evaluation of OCL-expressions is explained.
(2 pages, gzipped PostScript: 10kb via HTTP, uncompressed PostScript: 24kb via HTTP)


[Ziemann et al., 2004a]
Paul Ziemann, Karsten Hölscher, and Martin Gogolla. Coherently Explaining UML Statechart and Collaboration Diagrams by Graph Transformations. In Arnaldo Moura and Alexandre Mota, editors, Proc. Brazilian Symposium on Formal Methods (SBMF'2004). Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, 2004.
In this paper we continue our work on the formalization and validation of UML models by means of graph transformation systems. We here concentrate on statechart and collaboration diagrams albeit our approach covers use case, class, object, and sequence diagrams as well. The statechart and collaboration diagrams describe the operations of the underlying class diagram and include OCL expressions as guards and parts of message expressions. We illustrate in detail the generation of graph transformation rules for the statechart and collaboration diagrams.
(15 pages, gzipped PostScript: 178kb via HTTP, uncompressed PostScript: 549kb via HTTP)


[Ziemann et al., 2004b]
Paul Ziemann, Karsten Hölscher, and Martin Gogolla. From UML Models to Graph Transformation Systems. In Mark Minas, editor, Proc. Workshop Visual Languages and Formal Methods (VLFM'2004). Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, 2004.
In this paper we present an approach that allows to validate properties of UML models. The approach is based on an integrated semantics for central parts of the UML. We formally cover UML use case, class, object, statechart, collaboration, and sequence diagrams. Additionally full OCL is supported in the common UML fashion. Our semantics is based on the translation of a UML model into a graph transformation system consisting of graph transformation rules and a working graph that represents the system state. By applying the rules on the working graph, the evolution of the modeled system is simulated.
(16 pages, gzipped PostScript: 267kb via HTTP, uncompressed PostScript: 808kb via HTTP)


[Bezivin and Gogolla, 2003]
Jean Bezivin and Martin Gogolla, editors. Proc. 2nd UML Workshop in Software Model Engineering (WiSME'2003). www.metamodel.com, 2003. http://www.metamodel.com/wisme-2003/.
Model Driven Architecture (MDA) is an OMG initiative that attempts to separate business functionality specification from the implementation of that functionality on specific middleware technological platforms (CORBA, C#/DotNet, Java/EJB, XML/SOAP, etc.). This new approach is intended to play a key role in the fields of information system and software engineering. The stage is thus set but the efforts to move from the present situation to the idyllic automatic generation of executable models for various platforms remains huge. We need to mobilize the creative energies of a very broad category of contributors, from tool builders to theoretical specialists in the fields of language compilers, graph rewriting, model checking, ontology engineering, etc. The workshop brings together young researchers planning to invest in this emerging new area as well as more experienced professional having previous experience in areas related to automatic code generation, transformational and generative approaches, model checking, etc.

[Gogolla and Lindow, 2003]
Martin Gogolla and Arne Lindow. Transforming Data Models with UML. In Borys Omelayenko and Michel Klein, editors, Knowledge Transformation for the Semantic Web, pages 18-33. IOS Press, Amsterdam, Amsterdam, 2003.
This chapter studies an approach to establish a formal connection between data models, in particular between conceptual data models and implementation data models. We use metamodeling techniques based on the Meta Object Facility MOF. MOF may be regarded as a subset of the Unified Modeling Language UML. As prominent example data models, we formally describe and thereby analyze the Entity-Relationship and the Relational data model. In addition, we represent the transformation between these data models by MOF language features. Thus we describe the data models and their transformation within a single framework. All results are formally represented and validated by a MOF compliant tool. The approach presented is general enough so that it can used for other data models being important for the Semantic Web, e.g., the object-oriented data model or semi-structured data models like XML-based models.
(15 pages, gzipped PostScript: 124kb via HTTP, uncompressed PostScript: 1519kb via HTTP)


[Gogolla et al., 2003a]
Martin Gogolla, Jörn Bohling, and Mark Richters. Validation of UML and OCL Models by Automatic Snapshot Generation. In Grady Booch, Perdita Stevens, and Jonathan Whittle, editors, Proc. 6th Int. Conf. Unified Modeling Language (UML'2003), pages 265-279. Springer, Berlin, LNCS 2863, 2003.
We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model.
(15 pages, gzipped PostScript: 113kb via HTTP, uncompressed PostScript: 462kb via HTTP)


[Gogolla et al., 2003b]
Martin Gogolla, Mark Richters, and Jörn Bohling. Tool Support for Validating UML and OCL Models through Automatic Snapshot Generation. In Jarr Eloff, Andries Engelbrecht, Paula Kotze, and Mariki Eloff, editors, Proc. Annual Research Conf. South African Institute of Computer Scientists and Information Technologists on Enablement through Technology (SAICSIT'2003), pages 248-257. ACM International Conference Proceedings Series, 2003.
This paper studies tool support for the testing and certification of UML and OCL models as supported by the validation tool USE. We describe the features available in the UML/OCL tool USE and extend its features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. We explain the functionality offered by the USE tool. In particular, we demonstrate how the diverse windows, e.g., object diagram, class invariant, class extent, or OCL expression evaluation window, support the development process in early phases of software development.
(10 pages, gzipped PostScript: 202kb via HTTP, uncompressed PostScript: 2858kb via HTTP)


[Kollmann, 2003]
Ralf Kollmann. Design Recovery Techniques for Object-Oriented Software Systems. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2003.
Reverse engineering techniques have been applied successfully in software maintenance, reengineering, as well as traditional software engineering processes for many years. With the establishment of the UML as a standard for modeling of object-oriented software systems, many new opportunities but also challenges have opened up in the new field of UML-based reverse engineering. In this dissertation thesis, techniques for application of the UML in static design recovery as well as metric-based static software analysis are presented, with a focus on programs written in Java. To address the problem of uniquely representing aspects of existing programs in UML diagrams, a metamodel for the Java language has been developed. It serves as a foundation for a standardized metamodel-level translation scheme between Java and the UML. Based on this scheme, techniques for recovering the abstract design of a software system from the implementation model are introduced. The focus of these is on design recovery strategies for recognition of advanced UML class diagram features. When reverse engineering non-trivial software systems, the resulting amount of information is often huge. One of the central problems of UML diagrams is the tradeoff between detailed rendering and lack of space and readability: Even for programs of average size, the resulting diagrams tend to become quickly too large for comfortable viewing. In addition to metricbased analysis techniques, which help to understand the software by integrating metrics and UML diagrams, we present a metric-based approach for identification of logical substructures in a software architecture, which helps to partition the system and thus make it easier comprehensible. The techniques presented in this dissertation have been implemented in the reverse engineering tool IDEA, a system for static analysis of Java programs. IDEA supports generation of both UML class as well as activity diagrams from source code. Concerning its primary functionality, static design recovery, it is possible to recognize many of UML s advanced notational features in an interactive process. Furthermore, the calculation of metrics is supported and used both for integration in extended UML class diagrams, as well as for metric-based analyses. The approaches presented in this dissertation thesis contribute to the research field of reverse engineering, by showing novel ways to redocument and analyse object-oriented software systems using the graphical UML notation. Thereby, they help to improve a general understanding of how to apply the UML in reverse engineering and static program analysis.

[Krieg-Brückner et al., 2003]
Bernd Krieg-Brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, Erica Melis, Philipp Meier, Arnd Poetzsch-Heffter, Markus Roggenbach, George Russell, Jan-Georg Smaus, and Martin Wirsing. MultiMedia Instruction in Safe and Secure Systems. In Martin Wirsing, Dirk Pattinson, and Rolf Hennicker, editors, Proc. 16th Int. Workshop Abstract Data Types (WADT'02), pages 82-117. Springer, Berlin, LNCS 2755, 2003.
The aim of the MMiSS project is the construction of a multimedia Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure Systems. Traditional teaching materials (slides, handouts, annotated course material, assignments, and so on) are to be converted into a new hypermedia format, integrated with tool interactions for formally developing correct software; they will be suitable for learning on campus and distance learning, as well as interactive, supervised, or cooperative self-study. To ensure sustainable development, i.e. continuous long-term usability of the contents, coherence and consistency are especially emphasised, through extensive semantic linking of teaching elements and a particular version and configuration management, based on experience in formal software development and associated support tools.
(38 pages, gzipped PostScript: 1452kb via HTTP, uncompressed PostScript: 8909kb via HTTP)


[Radfelder, 2003]
Oliver Radfelder. Dreidimensionale, interaktive und animierte Softwarevisualisierung zur Unterstützung im Softwareentwicklungsprozess. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, 2003.
In Kapitel 1 werden bestehende Ansätze zur Visualisierung untersucht. Dabei werden speziell dreidimensionale und animierte Techniken und Systeme beleuchtet. Weiterhin werden Taxonimien und Evaluierungen der Softwarevisualisierung untersucht, um am Ende einen Kriterienkatalog für effektive Softwarevisualisierung zu entwickeln. In Kapitel 2 wird die UML am exemplarisch im Einsatz eines Softwareentwurfs gezeigt und Kritikpunkte gesammelt und am Ende diskutiert. In Kapitel 3 wird zunächst der Einsatz dreidimensionaler und animierter Softwarevisualisierung statischer Strukturen diskutiert. Während dessen stelle ich die relevanten Teile der zu diesem Zweck entwickelte Software Uvis vor. Kapitel 4 behandelt die Visualisierung dynamischer Vorgänge ebenfalls im Kontext von Uvis. In Kapitel 5 werden die dynamische und die statische Sicht zusammengeführt, wodurch es möglich wird, eine konzeptionelle Gesamtsicht auf ein Modell zu erhalten. Zusätzlich wird in dem Kapitel diskutiert, wie die Integration zweier ansonsten getrennter Sichtweisen durch die dreidimensionale, interaktive und animierte Visualisierung möglich wird: Die Einbettung der Oberflächen-orientierten Sichtweise des zukünftigen Benutzers in die Spezifikations-orientierte Sicht des Modellierers. In Kapitel 6 wird noch einmal die Arbeit zusammengefasst und diskutiert, sowie ein Ausblick auf mögliche weitere Arbeit zu diesem Thema gegeben.

[Richters and Gogolla, 2003]
Mark Richters and Martin Gogolla. Aspect-Oriented Monitoring of UML and OCL Constraints. In Omar Aldawud, Mohamed Kande, Grady Booch, Bill Harrison, Dominik Stein, Jeff Gray, Siobhan Clarke, Aida Zakaria, Peri Tarr, and Faisal Akkawi, editors, Proc. UML'2003 Workshop Aspect-Oriented Software Development with UML. Illinois Institute of Technology, Department of Computer Science, http://www.cs.iit.edu/ oaldawud/AOM/index.htm, 2003.
We present an approach utilizing aspect-oriented programming (AOP) techniques for mapping between di erent abstraction levels of software. The goal is to facilitate validation and testing of a software implementation against constraints specified on an associated UML model. We use AOP techniques for defining a monitor that observes the behavior of an implementation and maps it to model behavior. The model behavior is then validated against constraints with an existing tool. Constraint violations can thus be identified and traced to a specification of the model.
(7 pages, gzipped PostScript: 191kb via HTTP, uncompressed PostScript: 884kb via HTTP)


[Ziemann and Gogolla, 2003a]
Paul Ziemann and Martin Gogolla. An OCL Extension for Formulating Temporal Constraints. Research Report 1/03, Universität Bremen, 2003.
UML class diagrams are widely used to model the static structure of object-oriented software systems. The textual language OCL, which is part of the UML, is used for formulating constraints that can not be modeled by the diagrams. In this paper, we extend OCL with elements of linear temporal logic. With this extended OCL, which we call TOCL, we want to give software engineers a user-friendly means to specify constraints on the temporal evolution of the system structure as well as on the system behavior by stating temporal invariants and pre- and postconditions. We formally define syntax and semantics of the extended OCL.
(20 pages, gzipped PostScript: 179kb via HTTP, uncompressed PostScript: 444kb via HTTP)


[Ziemann and Gogolla, 2003b]
Paul Ziemann and Martin Gogolla. OCL Extended with Temporal Logic. In Manfred Broy and Alexandre Zamulin, editors, 5th Int. Conf. Perspectives of System Informatics (PSI'2003), pages 351-357. Springer, Berlin, LNCS 2890, 2003.
UML class diagrams have become a standard for modeling the static structure of object-oriented software systems. OCL can be used for formulating additional constraints that can not be expressed with the diagrams. In this paper, we extend OCL with temporal operators to formulate temporal constraints.
(7 pages, gzipped PostScript: 110kb via HTTP, uncompressed PostScript: 231kb via HTTP)


[Ziemann and Gogolla, 2003c]
Paul Ziemann and Martin Gogolla. Validating OCL Specifications with the USE Tool - An Example Based on the BART Case Study. In Thomas Arts and Wan Fokkink, editors, Proc. 8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS'2003). Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 80, Elsevier, 2003.
The Object Constraint Language (OCL) is part of the Unified Modeling Language (UML). Within software engineering, UML is regarded today as an important step towards development of high-quality object-oriented systems. OCL allows to sharpen UML diagrams through invariants as well as pre- and postconditions. This paper explains the functionality of the UML Specification Environment USE which allows to validate UML and OCL descriptions. The paper shows that central safety properties of the train system described in the well-known BART case study can be expressed with OCL. Test cases embodying central aspects of this train system can be formulated within the USE system. It can be shown that the safety properties are satisfied by the test cases examined.
(13 pages, gzipped PostScript: 188kb via HTTP, uncompressed PostScript: 695kb via HTTP)


[Gogolla, 2002]
Martin Gogolla. Editorial for the Special Issue on the UML 2001 Conference. Software and System Modeling (SoSyM), 1(2):83-85, 2002.
This paper is the editorial for the special issue of the journal on Software and Systems Modeling dedicated to the UML 2001 Conference (UML'2001)

[Gogolla and Henderson-Sellers, 2002]
Martin Gogolla and Brian Henderson-Sellers. Formal Analysis of UML Stereotypes within the UML Metamodel. In Steve Cook, Heinrich Hussmann, and Jean-Marc Jezequel, editors, Proc. 5th Int. Conf. Unified Modeling Language (UML'2002), pages 84-99. Springer, Berlin, LNCS 2460, 2002.
Stereotypes are a powerful and potentially expressive extension mechanism in the Unified Modeling Language UML. However, it seems that stereotypes are difficult to handle because using stereotypes needs an understanding of the UML metamodel and in particular an understanding of OCL constraints. Stereotypes are often applied in a wrong or at least sloppy way without proper declaration. There are also differences between the various versions of UML with respect to subtle details in the stereotype part. A graphical syntax for stereotypes including examples has been introduced only late in UML 1.4. Other difficulties are that constraints are used in the stereotype context in two completely different ways and that no full support of stereotypes is offered by tools yet. The paper points out these difficulties in detail, analyses the UML metamodel part dealing with stereotypes, and makes various suggestions to improve the definition and use of stereotypes.
(15 pages, gzipped PostScript: 235kb via HTTP, uncompressed PostScript: 3535kb via HTTP)


[Gogolla and Richters, 2002]
Martin Gogolla and Mark Richters. Development of UML Descriptions with USE. In Hassan Shafazand and A Min Tjoa, editors, Proc. 1st Eurasian Conf. Information and Communication Technology (EURASIA'2002), pages 228-238. Springer, Berlin, LNCS 2510, 2002.
The Object Constraint Language OCL is part of the Unified Modeling Language UML. Within software engineering, UML is regarded today as an important step towards development of high-quality object-oriented systems. OCL allows to describe system structure by invariants and system behavior by pre- and postconditions. This paper explains the functionality of the UML Specification Environment USE which allows to validate and verify UML and OCL descriptions. The paper also uses a new approach to handle UML statecharts by OCL pre- and postconditions.
(12 pages, gzipped PostScript: 196kb via HTTP, uncompressed PostScript: 5467kb via HTTP)


[Gogolla et al., 2002a]
Martin Gogolla, Arne Lindow, Mark Richters, and Paul Ziemann. Metamodel Transformation of Data Models. In Jean Bezivin and Robert France, editors, Proc. UML'2002 Workshop in Software Model Engineering (WiSME 2002). http://www.metamodel.com/wisme-2002, 2002.
This paper studies syntax and semantics of the Entity-Relationship (ER) and Relational data model and their transformation. The ER model may be regarded as a platform independent model and the Relational model as a prototypical platform specific model. The paper studies the transformation between these models and proposes to express that transformation again as a model.
(8 pages, gzipped PostScript: 124kb via HTTP, uncompressed PostScript: 947kb via HTTP)


[Gogolla et al., 2002b]
Martin Gogolla, Paul Ziemann, and Sabine Kuske. Towards an Integrated Graph Based Semantics for UML. In Paolo Bottoni and Mark Minas, editors, Proc. ICGT Workshop Graph Transformation and Visual Modeling Techniques (GT-VMT'2002). Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 72, No. 3, Elsevier, 2002.
Recently, we proposed an integrated formal semantics based on graph transformation for central aspects of UML class, object and state diagrams. In this paper, we explain the basic ideas of that approach and show how two more UML diagram types, sequence and collaboration diagrams, can be captured. For UML models consisting of a class diagram and particular state diagrams, a graph transformation system can be defined. Its graphs are associated with system states and its rules with operations in the class diagram and transitions in the state diagrams. Sequence and collaboration diagrams then characterize sequences of operation applications and therefore sequences of transformation rule applications. Thus valid sequence and collaboration diagrams correspond to derivations induced by the graph transformation system. Proceeding this way, it can be checked for example whether such an operation application sequence may be applied in a specific system state.
(16 pages, gzipped PostScript: 95kb via HTTP, uncompressed PostScript: 328kb via HTTP)


[Kollmann and Gogolla, 2002]
Ralf Kollmann and Martin Gogolla. Metric-Based Selective Representation of UML Diagrams. In Tibor Gyimóthy and Fernando Brito e Abreu, editors, Proc. 6th European Conf. Software Maintenance and Reengineering (CSMR'02). IEEE, Los Alamitos, 2002.
UML diagrams are widely employed for modeling of object-oriented software systems. In addition to their application in forward engineering, it is also possible to use them for the redocumentation of existing programs. However, the inherent structure of UML diagrams, which consists of graphical as well as textual information, makes it difficult to read and oversee large diagrams generated from complex systems. The view on such diagrams can be compared with taking a look at a detailed map: the reader has to decide whether to read the fine details or to view the whole structure. We present approaches to overcome this problem by using object-oriented metrics for program analysis and location of submodules in diagrams that belong together in terms of coupling. The shown techniques have been implemented into our reverse engineering tool Idea, which allows interactive selection and isolation of coherent regions of class diagrams.
(10 pages, gzipped PostScript: 295kb via HTTP, uncompressed PostScript: 1929kb via HTTP)


[Kollmann et al., 2002]
Ralf Kollmann, Petri Selonen, Eleni Stroulia, Tarja Systä, and Albert Zündorf. A Study on the Current State of the Art in Tool-Supported UML-Based Static Reverse Engineering. In Elizabeth Burd and Arie van Deursen, editors, Proc. 9th Working Conf. Reverse Engineering (WCRE'02). IEEE, Los Alamitos, 2002.
Today, software-engineering research and industry alike recognize the need for practical tools to support reverse-engineering activities. Most of the well-known CASE-tools nowadays support reverse engineering in some way. But although the Unified Modeling Language (UML) has emerged as the de facto standard for the abstract graphical representation of object-oriented software systems, there does not yet exist a standard scheme for representing the reverse engineered models of software systems. Due to the differences in understanding and application of the UML notation and the proprietary extensions that different tools adopt, it is often difficult to ensure that model semantics remains unambiguous when working with different tools at the same time. In this paper, we examine the capabilities of the two most successful industrial-strength CASE-tools in reverse engineering the static structure of software systems and compare them to the results produced by two academic prototypes. The comparisons are carried out both manually and automatically using a research prototype for manipulating and comparing UML models.
(11 pages, gzipped PostScript: 48kb via HTTP, uncompressed PostScript: 391kb via HTTP)


[Kuske et al., 2002]
Sabine Kuske, Martin Gogolla, Ralf Kollmann, and Hans-Jörg Kreowski. An Integrated Semantics for UML Class, Object, and State Diagrams based on Graph Transformation. In Michael Butler and Kaisa Sere, editors, 3rd Int. Conf. Integrated Formal Methods (IFM'02), pages 11-28. Springer, Berlin, LNCS 2335, 2002.
This paper studies the semantics of a central part of the Unified Modeling Language UML. It discusses UML class, object and state diagrams and presents a new integrated semantics for both on the basis of graph transformation. Graph transformation is a formal technique having some common ideas with the UML. Graph transformation rules are associated with the operations in class diagrams and with the transitions in state diagrams. The resulting graph transformations are combined into one system in order to obtain a single coherent semantic description.
(19 pages, gzipped PostScript: 109kb via HTTP, uncompressed PostScript: 494kb via HTTP)


[Richters, 2002]
Mark Richters. A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, Logos Verlag, Berlin, BISS Monographs, No. 14, 2002.
We present a precise approach that allows an analysis and validation of UML models and OCL constraints. We focus on models and constraints specified in the analysis and early design stage of a software development process. For this purpose, a suitable subset of UML corresponding to information that is usually represented in class diagrams is identified and formally defined. This basic modeling language provides a context for all OCL constraints. We define a formal syntax and semantics of OCL types, operations, expressions, invariants, and pre-/postconditions. We also give solutions for problems with the current OCL definition and discuss possible extensions. A metamodel for OCL is introduced that defines the abstract syntax of OCL expressions and the structure of types and values. The metamodel approach allows a seamless integration with the UML metamodeling architecture and makes the benefits of a precise OCL definition easier accessible. The OCL metamodel also allows to define context-sensitive conditions for well-formed OCL expressions more precisely. These conditions can now be specified with OCL whereas they previously were specified only informally. % In order to demonstrate the practical applicability of our work, we have realized substantial parts of it in a tool supporting the validation of models and constraints. Design specifications can be ``executed'' and animated thus providing early feedback in an iterative development process. Our approach offers novel ways for checking user data against specifications, for automating test procedures, and for checking CASE tools for standards conformance. Therefore, this work contributes to the goal of improving the overall quality of software systems by combining theoretical and practical techniques.

[Wang et al., 2002]
Rui-Jin Wang, Hui-Chuan Duan, and Martin Gogolla. Unified Modeling Language and Its Application to Modeling. Application Research of Computers, 19(8):80-84, 2002. ISSN 1001-3695.
In the present paper we introduced briefly the main concepts of the Unified Modeling Language (UML), concentrating on the nine kinds of diagrams. In order to show a clue to the application of the UML, we built a simple model for the sales management system in a supermarket using the UML.
(5 pages, gzipped PostScript: 1269kb via HTTP, uncompressed PostScript: 3558kb via HTTP)


[Ziemann and Gogolla, 2002]
Paul Ziemann and Martin Gogolla. An Extension of OCL with Temporal Logic. In Jan Jürjens, editor, Proc. UML'2002 Workshop Critical System Development (CSD 2002). Technical Report, Technical University of Munich, 2002.
UML class diagrams are widely used to model the static structure of object-oriented software systems. As a supplement, OCL becomes more and more popular for formulating constraints that can not be modeled by the diagrams. In this paper, we extend OCL with elements of temporal logic. With this extension, constraints on the temporal development of the system structure as well as on the system behavior can be stated in terms of temporal invariants and pre- and postconditions.
(10 pages, gzipped PostScript: 139kb via HTTP, uncompressed PostScript: 295kb via HTTP)


[Barbier et al., 2001]
Franck Barbier, Brian Henderson-Sellers, Andreas Opdahl, and Martin Gogolla. The Whole-Part Relationship in Object-Oriented Modeling. In Keng Siau and Terry Halpin, editors, Unified Modeling Language: Systems Analysis, Design, and Development Issues, pages 186-209. Idea Group Publishing, Hershey (PA), USA, 2001.
This study of the semantics of the Whole-Part relationship in OO modelling is based on previous detailed analysis of the semantics of UML's Aggregation and Composition (white and black diamonds). Although UML is nowadays a standard and an intensively used OO modelling language, the way the Whole-Part is formalised is unsatisfactory. In this respect, we provide a complete specification by using OCL (Object Constraint Language). This is based on a separation between primary characteristics assigned to the ``Whole-Part'' metatype, considered as necessary in the metamodel of UML, and secondary features possessed by subtypes of this metatype. This UML-compliant style of specification, based on the use of OCL as well as metamodelling, allows us to directly incorporate our results into the metamodel, in particular to revise UML's definition of Composition.
(20 pages, gzipped PostScript: 414kb via HTTP, uncompressed PostScript: 1058kb via HTTP)


[Gogolla, 2001a]
Martin Gogolla. Formal Methods versus UML's OCL. In Stefan Jähnichen, Jeff Kramer, Michel Lemoine, and Martin Wirsing, editors, Can Formal Methods Cope with Software-Intensive Systems, pages 19-20. Dagstuhl-Seminar-Report 308, 2001.
The talk explains the connection between the Unified Modeling Language UML and its Object Constraint Language OCL. It shows OCL features by considering the BART case study and giving a small abstract specification for it. This specification is animated by means of the UML Specification Environment USE developed at University of Bremen. Finally the talk discusses to what extent OCL is different from existing formal specification languages.
(2 pages, gzipped PostScript: 60kb via HTTP, uncompressed PostScript: 1314kb via HTTP)


[Gogolla, 2001b]
Martin Gogolla. Using OCL for Defining Precise, Domain-Specific UML Stereotypes. In Aybuke Aurum and Ross Jeffery, editors, Proc. 6th Australian Workshop on Requirements Engineering (AWRE'2001), pages 51-60. Centre for Advanced Software Engineering Research (CAESER), University of New South Wales, Sydney, 2001.
This paper studies the extension mechanisms of the Unified Modeling Language UML. It introduces a new appproach for defining UML stereotypes and shows its usefulness by considering domain-specific requirements for databases. The stereotypes introduced possess a precise meaning by translating them into expressions formulated in the Object Constraint Language OCL. Apart from proposing a general framework for stereotype definition, this work is also one step in the development of a domain-specific requirements language for information systems.
(10 pages, gzipped PostScript: 98kb via HTTP, uncompressed PostScript: 349kb via HTTP)


[Gogolla and Kobryn, 2001]
Martin Gogolla and Cris Kobryn, editors. Proc. 4th Int. Conf. Unified Modeling Language (UML'2001). Springer, Berlin, LNCS 2185, 2001.
This book contains the papers accepted for the 4th International Conference on the Unified Modeling Language (UML'2001).

[Gogolla and Richters, 2001]
Martin Gogolla and Mark Richters. Expressing UML Class Diagrams Properties with OCL. In Tony Clark and Jos Warmer, editors, Advances in Object Modelling with the OCL, pages 86-115. Springer, Berlin, LNCS 2263, 2001.
The Unified Modeling Language UML is a complex language offering many modeling features. Especially the description of static structures with class diagrams is supported by a rich set of primitives. This paper shows how to transfrom UML class diagrams involving cardinality constraints, qualifiers, association classes, aggregations, compositions, and generalizations into equivalent UML class diagrams employing only binary associations and OCL constraints. Thus we provide a better understanding of UML features. By reducing more complex features in terms of basic ones, we suggest an easy way users can gradually extend the set of UML elements they commonly apply in the modeling process.
(29 pages, gzipped PostScript: 96kb via HTTP, uncompressed PostScript: 747kb via HTTP)


[Kollmann and Gogolla, 2001a]
Ralf Kollmann and Martin Gogolla. Application of the UML Associations and Their Adornments in Design Recovery. In Peter Aiken and Elizabeth Burd, editors, Proc. 8th Working Conference on Reverse Engineering (WCRE'2001). IEEE, Los Alamitos, 2001.
Many CASE tools support reverse engineering and UML. However, it can be observed that usually, only a subset of the UML notation is supported, namely those parts with a more or less direct code representation. Although a lot of research is done in this field, the more advanced features of UML notations are not commonly supported in reverse engineering. In this paper, we show approaches to discover patterns in program code that can be represented by means of advanced notational features of UML class diagrams. We obtain the necessary information by reverse engineering Java programs with different methods. These have been implemented in a prototypical implementation.
(10 pages, gzipped PostScript: 53kb via HTTP, uncompressed PostScript: 163kb via HTTP)


[Kollmann and Gogolla, 2001b]
Ralf Kollmann and Martin Gogolla. Capturing Dynamic Program Behaviour with UML Collaboration Diagrams. In Pedro Sousa and Jürgen Ebert, editors, Proc. 5th European Conf. Software Maintenance and Reengineering (CSMR'01), pages 58-67. IEEE, Los Alamitos, 2001.
The UML provides means to specify both static and dynamic aspects of object-oriented software systems and can be used to assist in all phases of a software development process. With growing support by CASE tools, its applications become more and more widespread. In addition to the automatic generation of class code from diagrams, the recovery of static structure from source code has become common, too. In this paper however, we focus on the extraction of behavioural information from program code. We introduce a restricted meta model for Java code and present a new approach to extract the required data, which will then be rendered as UML collaboration diagrams.
(10 pages, gzipped PostScript: 37kb via HTTP, uncompressed PostScript: 137kb via HTTP)


[Kollmann and Gogolla, 2001c]
Ralf Kollmann and Martin Gogolla. Selektive Darstellung von Programmstrukturen mit UML. In Jürgen Ebert and Franz Lehner, editors, Proc. 3. Workshop Software-Reengineering. Universität Koblenz, Technischer Bericht, http://www.uni-koblenz.de/ ist/WSR2001, 2001.
Das Papier beschreibt, wie verschiedene Ansätze zur Selektion und Transformation von durch Reverse Engineering gesammelten Informationen dazu beitragen können, die Menge der durch Programmcode gegebenen Informationen in komprimierter Weise darzustellen, um Lesbarkeit und Verständnis zu erleichtern. Wir unterscheiden zwischen Abstraktion, wobei komplexere Elemente der UML Notation von Klassendiagrammen zum Einsatz kommen, und selektiver Darstellung, wobei die Transformation der Daten mit einer manuellen Selektion kombiniert wird. Beim Einsatz dieser Techniken hat sich gezeigt, daß durch die kombinierte Herangehensweise bessere Ergebnisse erreicht werden können.
(6 pages, gzipped PostScript: 54kb via HTTP, uncompressed PostScript: 133kb via HTTP)


[Lindow et al., 2001]
Arne Lindow, Martin Gogolla, and Mark Richters. Ein formal validiertes Metamodell für die Transformation von Schemata in Informationssystemen. In K. Bauknecht, W. Brauer, and T. Mück, editors, Proc. GI Jahrestagung (GI'2001), Band 1, Workshop Integrating Diagrammatic and Formal Specification Techniques, pages 662-669. Austrian Computer Society, Wien, 2001.
Dieses Papier stellt eine Verbindung von klassischen Datenmodellen wie dem Entity-Relationship-Modell und dem relationalen Modell mit dem Metamodellierungsansatz der Meta-Object-Facility her. Es wird eine Modellierung sowohl für das ER-Modell als auch für das relationale Modell vorgestellt. Ergänzend wird die Transformation von Entity-Relationship-Schemata in relationale Schemata diskutiert. Alle drei Ebenen werden formal spezifiziert und mit einem Werkzeug validiert.
(8 pages, gzipped PostScript: 111kb via HTTP, uncompressed PostScript: 3854kb via HTTP)


[Richters and Gogolla, 2001]
Mark Richters and Martin Gogolla. OCL - Syntax, Semantics and Tools. In Tony Clark and Jos Warmer, editors, Advances in Object Modelling with the OCL, pages 43-69. Springer, Berlin, LNCS 2263, 2001.
The Object Constraint Language OCL allows to formally specify constraints on a UML model. We present a formal syntax and semantics for OCL based on set theory including expressions, invariants and pre- and postconditions. A formal foundation for OCL makes the meaning of constraints precise and helps to eliminate ambiguities and inconsistencies. A precise language de nition is also a prerequisite for implementing CASE tools providing enhanced support for UML models and OCL constraints. We give a survey of some OCL tools and discuss one of the tools in some more detail. The design and implementation of the USE tool supporting the validation of UML models and OCL constraints is based on the formal approach presented in this paper.
(27 pages, gzipped PostScript: 135kb via HTTP, uncompressed PostScript: 524kb via HTTP)


[Warmer et al., 2001]
Jos Warmer, Anneke Kleppe, Tony Clark, Anders Ivner, Jonas Högström, Martin Gogolla, Mark Richters, Heinrich Hussmann, Steffen Zschaler, Simon Johnston, David S. Frankel, and Conrad Bock. Object Constraint Language 2.0. Technical report, Submission to the OMG, 2001.
This paper is a submission in response to the UML 2.0 OCL request for proposals. It proposes syntax and semantics of a new version of the Object Constraint Language OCL.
(155 pages, gzipped PostScript: 889kb via HTTP, uncompressed PostScript: 4317kb via HTTP)


[Gärtner, 2000]
Heino Gärtner. Schematransformationen in objektorientierten Informationssystemen. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, Shaker Verlag, Aachen, 2000.
Die vorliegende Arbeit konzentriert sich auf die Untersuchung der vertikalen Schemaevolution und geht dabei wie folgt vor: Nachdem im folgenden Abschnitt die benötigten Grundbegriffe aus dem Bereich der konzeptionellen Modellierung und der Schemaevolution geklärt worden sind, folgt zunächst die Präsentation eines einfachen Objektmodells, das im wesentlichen die Konzepte des ER-Modells umfaßt. Danach werden die Grundlagen von Schematransformation diskutiert und eine formal begründete Notation zur Beschreibung von atomaren Schemaänderungsoperationen, Schematransformationsprimitiven, vorgestellt. Mit Hilfe dieser Notation werden zunächst Transformationen auf den Konstrukten des einfachen Objektmodells beschrieben. Danach wird das einfache Objektmodell schrittweise um weitergehende Konzepte erweitert und deren Transformationsmöglichkeiten in dem präsentierten Rahmen diskutiert. Im darauf folgenden Abschnitt werden schließlich Transformationen von Spezifikationsanteilen, die über die Modellierung struktureller Information hinausgehen, am Beispiel von Objektlebensläufen erläutert. Im vorletzten Abschnitt wird die Perspektive der Spezifikation verlassen und erörtert, wie sich der vorgestellte Ansatz in den Softwareentwicklungsprozeß integrieren läßt. Eine Einordnung in die bisherige Forschung und ein Ausblick auf künftige Entwicklungsmöglichkeiten beschließt die Arbeit.

[Gogolla, 2000]
Martin Gogolla. Graph Transformations on the UML Metamodel. In Jose D.P. Rolim, Andrei Z. Broder, Andrea Corradini, Roberto Gorrieri, Reiko Heckel, Juraj Hromkovic, Ugo Vaccaro, and Joe B. Wells, editors, Proc. ICALP Workshop Graph Transformations and Visual Modeling Techniques (GTVMT'2000), pages 359-371. Carleton Scientific, Waterloo, Ontario, Canada, 2000.
The Unified Modeling Language UML is a rich language so that it seems not feasible to give a single semantics for the complete language in one step. In order to define the semantics, we propose to translate as many UML language features as possible into UML itself. The part of UML which cannot be treated in this way is called the UML core. The semantics of the non-core language features is given by a translation into the core, whereas a different semantics (for example a set-theoretic one or a semantics on the basis of graphs) must be given to the UML core. It turns out that for the first step, namely the translation of UML language features into the UML core, graph transformations are an ideal language for expressing the required manipulations and the UML metamodel gives the necessary fundamental vocabulary and notions.
(13 pages, gzipped PostScript: 91kb via HTTP, uncompressed PostScript: 371kb via HTTP)


[Gogolla and Kollmann, 2000]
Martin Gogolla and Ralf Kollmann. Re-Documentation of Java with UML Class Diagrams. In Eliot Chikofsky, editor, Proc. 7th Reengineering Forum, Reengineering Week 2000 Zürich, pages REF 41-REF 48. Reengineering Forum, Burlington, Massachusetts, 2000.
This paper describes the generation of class diagrams characterizing the static data and class structure of Java source code. To achieve such a diagrammatic representation, translation rules are defined that transform Java syntax into UML notation. Attention is paid especially to implicit and advanced properties of associations. First, an implementation view class diagram of the Java source code is generated that reflects program-specific details of the source code. In a second, more involved step, we try to create a design view from the source code and also represent certain patterns as ODMG language features. The focus of our approach is on minimizing the resulting UML diagrams (minimal with respect to the number of elements in the diagrams) by recognizing certain patterns in the source code and transforming certain low-level syntactic constructs into high-level semantic UML features.
(9 pages, gzipped PostScript: 67kb via HTTP, uncompressed PostScript: 199kb via HTTP)


[Gogolla and Richters, 2000]
Martin Gogolla and Mark Richters. Definition von UML mit UML und OCL: Ein Überblick zum Stand der Technik. In Mario Jeckle, Bernhard Rumpe, Andy Schürr, and Andreas Winter, editors, Proc. 7. GROOM-Workshop ``UML - Erweiterungen (Profile) und Konzepte der Metamodellierung''. Universität Koblenz-Landau, Fachbereich Informatik, 2000. Auch: Softwaretechnik-Trends, 20:2, 2000, ISSN 0720-8928.
Das Ziel dieser Arbeit ist es, einen Überblick zum Einsatz der Object Constraint Language OCL zum einen bei der Beschreibung von Modellen mit der Unified Modeling Language UML und zum anderen bei der Beschreibung des UML-Metamodells zu vermitteln. Eingang in die Überlegungen finden die Dokumente des UML-Standards, eigene Arbeiten und weitere Papiere anderer Arbeitsgruppen.
(2 pages, gzipped PostScript: 17kb via HTTP, uncompressed PostScript: 38kb via HTTP)


[Gogolla et al., 2000]
Martin Gogolla, Oliver Radfelder, Ralf Kollmann, and Mark Richters. Analysing Atomic Dynamic UML Notions by Surfing through the UML Metamodel. In Gianna Reggio, Alexander Knapp, Bernhard Rumpe, Bran Selic, and Roel Wieringa, editors, Proc. UML'00 Workshop Dynamic Behaviour in UML Models, pages 57-62. LMU München, Informatik-Bericht Nr. 0006, 2000.
This paper analyses atomic notions in UML which are fundamental for the understanding of dynamic aspects. The notions considered are: Action, Event, Exception, Message, Method, Signal, Stimulus, Operation, and Reception. We surf through the UML metamodel by combining the different metamodel class diagrams, where these notions are defined, into a single class diagram. Thereby we point out the intent, similarities and differences between these notions. Thus before doing a formalization, we try to make the concepts a bit clearer than they appear in the UML Semantics document.
(6 pages, gzipped PostScript: 44kb via HTTP, uncompressed PostScript: 153kb via HTTP)


[Huge, 2000]
Anne Kathrin Huge. Formalisierung objektorientierter Datenbanken auf der Grundlage von ODMG. PhD thesis, Universität Bremen, Fachbereich Mathematik und Informatik, Shaker Verlag, Aachen, 2000.
Die Untersuchung objektorientierter Methoden zeigt, daß die Bereitstellung einer formalen Grundlage ein häufiges Problem ist. Dabei stellt gerade eine formale Grundlage die Basis für ein eingehendes Verständnis der Semantik von Modellierungs- und Spracheigenschaften dar. Ein vergleichender Rückblick auf die generelle Entwicklung von Datenbanken ergibt, daß sich insbesondere das relationale Datenbankmodell auf eine wohldefinierte formale Grundlage stützt und somit den weitreichenden Erfolg relationaler Datenbanksysteme (inklusive SQL) begründet. Ausgehend von diesen Beobachtungen wird in dieser Arbeit eine formale Grundlage für objektorientierte Datenbanken auf der Grundlage des ODMG-Standards vorgestellt. Der ODMG-Standard vereinheitlicht die Konzepte objektorientierter Datenbanken und ermöglicht Portabilität. Um die Lücke zwischen der informellen Beschreibung von ODMG-Sprachkonstrukten und den theoretischen Grundlagen zu schließen, wird in dieser Arbeit ein mengentheoretischer Ansatz zur Beschreibung des ODMG-Objektmodells und der Anfragesprache OQL vorgestellt. Nach einer eher informellen Vorstellung der Konzepte des ODMG-Modells und deren Einbettung in die allgmeinen Konzepte objektorientierter Datenbanken und anschließender vergleichenden Darstellung mit anderen objektorientierten Datenmodellen und Modellierungssprachen wird eine formale Beschreibung des ODMG-Modells und der OQL vorgenommen. Die Formalisierung beruht auf einem Zwei-Schichten-Ansatz, wonach zwischen einer Datenschicht und einer Objektebene differenziert wird. Auf dies Weise erfolgt eine strikte Trennung zwischen unveränderlichen Datentypen und veränderlichen Objekttypen. Um eine konsistente Implementierung einer ODMG-Objektmodell-Spezifikation in einer der Sprachanbindungen (C++, Smalltalk, Java) zu gewährleisten, wird eine Transformation der Konstrukte des ODMG-Modells auf die entsprechenden Konstrukte der Sprachanbindungen vorgestellt.

[Radfelder and Gogolla, 2000]
Oliver Radfelder and Martin Gogolla. On Better Understanding UML Diagrams through Interactive Three-Dimensional Visualization and Animation. In Vito Di Gesu, Stefano Levialdi, and Laura Tarantino, editors, Proc. Advanced Visual Interfaces (AVI'2000), pages 292-295. ACM Press, New York, 2000.
Different approaches support the construction of software by representing certain aspects of a system graphically. Recently, the UML has become common to provide software designers with tools, in which they can create visual representations of software interactively. But the UML is intended to be drawn on two-dimensional surfaces. Our approach extends UML into a third and fourth dimension in a way that we can place both static and dynamic aspects in one single view. By this, we can show behavior in the context of structural aspects, instead of drawing different diagrams for each aspect with only loose relation to each other. We also use the third dimension to emphasize important things and to place less interesting things in the background. Thereby, we direct the viewer's attention to the important things in the foreground. Currently, UML shows dynamic behavior by diagrams which do not change and are therefore static in nature. In sequence diagrams, for example, time elapses from the top of the diagram to the bottom. We point out that behavior is better visualized by animated diagrams where message symbols move from the sender object to the receiver object. Our approach supports the creation of a system as well as the communication of its dynamic processes especially to customers.
(4 pages, gzipped PostScript: 526kb via HTTP, uncompressed PostScript: 851kb via HTTP)


[Radfelder et al., 2000]
Oliver Radfelder, Martin Gogolla, and Volker Behr. Entwurf und Implementierung eines Internet-basierten Material-Informationssystems. Interner Bericht, Universität Bremen, Fachbereich 3, 2000.
Das Projekt Material-Informationssystem hatte das Ziel, ein System zu entwickeln, mit dem Personen und Institutionen aus dem Bereich Verbundwerkstoffe auf einen gemeinsamen Produktdatenbestand zugreifen können. Wir haben ein System entwickelt, das den Zugriff über das Internet ermöglicht. Als Benutzungsschnittstelle wird lediglich ein Webbrowser vorausgesetzt anstatt eine vollständige Applikation auf den Rechnern der Teilnehmer zu installieren. Während der ersten Projektphase wurden die Anforderungen an ein solches neues System analysiert und ein Prototyp entworfen und implementiert. In der zweiten Projektphase wurde das System als Server mit Hilfe von SQL und Java implementiert.
(28 pages, gzipped PostScript: 319kb via HTTP, uncompressed PostScript: 969kb via HTTP)


[Richters and Gogolla, 2000a]
Mark Richters and Martin Gogolla. Validating UML Models and OCL Constraints. In Andy Evans and Stuart Kent, editors, Proc. 3rd Int. Conf. Unified Modeling Language (UML'2000), pages 265-277. Springer, Berlin, LNCS 1939, 2000.
The UML has been widely accepted as a standard for modeling software systems and is supported by a great number of CASE tools. However, UML tools often provide only little support for validating models early during the design stage. Also, there is generally no substantial support for constraints written in the Object Constraint Language (OCL). We present an approach for the validation of UML models and OCL constraints that is based on animation. The USE tool (UML-based Specification Environment) supports developers in this process. It has an animator for simulating UML models and an OCL interpreter for constraint checking. Snapshots of a running system can be created, inspected, and checked for conformance with the model. As a special case study, we have applied the tool to parts of the UML 1.3 metamodel and its well-formedness rules. The tool enabled a thorough and systematic check of the OCL well-formedness rules in the UML standard.
(13 pages, gzipped PostScript: 90kb via HTTP, uncompressed PostScript: 377kb via HTTP)


[Richters and Gogolla, 2000b]
Mark Richters and Martin Gogolla. Validierung von UML-Modellen und OCL-Bedingungen. In Martin Wirsing, Martin Gogolla, Hans-Jörg Kreowski, Tobias Nipkow, and Wolfgang Reif, editors, Proc. GI'2000 Workshop Rigorose Entwicklung software-intensiver Systeme, pages 21-32. LMU München, Informatik-Bericht Nr. 0005, 2000.
Die Unified Modeling Language (UML) ist ein allgemein akzeptierter Standard für die Modellierung von Software-Systemen und wird als solcher von einer großen Anzahl von CASE-Tools unterstützt. Oft weisen UML-Werkzeuge nur wenig Unterstützung für die Validierung von Modellen in frühen Entwurfsphasen auf. Es gibt im allgemeinen auch keine nennenswerte Unterstützung für Integritätsbedingungen, die in der Object Constraint Language (OCL) geschrieben sind. Wir stellen daher einen Ansatz für die Validierung von UML-Modellen und OCL-Bedingungen vor, der diese Unterstützung bereitstellt. Das USE-Werkzeug (UML-based Specification Environment) bietet einen Animator zum Simulieren von UML-Modellen und einen OCL-Interpreter für die überprüfung von Bedingungen. Einzelne Zustände eines laufenden Systems können untersucht und auf übereinstimmung mit dem Modell überprüft werden.
(12 pages, gzipped PostScript: 83kb via HTTP, uncompressed PostScript: 328kb via HTTP)


[Astesiano et al., 1999]
Egidio Astesiano, Andy Evans, Robert France, Guy Geniloud, Martin Gogolla, Brian Henderson Sellers, John Howse, Heinrich Hussmann, Shusaku Iida, Stuart Kent, Alain Le Guennec, Tom Mens, Richard Mitchell, Oliver Radfelder, Gianna Reggio, Mark Richters, Bernhard Rumpe, Perdita Stevens, Klaas van den Berg, Pim van den Broek, and Roel Wieringa. UML Semantics FAQ. In Ana Moreira and Serge Demeyer, editors, ECOOP'99 Workshop Reader, pages 33-56. Springer, Berlin, LNCS 1743, 1999.
This paper reports the results of a workshop held at ECOOP'99. The workshop was set up to find answers to questions fundamental to the definition of a semantics for the Unified Modelling Language. Questions examined the meaning of the term semantics in the context of UML; approaches to defining the semantics, including the feasibility of the meta-modelling approach; whether a single semantics is desirable and, if not, how to set up a framework for defining multiple, interlinked semantics; and some of the outstanding problems for defining a semantics for all of UML.
(25 pages, gzipped PostScript: 952kb via HTTP, uncompressed PostScript: 5795kb via HTTP)


[Gogolla, 1999]
Martin Gogolla. Identifying Objects by Declarative Queries. In Mike P. Papazoglou, Stefano Spaccapietra, and Zahir Tari, editors, Advances in Object-Oriented Data Modeling, pages 255-277. MIT Press, 1999.
Object identification in data models, especially in semantic, Entity-Relationship, and Object-Oriented data models is studied. Various known approaches to object identification are shown, and an alternative proposal to the topic is put forward. The main new idea is to attach to each object type an arbitrary query, a so-called observation term, in order to observe a unique, identifying property of objects of the corresponding type.
(25 pages, gzipped PostScript: 138kb via HTTP, uncompressed PostScript: 682kb via HTTP)


[Gogolla and Richters, 1999]
Martin Gogolla and Mark Richters. Transformation Rules for UML Class Diagrams. In Jean Bezivin and Pierre-Alain Muller, editors, Proc. 1st Int. Workshop Unified Modeling Language (UML'98), pages 92-106. Springer, Berlin, LNCS 1618, 1999.
UML is a complex language with many modeling features. Especially the modeling of static structures with class diagrams is supported by a rich set of description primitives. We show how to transfrom UML class diagrams involving cardinality constraints, qualifiers, association classes, aggregations, compositions, and generalizations into equivalent UML class diagrams employing only n-ary associations and OCL constraints. This provides a better understanding of UML features. By explaining more complex features in terms of basic ones, we suggest an easy way users can gradually extend the set of UML elements they commonly apply in the modeling process.
(15 pages, gzipped PostScript: 87kb via HTTP, uncompressed PostScript: 431kb via HTTP)


[Gogolla et al., 1999a]
Martin Gogolla, Oliver Radfelder, and Mark Richters. A UML Semantics FAQ - The View from Bremen. In S.J.H. Kent, A. Evans, and B. Rumpe, editors, Proc. ECOOP'99 Workshop UML Semantics FAQ. University of Brighton, 1999.
This note spells out questions the authors found while studying the material defining the Unified Modeling Language UML. After formulating a preliminary question in Sec. 1, some detailed questions with answers and some detailed questions without answers are given in Sec. 2 and 3, respectively. Sections 4 and 5 just state questions with and without answers but we do not go into details explaining the importance of the questions. Our answers to the `questions with answers' can be found in our recent. In Sec. 6, a short hint to relevant literature ends this note.
(10 pages, gzipped PostScript: 87kb via HTTP, uncompressed PostScript: 523kb via HTTP)


[Gogolla et al., 1999b]
Martin Gogolla, Oliver Radfelder, and Mark Richters. Towards Three-Dimensional Representation and Animation of UML Diagrams. In Robert France and Bernhard Rumpe, editors, Proc. 2nd Int. Conf. Unified Modeling Language (UML'99), pages 489-502. Springer, Berlin, LNCS 1723, 1999.
The UML notation is intended to be drawn on two-dimensional surfaces. However, three-dimensional diagram layout and animation may improve comprehension of complex diagrams significantly. The paper concentrates on special UML diagram forms well-suited for advanced visualization. It makes a proposal for representing and animating such UML diagrams in a three-dimensional style.
(14 pages, gzipped PostScript: 558kb via HTTP, uncompressed PostScript: 1845kb via HTTP)


[Radfelder et al., 1999]
Oliver Radfelder, Martin Gogolla, and Volker Behr. On Designing and Querying a Material Information System. In M. Türksever, N.Y. Topaloglu, N. Zincir-Heywood, A. Kantarci, C.A. Sürgevil, and Ö. Özmen, editors, Proc. 14th Int. Symposium Computer and Information Science (ISCIS'99), pages 132-142. Ege University, Izmir, 1999.
We present an information system which has been developed in cooperation with a composite material development laboratorium and other industrial partners. The system enables people interested in this field to get knowledge about project participants and their offers. The main purpose of the development was to let all the involved people participate regardless of their technical skills. One precondition to achieve this goal was the development of an easy-to-learn graphical query language. The implementation has been led by the demand for platform independence and the necessity to involve the project participants in the maintenance of the data.
(11 pages, gzipped PostScript: 33kb via HTTP, uncompressed PostScript: 123kb via HTTP)


[Richters and Gogolla, 1999a]
Mark Richters and Martin Gogolla. A Metamodel for OCL. In Robert France and Bernhard Rumpe, editors, Proc. 2nd Int. Conf. Unified Modeling Language (UML'99), pages 156-171. Springer, Berlin, LNCS 1723, 1999.
The Object Constraint Language (OCL) allows the extension of UML models with constraints in a formal way. While the UML itself is defined by following a metamodeling approach, there is currently no equivalent definition for the OCL. We propose a metamodel for OCL that fills this gap. The benefit of a metamodel for OCL is that it precisely defines the syntax of all OCL concepts like types, expressions, and values in an abstract way and by means of UML features. Thus, all legal OCL expressions can be systematically derived and instantiated from the metamodel. We also show that our metamodel smoothly integrates with the UML metamodel. The focus of this work lies on the syntax of OCL; the metamodel does not include a definition of the semantics of constraints.
(16 pages, gzipped PostScript: 82kb via HTTP, uncompressed PostScript: 265kb via HTTP)


[Richters and Gogolla, 1999b]
Mark Richters and Martin Gogolla. On the Need for a Precise OCL Semantics. In Robert France, Bernhard Rumpe, Brian Henderson-Sellers, Jean-Michel Bruel, and Ana Moreira, editors, Proc. OOPSLA Workshop ``Rigorous Modeling and Analysis with the UML: Challenges and Limitations''. Colorado State University, Fort Collins, Colorado, 1999.
In our view a formalization of the OCL is beneficial for achieving the following goals: (1) Improvement of the OCL itself by pointing out some potential problems with its current definition, (2) a more precise understanding of UML class models and their interpretation, (3) a solid foundation for implementing CASE tools supporting analysis, simulation and validation of UML models. We also feel that there is one aspect of OCL which often gets underrated. OCL expressions cannot only be used to specify constraints, but more generally, one can utilize them to specify queries retrieving non-trivial information about certain objects in a given system state. These queries can then be translated into statements of a query language of the chosen implementation environment. A precise OCL semantics would obviously facilitate a more systematic description of a translation scheme from OCL to e.g. SQL or the ODMG's Object Query Language (OQL).
(3 pages, gzipped PostScript: 36kb via HTTP, uncompressed PostScript: 84kb via HTTP)


[Wagner and Gogolla, 1999]
Annika Wagner and Martin Gogolla. Semantics of Object-Oriented Languages. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, and Gregorz Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph Transformation, Volume II, Applications, Languages, and Tools, pages 181-211. World Scientific, Singapore, 1999.
Graph transformations can be applied everywhere, where graphs are used as a natural and intuitive description of complex phenomena. One field where this is the case is object modeling. The important role graphs play during object-oriented analysis and design shows their usefulness in the context of object orientation. A main characteristic of graph transformations is its direct operational executability. Combining both observations, it seems to be natural to use graph transformations to specify the operational behavior of objects. In this contribution we follow this idea by providing an operational semantics for the textual object description language TROLL light by means of graph transformations. But this is not the only possible application of graph transformations in the object-oriented field because what we are doing can be used also in combination with the graphical object modeling language UML.
(16 pages, gzipped PostScript: 312kb via HTTP, uncompressed PostScript: 714kb via HTTP)


[Cerioli et al., 1998]
Maura Cerioli, Martin Gogolla, Helene Kirchner, Bernd Krieg-Brückner, Zhenyu Qian, and Markus Wolf, editors. Algebraic System Specification and Development - Survey and Annotated Bibliography. Monographs of the Bremen Institute of Safe Systems (BISS). Shaker, Aachen, 1998.
This book is an annotated bibliography that attempts to provide an up-to-date overview of most past and present work on algebraic specification for researchers in algebraic specification and neighbouring fields. It extends the previous annotated bibliography by Bidoit, Kreowski, Lescanne, Orejas and Sannella. A review of the main topics of current and past research is given, with some indication of how the different approaches are related and pointers to relevant papers.
(142 pages, gzipped PostScript: 383kb via HTTP, uncompressed PostScript: 1535kb via HTTP)


[Gogolla, 1998]
Martin Gogolla. UML for the Impatient. Research Report 3/98, Universität Bremen, 1998.
By examples we give a short introduction into the nine diagram forms provided by the Unified Modeling Language (UML). The running example we use is a small traffic light system which we first formally describe in an object specification language. Afterwards, central aspects of the specification and the specified system are visualized with UML constructs. As a conclusion, we discuss a classification of the various UML diagram forms.
(23 pages, gzipped PostScript: 140kb via HTTP, uncompressed PostScript: 886kb via HTTP)


[Gogolla and Parisi-Presicce, 1998]
Martin Gogolla and Francesco Parisi-Presicce. State Diagrams in UML - A Formal Semantics using Graph Transformation. In Manfred Broy, Derek Coleman, Tom Maibaum, and Bernhard Rumpe, editors, Proc. ICSE'98 Workshop on Precise Semantics of Modeling Techniques (PSMT'98), pages 55-72. Technical University of Munich, Technical Report TUM-I9803, 1998.
We show how to transform UML (Unified Modeling Language) state diagrams into graphs by making explicit the intended semantics of the diagram. The process of state expansion in nested state diagrams is explained by graph transformations in three steps: (1) adding boundary nodes introducing a precise interface for the state to be expanded, (2) expanding the state, and (3)  removing the boundary nodes. The general idea of approaching the semantics of UML diagrams by graph transformations is applicable to other forms of UML diagrams as well. The main advantage of the graph transformation approach is the closeness between the (mathematical) graph representation and the (UML) diagram representation.
(18 pages, gzipped PostScript: 111kb via HTTP, uncompressed PostScript: 649kb via HTTP)


[Gogolla and Richters, 1998]
Martin Gogolla and Mark Richters. On Combing Semi-Formal and Formal Object Specification Techniques. In Francesco Parisi-Presicce, editor, Proc. 12th Int. Workshop Abstract Data Types (WADT'97), pages 238-252. Springer, Berlin, LNCS 1376, 1998.
In the early phases of software development it seems profitable to freely mix semi-formal and formal design techniques. Formal techniques have their strength in their ability to rigorously define desired software qualities like functionality, whereas semi-formal methods are usually said to be easier to understand and to be more human-nature oriented. We propose a new approach in order to combine these two areas by exploiting how constructs of the formal specification language TROLL light are related to the graphical elements of the UML approach.
(16 pages, gzipped PostScript: 77kb via HTTP, uncompressed PostScript: 353kb via HTTP)


[Gogolla et al., 1998]
Martin Gogolla, Anne Kathrin Huge, and Bodo Randt. Stepwise Re-Engineering and Development of Object-Oriented Database Schemata. In Roland R. Wagner, editor, Proc. 9th Int. Workshop Database and Expert Systems Applications (DEXA'98). IEEE, Los Alamitos, 1998.
We present a general approach for re-engineering of object-oriented database schemata. The approach consists of four dependent steps: (1) description of the data within the underlying basic data format, (2) application of a powerful semantic data model in order to construct a semantic database schema, (3) translation of the achieved schema into a general object model, and (4) implementation of the object schema in a concrete object-oriented database system. As an instantiation of this general procedure we report on a case study carried out in an industrial context where an Extended Entity-Relationship model was used as the semantic data model and ObjectStore as the implementation platform.
(6 pages, gzipped PostScript: 40kb via HTTP, uncompressed PostScript: 123kb via HTTP)


[Richters and Gogolla, 1998]
Mark Richters and Martin Gogolla. On Formalizing the UML Object Constraint Language OCL. In Tok-Wang Ling, Sudha Ram, and Mong Li Lee, editors, Proc. 17th Int. Conf. Conceptual Modeling (ER'98), pages 449-464. Springer, Berlin, LNCS 1507, 1998.
We present a formal semantics for the Object Constraint Language (OCL) which is part of the Unified Modeling Language (UML) -- an emerging standard language and notation for object-oriented analysis and design. In context of information systems modeling, UML class diagrams can be utilized for describing the overall structure, whereas additional integrity constraints and queries are specified with OCL expressions. By using OCL, constraints and queries can be specified in a formal yet comprehensible way. However, the OCL itself is currently defined only in an informal way. Thus the semantics of constraints is in general not precisely defined. Our approach gives precise meaning to OCL concepts and to some central aspects of UML class models. In consequence, a formal semantics facilitates verification, validation and simulation of models improving the quality of models and software design.
(16 pages, gzipped PostScript: 103kb via HTTP, uncompressed PostScript: 472kb via HTTP)


[Richters et al., 1998]
Mark Richters, Martin Gogolla, and Heino Gärtner. SIGN - Software Implementierung durch Graphische Notation. Interner Bericht, Universität Bremen, Fachbereich 3, 1998.
Das studentische Projekt SIGN (Software Implementierung durch Graphische Notation) wurde an der Universität Bremen von 1996 bis 1998 durchgeführt. Ziel des Projektes war die Entwicklung einer graphischen Modellierungssprache zur Unterstützung des objektorientierten Systementwurfs. Zur praktischen Umsetzung der Modellierungssprache wurde außerdem eine Entwicklungsumgebung entworfen und implementiert. Sowohl Sprache als auch das Entwicklungssystem wurden durchgehend objektorientiert entwickelt. Dabei wurde im Rahmen der Metamodellierung auch die zu entwerfende Sprache selbst eingesetzt. Dieses Papier faßt die Ziele, Methoden und Ergebnisse des Projektes zusammen.
(9 pages, gzipped PostScript: 82kb via HTTP, uncompressed PostScript: 480kb via HTTP)


[Buddrus et al., 1997]
Frank Buddrus, Heino Gärtner, and Sven-Eric Lautemann. First Steps to a Formal Framework for Multilevel Database Modifications. In A. Hameurlain and A Min Tjoa, editors, Proc. 8th Int. Conf. Database and Expert Systems Applications (DEXA'97), pages 240-251. Springer, Berlin, LNCS 1308, 1997.
We propose a formal basis for operations which can be understood as implicitly used in many kinds of schema modifications. Approaches for view definition, schema evolution, and schema versioning all rely on operations which work either on instance, on schema, or on both levels. This paper discusses a basic set of these operations called modification primitives and describes their semantics on the basis of the Extended Entity Relationship (EER) Model in a Hoare-style notation. We focus on the structural part of the schema definition and outline our ideas for arbitrary manipulations of instances.
(13 pages, gzipped PostScript: 82kb via HTTP, uncompressed PostScript: 383kb via HTTP)


[Gärtner, 1997]
Heino Gärtner. Perspectives for a Formal Framework for Schema Modification in Object Databases. In D.J. Ram, editor, Proc. 8th Int. Conf. Management of Data (COMAD'97), pages 238-249. Narosa, New Delhi, 1997.
This paper proposes a formal basis for the description of schema modification in object databases. We identify three necessary building blocks for the structural aspect of such a description: (i) basic schema and database objects, (ii) properties of (classes of) schema and database objects, and (iii) schema modifications, i.e. transitions between schemata and transitions between database states. The semantics for the basic schema and database objects is given in a denotational style. Properties of schemata can be described as formulas. For schema modification we introduce a set of schema modification primitives and describe their semantics by means of pre- and postcondition in a Hoare-style notation. We focus on the structural aspects of schema modification and describe some simple properties of our framework.
(12 pages, gzipped PostScript: 96kb via HTTP, uncompressed PostScript: 476kb via HTTP)


[Gogolla, 1997]
Martin Gogolla. On Behavioral Model Quality and Transformation. In Stephen W. Liddle, Stephen W. Clyde, and Scott N. Woodfield, editors, Proc. 16th Int. Conf. on Conceptual Modeling (ER'97), Workshop on Behavioral Models and Design Transformations. verb !http://osm7.cs.byu.edu/ER97/workshop4!, 1997.
This statement reflects experience of our group in conceptual modelling with Entity-Relationship and object-oriented approaches. It describes a general view on structural and behavioral aspects of conceptual models, their interrelationships, and their transformations, and sketches a proposal to build integrated models of them.
(4 pages, gzipped PostScript: 54kb via HTTP, uncompressed PostScript: 279kb via HTTP)


[Gogolla and Parisi-Presicce, 1997]
Martin Gogolla and Francesco Parisi-Presicce. State Diagrams in UML - A Formal Semantics using Graph Transformation. Rapporto di Ricerca 97/15, University of Rome `La Sapienza', Dipartimento di Scienze dell' Informazione, 1997.
We show how to transform UML (Unified Modeling Language) state diagrams into graphs by making explicit the intended semantics of the diagram. The process of state expansion in nested state diagrams is explained by graph transformations in three steps: (1) adding boundary nodes introducing a precise interface for the state to be expanded, (2) expanding the state, and (3)  removing the boundary nodes. The general idea of approaching the semantics of UML diagrams by graph transformations is applicable to other forms of UML diagrams as well. The main advantage of the graph transformation approach is the closeness between the (mathematical) graph representation and the (UML) diagram representation.
(19 pages, gzipped PostScript: 112kb via HTTP, uncompressed PostScript: 685kb via HTTP)


[Gogolla and Richters, 1997a]
Martin Gogolla and Mark Richters. On Constraints and Queries in UML. In Martin Schader and Axel Korthaus, editors, Proc. UML'97 Workshop `The Unified Modeling Language - Technical Aspects and Applications', pages 109-121. Physica-Verlag, Heidelberg, 1997.
The UML has recently been extended by an Object Constraint Language (OCL). This formal language can be used for specifying constraints on a model in order to restrict possible system states. We present some examples for illustrating main concepts of OCL. Problems with the current definition of OCL resulting from imprecise or ambiguous definitions are investigated. A comparison of OCL with a language for specification of queries and integrity constraints in an Extended Entity-Relationship model shows similarities between both approaches. This comparison could lead to a better understanding of OCL.
(14 pages, gzipped PostScript: 86kb via HTTP, uncompressed PostScript: 456kb via HTTP)


[Gogolla and Richters, 1997b]
Martin Gogolla and Mark Richters. Web-Based Object Animation. In Hans-Dieter Ehrich, Yulin Feng, and David Kung, editors, Object-Oriented Software Development, pages 16-16. Dagstuhl-Seminar-Report Nr. 174, 1997.
The current activities of our group comprises concrete case studies arising from practical projects: (1) Reengineering of a tram simulation system and (2) development of a material information system. Both projects use object-oriented description techniques on a semi-formal (OMT-like) and formal (TROLL-like) level. Semi-formal techniques are also the topic of a student project (18 students, 2 years). The aim of this student project is the development of an OMT design system. The formal basis for the above activities is the object description language TROLL light. Our group already has experience with implementations of this language on different platforms. The current implementation uses Java. The talk explains the user-interface of the current animation system which is based on HTML documents. Thus any Web browser can be employed for the validation of specifications. For demonstration purposes we use a small description of a car rentals case system.
(1 pages, gzipped PostScript: 15kb via HTTP, uncompressed PostScript: 86kb via HTTP)


[Richters, 1997]
Mark Richters. jtrl User Manual. Internal Report, Universität Bremen, 1997.
This manual provides information on using the jtrl system for developing and validating specifications written in the TROLL light language. Such specifications are used for modeling information systems as a set of interacting and communicating objects. With jtrl a model can be validated by direct execution (also called animation) of its specification. The manual presents all steps necessary to work with jtrl. These include instructions on system usage via the various user interfaces: command line, Web interface, and the graph visualization tool daVinci. A complete list of builtin operations and a grammar serve as reference for the language supported by jtrl.
(26 pages, gzipped PostScript: 162kb via HTTP, uncompressed PostScript: 921kb via HTTP)


[Richters and Gogolla, 1997a]
Mark Richters and Martin Gogolla. A Web-based Animator for Validating Object Specifications. In Bipin C. Desai and Barry Eaglestone, editors, Proc. Int. Database Engineering and Applications Symposium (IDEAS'97), pages 211-219. IEEE, Los Alamitos, 1997.
One of the central tasks in developing information systems is the specification of desired system properties. We use the object specification language TROLL light to formalize the conceptual model of a system. A TROLL light specification describes structural as well as dynamic characteristics of objects representing real-world entities. For validating specifications, we have developed an animation tool allowing us to reflect structural properties and dynamic behavior. The main concepts of the animator are illustrated by a working example. We present a simple specification of a car rental company and describe some of the steps performed during a typical animation session. The animation allows to check whether desired properties are fulfilled by the given object descriptions. Finally, some design and implementation issues regarding the utilized persistent programming environment and the Web-based user interface are discussed.
(9 pages, gzipped PostScript: 106kb via HTTP, uncompressed PostScript: 701kb via HTTP)


[Richters and Gogolla, 1997b]
Mark Richters and Martin Gogolla. A Web User Interface for an Object Specification Language. In Michel Bidoit, editor, Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), pages 867-870. Springer, Berlin, LNCS 1214, 1997.
We present an animation tool for the formal specification language TROLL light. The system allows the manipulation and querying of objects and navigation through object hierarchies. A Web-based user interface simplifies the usage of the system.
(5 pages, gzipped PostScript: 69kb via HTTP, uncompressed PostScript: 436kb via HTTP)


[Claßen et al., 1996]
Ingo Claßen, Martin Gogolla, and Michael Löwe. Dynamics in Information Systems - An Algebraic Approach to Specification, Construction and Correctness. Forschungsbericht 96/01, Technische Universität Berlin, 1996.
A formal framework based on algebraic graph theory is presented that integrates specification and construction of dynamics in information systems. Specifications are based on temporal logic whose semantics is given by algebras and partial homomorphisms. Constructions are given by graph transformation rules whose operational nature provides a first step towards actual implementations. Both are related by a correctness notion. The formal framework is especially suited as a semantical basis for graphical notations as used in conceptual modeling, thus combining intuitiveness of such notations with precision of formal methods.
(21 pages, gzipped PostScript: 80kb via HTTP, uncompressed PostScript: 225kb via HTTP)


[Gärtner and Gogolla, 1996]
Heino Gärtner and Martin Gogolla. LASSY - A System for Analysing Grammatical Dependencies in Latin. In Roland R. Wagner and Helmut Thoma, editors, Proc. 7th Int. Workshop Database and Expert Systems Applications (DEXA'96), pages 275-284. IEEE, Los Alamitos, 1996.
We introduce the Latin analysis system Lassy, a slim system for analyzing Latin sentences. Tools for interacting with a database for morphological features are integrated as well as an interface for defining and applying a grammar database. We also give a small outline of the grammar model used in Lassy which is a pragmatic integration of linguistic theories known from both dependency and phrase structure grammar.
(10 pages, gzipped PostScript: 105kb via HTTP, uncompressed PostScript: 577kb via HTTP)


[Gogolla, 1996a]
Martin Gogolla. Parameterizing Object Specifications. In Luigia Aiello, editor, Proc. 4th Int. Symposium Design and Implementation of Symbolic Computation Systems (DISCO'96), pages 126-137. Springer, Berlin, LNCS 1128, 1996.
We present a proposal for parameterized object specifications allowing especially objects sorts in the parameter. These object specifications permit to describe the part of the world to be modeled as an object community of concurrently existing and communicating objects. Our proposal for parameter passing works well on the syntactical level by means of a pushout construction. On the semantic level we use free constructions and corresponding forgetful functors.
(12 pages, gzipped PostScript: 47kb via HTTP, uncompressed PostScript: 152kb via HTTP)


[Gogolla, 1996b]
Martin Gogolla. Towards Object Visualization by Conceptual Graphs. In Peter W. Eklund, Gerard Ellis, and Graham Mann, editors, Proc. 4th Int. Conf. Conceptual Structures (ICCS'96), Auxiliary Proceedings, pages 175-188. University of New South Wales, Sydney, 1996.
The specification language TROLL light allows to describe the part of the world to be modeled in the information system design process as a community of concurrently existing and communicating objects. It follows the object paradigm by coherently describing structure as well behavior of conceptual objects. A TROLL light specification is divided into a signature part and an axiom part where formulas over the signature characterizing the object are formulated. Conceptual graphs are employed to visualize object schemata as well as object instances. Thereby, we provide a uniform platform for representing static and dynamic properties of objects and reasoning about them. By giving appropriate graph substitution rules, conceptual structures are capable to express system dynamics as well.
(14 pages, gzipped PostScript: 82kb via HTTP, uncompressed PostScript: 240kb via HTTP)


[Gogolla and Richters, 1996]
Martin Gogolla and Mark Richters. An Object Specification Language Implementation with Web User Interface based on Tycoon. In Hartmut Ehrig, Friedrich von Henke, Jose Meseguer, and Martin Wirsing, editors, Specification and Semantics, pages 8-11. Dagstuhl-Seminar-Report Nr. 151, 1996.
We concentrate on the user interface of a TROLL light implementation based on Tycoon. The implementation employs a normal Web browser (Netscape, Mosaic, etc.) for both the exploration of template, i.e. object type, descriptions and objects, i.e. instances of these templates. In particular, objects are represented by HTML documents and object references can be followed simply with the Web browser.
(3 pages, gzipped PostScript: 47kb via HTTP, uncompressed PostScript: 267kb via HTTP)


[Meyer et al., 1996]
Bernd Meyer, Gerhard D. Westerman, and Martin Gogolla. Drafting ER and OO Schemas in Prototyping Environments. Data and Knowledge Engineering, 19(3):201-240, 1996.
The system QUEER is a prototype of an information system design tool which directly supports an extended Entity-Relationship model on its front-end and uses a semantically well-founded query and manipulation language based on an Entity-Relationship calculus. The system basically consists of a set of compilers written in PROLOG which translate data specifications, schema definitions, queries, integrity constraints, and data-manipulation statements into PROLOG programs. All features mentioned are implemented in form and extent as described here.
(48 pages, gzipped PostScript: 106kb via HTTP, uncompressed PostScript: 353kb via HTTP)


[Wagner and Gogolla, 1996]
Annika Wagner and Martin Gogolla. Defining Operational Behavior of Object Specifications by Attributed Graph Transformations. Fundamenta Informaticae, 3,4:407-431, 1996.
A single pushout approach to the transformation of attributed partial graphs based on categories of partial algebras and partial morphisms is introduced. A sufficient condition for pushouts in these categories is presented. As the synchronization mechanism we use amalgamation of rules and show how synchronization can be minimized. We point out how the results obtained can be employed in order to define an operational semantics for object specification languages.
(25 pages, gzipped PostScript: 93kb via HTTP, uncompressed PostScript: 348kb via HTTP)


[Conrad et al., 1995]
Stefan Conrad, Grit Denker, Martin Gogolla, Rudolf Herzig, Nikolaos Vlachantonis, and Hans-Dieter Ehrich. Entwicklung zuverlässiger Informationssysteme. GI EMISA-Forum, 2:25-33, 1995.
Ausgehend von einem einfachen objektorientierten Ansatz zur Modellierung von Objektgesellschaften als Informationssysteme wird insbesondere eine geeignete Entwicklungsumgebung konzipiert, der Bereich Validation von Objektspezifikationen mittels Animation untersucht und ein Beweisunterstützungssystem entworfen, das formale Nachweise von Objekteigenschaften ermöglicht. Ziel ist die Entwicklung von Informationssystemen auf der Grundlage von objektorientierten Datenbanksystemen.
(9 pages, gzipped PostScript: 90kb via HTTP, uncompressed PostScript: 234kb via HTTP)


[Gogolla, 1995a]
Martin Gogolla. A Declarative Query Approach to Object Identification. In Mike Papazoglou, editor, Proc. 14th Int. Conf. Object-Oriented and Entity-Relationship Modelling (ER'95), pages 65-76. Springer, Berlin, LNCS 1021, 1995.
Object identification in data models, especially in semantic, Entity-Relationship, and object-oriented data models is studied. Various known approaches to object identification are shown, and an alternative proposal to the topic is put forward. The main new idea is to attach to each object type an arbitrary query in order to observe a unique, identifying property of objects of the corresponding type.
(12 pages, gzipped PostScript: 47kb via HTTP, uncompressed PostScript: 165kb via HTTP)


[Gogolla, 1995b]
Martin Gogolla. Identifying Objects by Declarative Queries. In Jan Chomicki, Gunter Saake, and Christina Sernadas, editors, The Role of Logics in Information Systems. Dagstuhl-Seminar-Report Nr. 121, 1995.
In this talk we study object identification in data models, especially in semantic, Entity-Relationship, and object-oriented data models. Various known approaches to object identification are shown, and an alternative proposal to the topic is put forward. The main new idea is to attach to each object type an arbitrary query in order to observe a unique, identifying property of objects of the corresponding type. This proposal seems to be more general than the well-known ``deep equality'' approach. The talk is organized as follows. First we introduce an example schema which will be used throughout the paper, and sketch the interpretation of object schemas in an informal way. Several known and our new proposal (the so-called observation term approach) to object identification are studied afterwards. The advantages of our new proposal are discussed, and its formal definition is mentioned. The talk ends with some concluding remarks.
(1 pages, gzipped PostScript: 16kb via HTTP, uncompressed PostScript: 89kb via HTTP)


[Gogolla, 1995c]
Martin Gogolla. Towards Schema Queries for Semantic Data Models. In Norman Revell and A Min Tjoa, editors, Proc. 6th Int. Conf. and Workshop on Database and Expert Systems Applications (DEXA'95), pages 274-283. ONMIPRESS, San Mateo, 1995.
We contribute to metadata management by giving a specification of extended Entity-Relationship schemas with the extended Entity-Relationship model itself. We formulate a number of integrity constraints describing the context-sensitive requirements an extended Entity-Relationship schema has to fulfill. By doing this, a certain class of schema queries can be formulated.
(10 pages, gzipped PostScript: 66kb via HTTP, uncompressed PostScript: 176kb via HTTP)


[Gogolla and Cerioli, 1995a]
Martin Gogolla and Maura Cerioli. What is an Abstract Data Type, after all? Technical Report PDISI-95-01, Dipartimento di Informatica e Scienze dell'Informazione, Universita di Genova, 1995.
We look back on ten Workshops on Abstract Data Types. A comprehensive KWIC index of titles of talks held at the workshop, a list of authors referencing their talks and publications, and a bibliography are presented.
(76 pages, gzipped PostScript: 169kb via HTTP, uncompressed PostScript: 784kb via HTTP)


[Gogolla and Cerioli, 1995b]
Martin Gogolla and Maura Cerioli. What is an Abstract Data Type, after all? In Egidio Astesiano, Gianna Reggio, and Andrzej Tarlecki, editors, Proc. 10th Int. Workshop Abstract Data Types (WADT'94), pages 499-523. Springer, Berlin, LNCS 906, 1995.
We look back on ten Workshops on Abstract Data Types. Organizers and publications, a list of authors referencing their talks and papers on the workshops, and a workshop bibliography are presented.
(26 pages, gzipped PostScript: 72kb via HTTP, uncompressed PostScript: 198kb via HTTP)


[Gogolla and Herzig, 1995a]
Martin Gogolla and Rudolf Herzig. An Algebraic Development Technique for Information Systems. In Vangalur S. Alagar and Maurice Nivat, editors, Proc. 4th Int. Conf. Algebraic Methodology and Software Technology (AMAST'95), pages 446-460. Springer, Berlin, LNCS 936, 1995.
This paper reports on successful application of algebraic ideas to the formal development of software systems, in particular information systems. It describes (1) a formalism, i.e., a language, for the specification of information systems, (2) a method for the construction of specifications in this language, and (3) implemented and planned parts of a specification environment covering important phases of the software development process.
(15 pages, gzipped PostScript: 85kb via HTTP, uncompressed PostScript: 222kb via HTTP)


[Gogolla and Herzig, 1995b]
Martin Gogolla and Rudolf Herzig. An Algebraic Semantics for the Object Specification Language TROLL light. In Egidio Astesiano, Gianna Reggio, and Andrzej Tarlecki, editors, Proc. 10th Int. Workshop Abstract Data Types (WADT'94), pages 288-304. Springer, Berlin, LNCS 906, 1995.
Within the KORSO project we have developed the object specification language TROLL light which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Recently, we have worked out the basic notions of a pure algebraic semantics for our language. The main underlying idea is to present a transition system where the states represent the states of the specified information system, and state transitions are caused by the occurrence of finite sets of events. This semantics is formulated by representing states and state transitions as algebras. The various constructs of TROLL light are unified to general axioms restricting the possible interpretations for TROLL light object descriptions.
(17 pages, gzipped PostScript: 97kb via HTTP, uncompressed PostScript: 256kb via HTTP)


[Gogolla et al., 1995a]
Martin Gogolla, Stefan Conrad, Grit Denker, Rudolf Herzig, and Nikolaos Vlachantonis. A Development Environment for an Object Specification Language. IEEE Transactions on Knowledge and Data Engineering, 7(3):505-508, 1995.
Techniques for the development of reliable information systems on the basis of their formal specification are the main concern in our project. Our work focuses on the specification language TROLL light which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes along with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. Two important ingredients of the environment to be described here in more detail are the animator and the proof support system.
(6 pages, gzipped PostScript: 64kb via HTTP, uncompressed PostScript: 300kb via HTTP)


[Gogolla et al., 1995b]
Martin Gogolla, Stefan Conrad, Grit Denker, Rudolf Herzig, Nikolaos Vlachantonis, and Hans-Dieter Ehrich. TROLL light - The Language and Its Development Environment. In Manfred Broy and Stefan Jähnichen, editors, KORSO - Methods, Languages, and Tools for the Construction of Correct Software (KORSO'95), pages 204-220. Springer, Berlin, LNCS 1009, 1995.
In our sub-project we are concerned with techniques for the development of reliable information systems on the basis of their formal specification. Our work focuses on the specification language TROLL light which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes along with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. Two important ingredients of the environment to be described here in more detail are the animator and the proof support system.
(16 pages, gzipped PostScript: 84kb via HTTP, uncompressed PostScript: 229kb via HTTP)


[Herzig and Gogolla, 1995]
Rudolf Herzig and Martin Gogolla. An Animator for the Object Specification Language TROLL light. In Vangalur S. Alagar and Rokia Missaoui, editors, Proc. Int Colloquium Object Orientation in Databases and Software Engineering (COODBSE'94), pages 156-170. World Scientific, River Edge (NJ), 1995.
In our project we are concerned with techniques for the development of reliable information systems on the basis of their formal specification. Our work focuses on the specification language TROLL light which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes along with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. One important ingredient of the environment to be described here in more detail is the TROLL light animator.
(15 pages, gzipped PostScript: 62kb via HTTP, uncompressed PostScript: 233kb via HTTP)


[Herzig et al., 1995]
Rudolf Herzig, Martin Gogolla, and Grit Denker. KORSO Reference Languages: Concepts and Application Domains - TROLL light. In Manfred Broy and Stefan Jähnichen, editors, KORSO - Methods, Languages, and Tools for the Construction of Correct Software (KORSO'95), pages 156-162. Springer, Berlin, LNCS 1009, 1995.
This paper gives an overview of the three KORSO reference languages SPECTRUM, TROLL light, and SPECIAL, exposing their motivation and background, language concepts, and typical application domains. The presentation of the different languages is followed by a discussion to what extent these languages may complement each other in the software development process.
(23 pages, gzipped PostScript: 61kb via HTTP, uncompressed PostScript: 164kb via HTTP)


[Conrad et al., 1994]
Stefan Conrad, Martin Gogolla, and Rudolf Herzig. Safe Derivations in Object Hierarchies. In D. Patel, Y. Sun, and S. Patel, editors, Proc. Int. Conf. Object-Oriented Information Systems (OOIS'94), pages 306-319. Springer, London, 1994.
We present a language for specifying structure and behavior of objects in information systems. This language is restricted to a set of core concepts for conceptual modeling. But it includes powerful concepts for specifying constraints and derived data. We present an algorithm for deciding on safe computation of derived information and demonstrate how this algorithm works with an example.
(14 pages, gzipped PostScript: 48kb via HTTP, uncompressed PostScript: 126kb via HTTP)


[Denker and Gogolla, 1994]
Grit Denker and Martin Gogolla. Translating TROLL light Concepts to Maude. In Hartmut Ehrig and Fernando Orejas, editors, Proc. 9th Int. Workshop Abstract Data Types (WADT'92), pages 173-187. Springer, Berlin, LNCS 785, 1994.
The specification language TROLL light is designed for the conceptual modeling of information systems. Maude is a logic programming language, which unifies the two paradigms of functional and concurrent object-oriented programming. Because of the very similar features offered by both languages, we present a translation from TROLL light concepts into the Maude language in order to compare the languages. Apart from presenting the translation, the languages are briefly described and illustrated by examples.
(16 pages, gzipped PostScript: 66kb via HTTP, uncompressed PostScript: 166kb via HTTP)


[Ehrich et al., 1994]
Hans-Dieter Ehrich, Martin Gogolla, Stefan Conrad, Grit Denker, Rudolf Herzig, and Nikolaos Vlachantonis. Entwicklung zuverlässiger Informationssysteme - Stand der Arbeiten im Januar'94. In Manfred Broy and Stefan Jähnichen, editors, Korrekte Software durch formale Methoden - 6. KORSO-Workshop (KORSO'93), pages 82-94, 1994.
Zwei wichtige Komponenten der TROLL light-Entwicklungsumgebung sind der Animator und das Beweisunterstützungssystem. Der Animator dient dem Prototyping einer mit TROLL light spezifizierten Objektgesellschaft und das Beweisunterstützungssystem hilft beim formalen Nachweis bestimmter Eigenschaften der Spezifikation. Eine andere Komponente ist ein Tool, das den Objektansatz von TROLL light mit der etablierten Entity-Relationship-Modellierungstechnik verbindet.

[Gogolla, 1994a]
Martin Gogolla. An Extended Entity-Relationship Model - Fundamentals and Pragmatics. Springer, Berlin, LNCS 767, 1994.
This text presents a comprehensive introduction to an extended Entity-Relationship model both on a conceptual and on a formal, mathematical level. In addition to the primitives given by the data model the text introduces a language for the formulation of constraints in order to restrict database states to consistent ones. The same language can be used to query databases. The text also explains an implementation of the approach chosen in the logic programming language PROLOG and discusses in this context the computational power of the proposed calculus. Finally, the extended Entity-Relationship calculus is applied in order to define the meaning of the relational query language SQL.
(145 pages, gzipped PostScript: 266kb via HTTP, uncompressed PostScript: 881kb via HTTP)


[Gogolla, 1994b]
Martin Gogolla. An Extended Entity-Relationship Model - Fundamentals and Pragmatics. GI EMISA-Forum, 1:80-80, 1994.
This text presents a comprehensive introduction to an extended Entity-Relationship model both on a conceptual and on a formal, mathematical level. In addition to the primitives given by the data model the text introduces a language for the formulation of constraints in order to restrict database states to consistent ones. The same language can be used to query databases. The text also explains an implementation of the approach chosen in the logic programming language PROLOG and discusses in this context the computational power of the proposed calculus. Finally, the extended Entity-Relationship calculus is applied in order to define the meaning of the relational query language SQL.
(1 pages, gzipped PostScript: 17kb via HTTP, uncompressed PostScript: 89kb via HTTP)


[Gogolla, 1994c]
Martin Gogolla. An Extended Entity-Relationship Model - Fundamentals and Pragmatics. GI Datenbankrundbrief, 13:86-86, 1994.
This text presents a comprehensive introduction to an extended Entity-Relationship model both on a conceptual and on a formal, mathematical level. In addition to the primitives given by the data model the text introduces a language for the formulation of constraints in order to restrict database states to consistent ones. The same language can be used to query databases. The text also explains an implementation of the approach chosen in the logic programming language PROLOG and discusses in this context the computational power of the proposed calculus. Finally, the extended Entity-Relationship calculus is applied in order to define the meaning of the relational query language SQL.
(1 pages, gzipped PostScript: 17kb via HTTP, uncompressed PostScript: 89kb via HTTP)


[Gogolla, 1994d]
Martin Gogolla. Grundlagen von Entity-Relationship-Modellen. Informatik-Skript 33, Technische Universität Braunschweig, 1994.
Nach einer kurzen Motivation in der Datenbanksysteme, Datenmodelle und insbesondere semantische Datenmodelle kurz charakterisiert werden wird das Braunschweiger Erweiterte Entity-Relationship-Modell mit einem zugehörigen Entity-Relationship-Kalkül samt Anwendungen des Kalküls vorgestellt. Es werden anschließend weitere semantische Datenmodelle wie IFO, ERC und OMT auf die Konzepte des vorgenannten Entity-Relationship-Modells zurückgeführt.
(62 pages, gzipped PostScript: 173kb via HTTP, uncompressed PostScript: 500kb via HTTP)


[Gogolla, 1994e]
Martin Gogolla. On Formal Semantics of Some Semantic Data Models. In Selahattin Kuru, Ufuk Caglayan, Erol Gelenbe, Levent Akin, and Cem Ersoy, editors, Proc. 9th Int. Symposium Computer and Information Science (ISCIS'94), pages 33-40. Bogazici University Printhouse, Istanbul, 1994.
We explain how different semantic data models like the ER model, the ERC approach and the OMT structural modeling method could be transformed into a semantically well-defined extended Entity-Relationship model and calculus.
(8 pages, gzipped PostScript: 68kb via HTTP, uncompressed PostScript: 165kb via HTTP)


[Gogolla et al., 1994a]
Martin Gogolla, Sedat Güler, and Rudolf Herzig. From Object Specification to Enhanced Logic Programming. In Selahattin Kuru, Ufuk Caglayan, Erol Gelenbe, Levent Akin, and Cem Ersoy, editors, Proc. 9th Int. Symposium Computer and Information Science (ISCIS'94), pages 423-430. Bogazici University Printhouse, Istanbul, 1994.
We combine the area of object-oriented specification and object-oriented logic programming by indicating the translation of a specification language into an enhanced logic programming language. The translation shows that in comparison to the programming language the specification language offers richer concepts. The background of our work is the development of rapid prototyping systems for object-oriented specification languages.
(8 pages, gzipped PostScript: 68kb via HTTP, uncompressed PostScript: 165kb via HTTP)


[Gogolla et al., 1994b]
Martin Gogolla, Nikolaos Vlachantonis, Rudolf Herzig, Grit Denker, Stefan Conrad, and Hans-Dieter Ehrich. The KORSO Approach to the Development of Reliable Information Systems. Informatik-Bericht 94-06, Technische Universität Braunschweig, 1994.
KORSO was a joint project of fourteen university partners and one industrial partner, sponsored by the German Ministry of Research and Technology (BMFT). The project aimed at the consolidation of existing and the investigation of new methods for the development of correct software. Within this framework the focus of the KORSO group at the Technical University of Braunschweig was on the improvement of techniques for the development of reliable information systems. Our work focused on the specification language TROLL light which allows to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes along with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. This report summarizes the results achieved by the Braunschweig KORSO group.
(59 pages, gzipped PostScript: 172kb via HTTP, uncompressed PostScript: 468kb via HTTP)


[Herzig and Gogolla, 1994a]
Rudolf Herzig and Martin Gogolla. A SQL-like Query Calculus for Object-Oriented Database Systems. In Elisa Bertino and Susan Urban, editors, Proc. Int. Symposium Object-Oriented Methodologies and Systems (ISOOMS'94), pages 20-39. Springer, Berlin, LNCS 858, 1994.
Currently much effort is being spent on providing object-oriented databases with ad hoc query facilities. In this paper we present a SQL-like query calculus whose major contribution lies in its inherent orthogonality and rigorous mathematical foundation. The calculus is essentially a calculus of complex values but it is defined independently of any concrete database model. The calculus can be used to formulate queries in value-based and object-based data models. Moreover it provides a general facility for the manipulation of complex values.
(20 pages, gzipped PostScript: 68kb via HTTP, uncompressed PostScript: 230kb via HTTP)


[Herzig and Gogolla, 1994b]
Rudolf Herzig and Martin Gogolla. On a Better Formal Basis for Stating SQL-like Queries in Value- And Object-Based Database Systems. Technical Report 9/94, Universität Bremen, 1994.
We present a formalism whose purpose is to serve as a rigid basis for describing SQL-like queries and constraints in context of both value- and object-based data models. The formalism, whose major contribution lies in its inherent orthogonality and rigorous mathematical foundation, is defined independently of any concrete database model. Instead it offers a general facility for the ad-hoc manipulation of structured values. In an improvement to the well-known relational domain or tuple calculi (or their extensions towards extended relational models) the formalism (1) guarantees safe and computable queries in an immanent way, (2) allows to explain duplicates in query results, and (3) supports the composition of queries from subqueries without the need to name intermediate query results. Hence it should be seen closer to concrete SQL than classical query calculi.
(26 pages, gzipped PostScript: 83kb via HTTP, uncompressed PostScript: 272kb via HTTP)


[Herzig et al., 1994a]
Rudolf Herzig, Stefan Conrad, and Martin Gogolla. Compositional Description of Object Communities with TROLL light. In Chris Chrisment, editor, Proc. Basque Int. Workshop Information Technology (BIWIT'94), pages 183-194. Cepadues Editions, Toulouse, 1994.
TROLL light is a language for the modeling of information systems. It is designed to describe the Universe of Discourse (UoD) as a system of concurrently existing and interacting objects. TROLL light objects have observable properties modeled by attributes, and the behavior of objects is described by events. Possible object observations may be restricted by constraints, whereas event occurrences may be restricted to specified life cycles. TROLL light objects are organized in an object hierarchy established by subobject relationships. Communication between objects is supported by event calling. Apart from introducing the various possibilities for the syntactical description of objects, we aim to describe how the state of an object community may be changed by event occurrences.
(12 pages, gzipped PostScript: 35kb via HTTP, uncompressed PostScript: 98kb via HTTP)


[Herzig et al., 1994b]
Rudolf Herzig, Heiko Fischer, and Martin Gogolla. Zur Gestaltung der Benutzeroberfläche bei der Animation von Objektspezifikationen. GI Datenbankrundbrief, 13:43-45, 1994. Proc. Workshop GI-Fachgruppe Datenbanken.
Im Rahmen des BMFT-Verbundprojekts KORSO beschäftigt sich die Braunschweiger Gruppe mit Aspekten der Entwicklung zuverlässiger Informationssysteme. Der Schwerpunkt liegt dabei auf Fragen der Spezifikation, Analyse und Validierung konzeptioneller Schemata. Zu TROLL light wurde eine Entwicklungsumgebung konzipiert, deren wesentliche, bisher implementierte Bestandteile ein Parser zur syntaktischen Analyse, eine Struktur zur persistenten Ablage, ein Beweisunterstützungssystem zum Nachweis spezieller Eigenschaften und ein Animationssystem zur Validierung von Objektspezifikationen sind. Wir diskutieren einige Anforderungen, die an ein Werkzeug zur Unterstützung der Animation von TROLL light-Objektspezifikationen zu stellen sind, und gehen darauf ein, in welcher Weise diese Anforderungen in der aktuellen Implementierung der Benutzungsschnittstelle des TROLL light-Animationssystems realisiert worden sind.
(4 pages, gzipped PostScript: 77kb via HTTP, uncompressed PostScript: 279kb via HTTP)


[Conrad et al., 1993]
Stefan Conrad, Grit Denker, Martin Gogolla, Rudolf Herzig, Nikolaos Vlachantonis, and Hans-Dieter Ehrich. Zur Entwicklung zuverlässiger Informationssysteme in KORSO. In H. Reichel, editor, Proc. 23. GI Jahrestagung (GI'93) - Informatik - Wirtschaft - Gesellschaft, pages 464-469. Springer, Berlin, Informatik Aktuell, 1993.
Innerhalb des KORSO-Projektes verfolgt unsere Gruppe das Ziel, die Entwicklung zuverlässiger Informationssysteme auf der Basis formaler Spezifikationen zu unterstützen. Dazu konzentriert sich unsere Arbeit auf die Spezifikationssprache TROLL light, die es erlaubt, Teile der zu modellierenden Welt als eine Gemeinschaft nebeneinander bestehender und miteinander kommunizierender Objekte zu beschreiben. Auf diese Weise bestimmen wir sowohl die Struktur als auch das Verhalten der konzeptionellen Objekte. Unsere Spezifikationsumgebung für TROLL light erlaubt die Animation von Spezifikationen ebenso wie das Beweisen von Eigenschaften der Spezifikationen unter Verwendung von Theorembeweisern.
(6 pages, gzipped PostScript: 58kb via HTTP, uncompressed PostScript: 144kb via HTTP)


[Ehrich et al., 1993a]
Hans-Dieter Ehrich, Martin Gogolla, Stefan Conrad, Grit Denker, Rudolf Herzig, and Nikolaos Vlachantonis. Beiträge zu ``Das BMFT-Verbundprojekt Korrekte Software (KORSO)''. In Manfred Broy and Stefan Jähnichen, editors, Das BMFT-Verbundprojekt Korrekte Software (KORSO), pages 160-161. Informatik - Forschung und Entwicklung, Vol. 8, No. 3, 1993.
Innerhalb des KORSO-Projektes verfolgt unsere Gruppe das Ziel, die Entwicklung zuverlässiger Informationssysteme auf der Basis formaler Spezifikationen zu unterstützen. Dazu konzentriert sich unsere Arbeit auf die Spezifikationssprache TROLL light, die es erlaubt, Teile der zu modellierenden Welt als eine Gemeinschaft nebeneinander bestehender und miteinander kommunizierender Objekte zu beschreiben. Auf diese Weise bestimmen wir sowohl die Struktur als auch das Verhalten der konzeptionellen Objekte. Unsere Spezifikationsumgebung für TROLL light erlaubt die Animation von Spezifikationen ebenso wie das Beweisen von Eigenschaften der Spezifikationen unter Verwendung von Theorembeweisern.

[Ehrich et al., 1993b]
Hans-Dieter Ehrich, Martin Gogolla, Stefan Conrad, Grit Denker, Rudolf Herzig, and Nikolaos Vlachantonis. Entwicklung zuverlässiger Informationssysteme - Stand der Arbeiten im Januar'93. In Manfred Broy and Stefan Jähnichen, editors, Korrekte Software durch formale Methoden - 4. KORSO-Workshop (KORSO'93), pages 50-56, 1993.
Innerhalb des KORSO-Projektes befaßt sich unsere Gruppe damit, die Entwicklung zuverlässiger Informationssysteme auf der Basis formaler Spezifikationen zu unterstützen. Dazu konzentriert sich unsere Arbeit auf die Spezifikationssprache TROLL light, die es erlaubt, Teile der zu modellierenden Welt als eine Gemeinschaft nebeneinander bestehender und miteinander kommunizierender Objekte zu beschreiben. Auf diese Weise bestimmen wir sowohl die Struktur als auch das Verhalten konzeptioneller Objekte. Unsere Spezifikationsumgebung für TROLL light erlaubt die Animation von Spezifikationen ebenso wie das Beweisen von Eigenschaften der Spezifikationen unter Verwendung von Theorembeweisern.

[Gogolla, 1993a]
Martin Gogolla. A Computational Model for TROLL light. In Hartmut Ehrig, Friedrich von Henke, Jose Meseguer, and Martin Wirsing, editors, Specification and Semantics. Dagstuhl-Seminar-Report Nr. 64, 1993.
The object specification language TROLL light is intended to be used for conceptual modeling of information systems. It is designed to describe the Universe of Discourse (UoD) as a system of concurrently existing and interacting objects, i.e., an object community. The first part of the talk introduces the various language concepts offered by TROLL light. The second part of our paper outlines a simplified computational model for TROLL light. After introducing signatures for collections of object types we explain how single states of an object community are constructed. By parallel occurrence of a finite set of events the states of object communities change. The object community itself is regarded as a graph where the nodes are the object community states reachable from an initial state and the edges represent transitions between states.
(1 pages, gzipped PostScript: 20kb via HTTP, uncompressed PostScript: 118kb via HTTP)


[Gogolla, 1993b]
Martin Gogolla. Some Examples for TROLL light Templates. In Hans-Dieter Ehrich, editor, Beiträge zu KORSO- und TROLL light-Fallstudien, pages 51-62. Technische Universität Braunschweig, Informatik-Bericht Nr. 93-11, 1993.
We introduce some small examples for templates which are given in the language TROLL light which is intended for the specification of conceptual objects in information systems. The spectrum of our examples ranges however from rather untypical information systems like clocks, counters, or flipflops over stacks and trees to more specific information system applications like libraries.
(68 pages, gzipped PostScript: 191kb via HTTP, uncompressed PostScript: 517kb via HTTP)


[Gogolla, 1993c]
Martin Gogolla. TROLL light - A Core Language for Specifying Objects. In Catriel Beeri, Andreas Heuer, Gunter Saake, and Susan Urban, editors, Formal Aspects of Object Base Dynamics. Dagstuhl-Seminar-Report Nr. 62, 1993.
TROLL light is a language for conceptual modeling of information systems. It is designed to describe the Universe of Discourse (UoD) as a system of concurrently existing and interacting objects. As a basis for our language we took the specification language TROLL. However, some details have been added or modified in order to round off TROLL light. This was necessary because we needed a clear and balanced semantic basis for our specification language. In TROLL light classes are understood as composite objects having the class extension as sub-objects. Therefore in contrast to TROLL an extra notion of class is not needed in TROLL light. Over and above that concepts like class attributes, meta-classes, or heterogeneous classes are inherent in TROLL light. Second TROLL light incorporates a query calculus providing a general declarative query facility for object-oriented databases.
(1 pages, gzipped PostScript: 31kb via HTTP, uncompressed PostScript: 170kb via HTTP)


[Gogolla and Claßen, 1993]
Martin Gogolla and Ingo Claßen. An Object-Oriented Design for the ACT ONE Environment. In Maurice Nivat, Charles Rattray, Theodor Rus, and Giuseppe Scollo, editors, Proc. 3rd Int. Conf. Algebraic Methodology and Software Technology (AMAST'93), pages 361-368. Springer, London, Workshops in Computing, 1993.
We define a conceptual model, i.e., an information system schema, for the well-established algebraic specification language ACT ONE and its accompanying specification environment. This paper gives a formal description of suitable database support for an environment supporting the interactive development of ACT ONE specifications. The object-oriented data model of TROLL light, a language developed recently within the KORSO project, is used to present the design of such an environment and its dynamic behavior. However, the concepts used are general enough to support other specification and even programming languages as well. Therefore, we feel the design of a conceptual schema for ACT ONE is mainly a case study in employing an object-oriented data model for database support of specification or programming languages. It is therefore a proposal for the consolidation of environments for algebraic specification languages.
(8 pages, gzipped PostScript: 55kb via HTTP, uncompressed PostScript: 134kb via HTTP)


[Gogolla et al., 1993a]
Martin Gogolla, Stefan Conrad, and Rudolf Herzig. Sketching Concepts and Computational Model of TROLL light. In Alfonso Miola, editor, Proc. 3rd Int. Symposium Design and Implementation of Symbolic Computation Systems (DISCO'93), pages 17-32. Springer, Berlin, LNCS 722, 1993.
The specification language TROLL light is intended to be used for conceptual modeling of information systems. It is designed to describe a system of concurrently existing and interacting objects. We introduces the various language concepts offered by TROLL light. TROLL light objects have observable properties modeled by attributes, and the behavior of objects is described by events. TROLL light objects are organized in an object hierarchy established by sub-object relationships. Communication among objects is supported by event calling. We outlines a simplified computational model for TROLL light. We explain how single states of an object community are constructed. By parallel occurrence of a finite set of events the states of object communities change. The object community itself is regarded as a graph where the nodes are the object community states reachable from an initial state and the edges represent transitions between states.
(16 pages, gzipped PostScript: 106kb via HTTP, uncompressed PostScript: 264kb via HTTP)


[Gogolla et al., 1993b]
Martin Gogolla, Rudolf Herzig, Stefan Conrad, Grit Denker, and Nikolaos Vlachantonis. Integrating the ER Approach in an OO Environment. In Ramez Elmasri, Vram Kouramajian, and Bernhard Thalheim, editors, Proc. 12th Int. Conf. Entity-Relationship Approach (ER'93), pages 376-389. Springer, Berlin, LNCS 823, 1993.
We translate Entity-Relationship (ER) schemas into the object-oriented specification language TROLL light. This language describes the Universe of Discourse (UoD) as a system of concurrently existing and interacting objects, i.e., an object community. Thereby two essential aspects, structure and behavior, are integrated in one formalism. By doing the translation from ER to TROLL light we preserve the visual advantages of the former and receive a formalism through the latter which can be mapped to an adequate object-oriented database system. Proceeding this way we hope our proposal for transforming ER schemas into TROLL light specifications provides a valuable link between structural and dynamic modeling.
(14 pages, gzipped PostScript: 94kb via HTTP, uncompressed PostScript: 231kb via HTTP)


[Vlachantonis et al., 1993]
Nikolaos Vlachantonis, Rudolf Herzig, Martin Gogolla, Grit Denker, Stefan Conrad, and Hans-Dieter Ehrich. Towards Reliable Information Systems: The KORSO Approach. In Colette Rolland, Francois Bodart, and Corine Cauvet, editors, Proc. 5th Int. Conf. Advanced Information Systems Engineering (CAiSE'93), pages 463-483. Springer, Berlin, LNCS 685, 1993.
Within the compound project KORSO our team is concerned with the research on techniques and methods for the development of reliable information systems on the basis of formal specifications. Our work focuses on the specification language TROLL light which allows to describe the part of the world which is to be modeled as a community of concurrently existing and communicating objects by determining their structure as well as their behavior. Moreover we develop and implement a computer aided specification environment for TROLL light which permits specification animation as well as the proof of properties of specifications.
(20 pages, gzipped PostScript: 87kb via HTTP, uncompressed PostScript: 229kb via HTTP)


[Conrad and Gogolla, 1992]
Stefan Conrad and Martin Gogolla. An Annotated Bibliography on Object-Orientation and Deduction. ACM SIGMOD Record, 21(1):123-132, 1992.
This note tries to briefly survey research activities and results on the integration of object-oriented concepts and deductive database languages.
(10 pages, gzipped PostScript: 61kb via HTTP, uncompressed PostScript: 150kb via HTTP)


[Conrad et al., 1992]
Stefan Conrad, Martin Gogolla, and Rudolf Herzig. TROLL light - A Core Language for Specifying Objects. Informatik-Bericht 92-02, Technische Universität Braunschweig, 1992.
TROLL light is a language for conceptual modeling of information systems. It is designed to describe the Universe of Discourse (UoD) as a system of concurrently existing and interacting objects. TROLL light objects have observable properties modeled by attributes, and the behavior of objects is described by events. Possible object observations may be restricted by constraints, whereas event occurrences may be restricted to specified life cycles. TROLL light objects are organized in an object hierarchy established by subobject relationships. Communication among objects is supported by event calling. Apart from introducing the various possibilities for the syntactical description of objects, we aim to describe how the state of an object community may be changed by event occurrences.
(26 pages, gzipped PostScript: 114kb via HTTP, uncompressed PostScript: 301kb via HTTP)


[Engels et al., 1992]
Gregor Engels, Martin Gogolla, Uwe Hohenstein, Klaus Hülsmann, Perdita Löhr-Richter, Gunter Saake, and Hans-Dieter Ehrich. Conceptual Modelling of Database Applications Using an Extended ER Model. Data and Knowledge Engineering, 9(2):157-204, 1992.
In this paper, we motivate and present a data model for conceptual design of structural and behavioural aspects of databases. We follow an object centered design paradigm in the spirit of semantic data models. The specification of structural aspects is divided into modelling of object structures and modelling of data types used for describing object properties. The specification of object structures is based on an Extended Entity-Relationship (EER) model. The specification of behavioural aspects is divided into the modelling of admissible database state evolutions by means of temporal integrity constraints and the formulation of database (trans)actions. The central link for integrating these design components is a descriptive logic-based query language for the EER model. The logic part of this language is the basis for static constraints and descriptive action specifications by means of pre- and postconditions.
(58 pages, gzipped PostScript: 163kb via HTTP, uncompressed PostScript: 484kb via HTTP)


[Gogolla, 1992a]
Martin Gogolla. Contributions to ``A Framework for Software Development in KORSO''. In Martin Wirsing, editor, A Framework for Software Development in KORSO. Ludwig-Maximilians-Universität München, Institut für Informatik, Bericht 9205, 1992.
This paper reports on the results of the first meeting of the KORSO methods group, held in Munich, January 1992. It presents an outline of a framework for a software development methodology in KORSO. The framework is based on a generic algebraic-axiomatic approach to software development. Goals and requirements for KORSO developments are described. The roles of correctness and verification are discussed.

[Gogolla, 1992b]
Martin Gogolla. Fundamentals and Pragmatics of an Entity-Relationship Approach. Habilitation thesis, Technische Universität Braunschweig, Naturwissenschaftliche Fakultät, 1992. Submitted November 1992, Accepted May 1993.
This text presents a comprehensive introduction to an extended Entity-Relationship model both on a conceptual and on a formal, mathematical level. In addition to the primitives given by the data model the text introduces a language for the formulation of constraints in order to restrict database states to consistent ones. The same language can be used to query databases. The text also explains an implementation of the approach chosen in the logic programming language PROLOG and discusses in this context the computational power of the proposed calculus. Finally, the extended Entity-Relationship calculus is applied in order to define the meaning of the relational query language SQL.
(145 pages, gzipped PostScript: 266kb via HTTP, uncompressed PostScript: 881kb via HTTP)


[Herzig and Gogolla, 1992]
Rudolf Herzig and Martin Gogolla. Transforming Conceptual Data Models into an Object Model. In Günter Pernul and A Min Tjoa, editors, Proc. 11th Int. Conf. Entity-Relationship Approach (ER'92), pages 280-298. Springer, Berlin, LNCS 645, 1992.
In this paper a conceptually simple structural object model focusing on object types, attributes and ISA relationships is introduced. The model is derived mainly from an extended Entity-Relationship approach, but concepts from other semantic and object-oriented models have influenced its features. It is shown how high-level conceptual data models can be mapped to this model, and to what extent the object model subsumes classical modeling paradigms.
(19 pages, gzipped PostScript: 108kb via HTTP, uncompressed PostScript: 278kb via HTTP)


[Claßen and Gogolla, 1991]
Ingo Claßen and Martin Gogolla. Towards a Conceptual Model for the Environment of the Algebraic Specification Language ACT ONE. Forschungsbericht 91/11, Technische Universität Berlin, 1991.
The paper defines a conceptual model for the algebraic specification language ACT ONE and its accompanying specification environment. But the approach chosen is quite general and can be employed for other specification languages as well. The definition of the database schema including integrity constraints is done by means of an expressive and semantically well-founded extended Entity-Relationship model and a respective calculus. The basic idea is to start with the context free grammar of ACT ONE and to introduce entity types for non-terminal symbols. Productions are modelled by a type construction and appropriate components. Context sensitive conditions are translated into integrity constraints formulated in the calculus. This approach especially allows to describe various degrees of incompleteness of ACT ONE types, for instance whether an ACT ONE type has already been checked syntactically or whether the flat equivalent of the type is available.
(24 pages, gzipped PostScript: 100kb via HTTP, uncompressed PostScript: 261kb via HTTP)


[Ehrich et al., 1991]
Hans-Dieter Ehrich, Martin Gogolla, and Amilcar Sernadas. Objects and Their Specification. In Michel Bidoit and Christine Choppy, editors, Proc. 8th Int. Workshop Abstract Data Types (WADT'91), pages 40-65. Springer, Berlin, LNCS 655, 1991.
Object-oriented concepts and constructions are explained in an informal and language-independent way. Various algebraic approaches for dealing with objects and their specification are examined, ADT-based ones as well as process-based ones. The conclusion is that the process view of objects seems to be more appropriate than the data type view.
(26 pages, gzipped PostScript: 97kb via HTTP, uncompressed PostScript: 255kb via HTTP)


[Gogolla and Ehrich, 1991]
Martin Gogolla and Hans-Dieter Ehrich. Contributions to ``COMPASS - A Comprehensive Algebraic Approach to System Specification and Development''. In Michel Bidoit, Hans-Jörg Kreowski, Pierre Lescanne, Fernando Orejas, and Don Sannella, editors, COMPASS - A Comprehensive Algebraic Approach to System Specification and Development. Springer, Berlin, LNCS 501, 1991.
This volume arose out of the work of the COMPASS Basic Research Working Group, funded by the European Community under the Basic Research Action programme, ref. no. 3264. The name COMPASS stands for ``a COMPrehensive Algebraic approach to System Specification and development''. An early version of this document was included in the original COMPASS project proposal as a review of the state of the art. The current version is the result of suggestions for improvements from the participants in the COMPASS project, assembled and edited into a more or less coherent form by five editors. Since the COMPASS working group includes most of the leading European experts in algebraic specification, the result should be a relatively comprehensive overview of the main work in the field. In spite of its deficiencies, we hope that it nevertheless represents a useful snapshot of the current state of the art.

[Gogolla and Hohenstein, 1991]
Martin Gogolla and Uwe Hohenstein. Towards a Semantic View of an Extended Entity-Relationship Model. ACM Transactions on Database Systems, 16(3):369-416, 1991.
This paper introduces an extended ER model concentrating nearly all concepts of known so-called semantic data models to a few syntactical constructs. Moreover, we provide our extended ER model with a formal mathematical semantics. On this basis a well-founded calculus is developed taking into account data operations on arbitrary user-defined data types and aggregate functions. We pay special attention to arithmetic operations as well as multivalued terms allowing nested queries in a uniform and consistent manner. We prove our calculus only allows the formulation of safe terms and queries yielding a finite result, and to be (at least) as expressive as the relational calculi.
(48 pages, gzipped PostScript: 5025kb via HTTP, uncompressed PostScript: 47544kb via HTTP)


[Gogolla et al., 1991]
Martin Gogolla, Bernd Meyer, and Gerhard D. Westerman. Drafting Extended Entity-Relationship Schemas with QUEER. In Toby Teorey, editor, Proc. 10th Int. Conf. Entity-Relationship Approach (ER'91), pages 561-585. ER Institute, San Mateo, 1991.
The system QUEER is a prototype of an information system design tool which directly supports an extended Entity-Relationship model on its front-end and uses a semantically well-founded query and manipulation language based on an Entity-Relationship calculus. The system basically consists of a set of compilers written in PROLOG which translate data specifications, schema definitions, queries, integrity constraints, and data-manipulation statements into PROLOG programs. All features mentioned are implemented in form and extent as described here.
(25 pages, gzipped PostScript: 111kb via HTTP, uncompressed PostScript: 290kb via HTTP)


[Engels et al., 1990]
Gregor Engels, Martin Gogolla, Uwe Hohenstein, Klaus Hülsmann, Perdita Löhr-Richter, Gunter Saake, and Hans-Dieter Ehrich. Conceptual Modelling of Database Applications Using an Extended ER Model. Informatik-Bericht 90-05, Technische Universität Braunschweig, 1990.
In this paper, we motivate and present a data model for conceptual design of structural and behavioural aspects of databases. We follow an object centered design paradigm in the spirit of semantic data models. The specification of structural aspects is divided into modelling of object structures and modelling of data types used for describing object properties. The specification of object structures is based on an Extended Entity-Relationship (EER) model. The specification of behavioural aspects is divided into the modelling of admissible database state evolutions by means of temporal integrity constraints and the formulation of database (trans)actions. The central link for integrating these design components is a descriptive logic-based query language for the EER model. The logic part of this language is the basis for static constraints and descriptive action specifications by means of pre- and postconditions.
(58 pages, gzipped PostScript: 163kb via HTTP, uncompressed PostScript: 484kb via HTTP)


[Gogolla, 1990a]
Martin Gogolla. A Note on the Translation of SQL to Tuple Calculus. Bulletin of the EATCS, 40:231-236, 1990.
This note presents a translation of a subset of the relational query language SQL into the well known tuple calculus. Roughly speaking, tuple calculus corresponds to first order predicate calculus. The SQL subset is relationally complete and represents a ``relational core'' of the language. Nevertheless, our translation is simple and elegant. Therefore it is especially well suited as a beginners course into the principles of a formal definition of SQL.
(5 pages, gzipped PostScript: 47kb via HTTP, uncompressed PostScript: 117kb via HTTP)


[Gogolla, 1990b]
Martin Gogolla. A Note on the Translation of SQL to Tuple Calculus. ACM SIGMOD Record, 19(1):18-22, 1990.
This note presents a translation of a subset of the relational query language SQL into the well known tuple calculus. Roughly speaking, tuple calculus corresponds to first order predicate calculus. The SQL subset is relationally complete and represents a ``relational core'' of the language. Nevertheless, our translation is simple and elegant. Therefore it is especially well suited as a beginners course into the principles of a formal definition of SQL.
(5 pages, gzipped PostScript: 47kb via HTTP, uncompressed PostScript: 117kb via HTTP)


[Gogolla, 1990c]
Martin Gogolla. Datalog - Eine deduktive Datenbanksprache. Informatik-Skript 25, Technische Universität Braunschweig, 1990.
Die vorliegenden Notizen sind Überarbeitungen der Folien, die für eine Vorlesung verwendet wurden. Stoffauswahl und Detailierungsgrad waren wesentlich von dem Umstand bestimmt, daß eine zweistündige Veranstaltung in einem Sommersemester mit 12 Wochen gehalten wurde. Die Struktur der Vorlesung lehnt sich an einen Übersichtsartikel von Ceri, Gottlob und Tanca an. Zusätzliche Definitionen, Sätze, Verfahren und Beispiele stammen aus der angegebenen Literatur. Andere Beispiele wurden in der Veranstaltung entwickelt. Die Hörer der Vorlesung haben durch kritische Fragen und Bemerkungen zur Verbesserung des Materials beigetragen.

[Gogolla and Karge, 1990]
Martin Gogolla and Ulrich Karge. Zur formalen Semantik von SQL. In Udo Walter Lipeck, Stefan Braß, and Gunter Saake, editors, Kurzfassungen 2. Workshop Grundlagen von Datenbanken (GvD'90), pages 27-29. Technische Universität Braunschweig, Informatik-Bericht Nr. 90-02, 1990.
Es wird ein Vorschlag zur Definition der formalen Semantik von SQL auf der Grundlage eines erweiterten Entity-Relationship-Kalküls diskutiert. Dieser zugrunde liegende Kalkül gestattet insbesondere eine semantisch wohl-definierte Verwendung von Aggregierungsfunktionen auf der Grundlage von Multimengen. Damit ist es möglich, sowohl die SQL Gruppierungsmöglichkeiten mittels GROUP BY als auch die (zumindest teilweise) hierauf basierenden SQL Aggregierungen MAX, MIN, AVG, COUNT und SUM präzise zu erklären. Auf dieser Grundlage können so Aussagen u.a. über die Äquivalenz von Anfragen und somit über beweisbare Eigenschaften der Sprache gemacht werden. Auf diesem Weg wird dann auch gezeigt, daß Unteranfragen, die mittels IN, ALL, ANY oder EXISTS gebildet werden, sich durch ein einziges Konstrukt, nämlich COUNT ausdrücken lassen.

[Karge and Gogolla, 1990]
Ulrich Karge and Martin Gogolla. Formal Semantics of SQL Queries. Informatik-Bericht 90-02, Technische Universität Braunschweig, 1990.
A formal semantics of the relational query language SQL (Structured Query Language) is presented by translating SQL into an extended relational calculus. This calculus allows the handling of grouping and aggregation as well as null vallues, and therefore special emphasis is laid on the correct translation of grouping and aggregation of SQL. The translation of an SQL query is performed in eight steps. Some steps can be omitted for most of the queries. Making use of the presented translation, it is possible to prove properties of SQL, e.g. subqueries which are added with IN, ALL, or EXISTS can be replaced equivalently by subqueries using the aggregation function COUNT.

[Meyer et al., 1990]
Bernd Meyer, Gerhard D. Westerman, and Martin Gogolla. QUEER - A Prolog Based Prototype for an Extended ER Approach. Informatik-Bericht 90-03, Technische Universität Braunschweig, 1990.
The combination of logic programming and databases has been given broad attention in recent years. However, mainly the connections between the relational data model and logic programming have been investigated. The application of logic programming languages as a basis for information systems founded on more complex, i.e. conceptual data models has received comparatively less attention. With the system QUEER, we introduce the prototype of a PROLOG-based information system which directly supports an extended Entity-Relationship model on its front-end and uses a semantically well-founded query and manipulation language based on an Entity-Relationship calculus. The system basically consists of a set of compilers written in PROLOG which translate data specifications, schema definitions, queries, and data-manipulation statements into PROLOG programs.
(36 pages, gzipped PostScript: 136kb via HTTP, uncompressed PostScript: 367kb via HTTP)


[Ehrich et al., 1989a]
Hans-Dieter Ehrich, Gregor Engels, Martin Gogolla, and Gunter Saake, editors. Abstracts Workshop Grundlagen von Datenbanken (GvD'89). Technische Universität Braunschweig, Informatik-Bericht Nr. 89-02, 1989.
Der vorliegende Bericht faßt die Kurzfassungen der Vorträge zusammen, die für den Workshop Grundlagen von Datenbanken (16.-19.5.89 im Herrenhaus Volkse) angemeldet wurden. Der Workshop hat das Anliegen, die Kommunikation zwischen den deutschsprachigen Arbeitsgruppen zu fördern, die um Bereich der theoretischen, konzeptionellen und methodologischen Grundlagen von Daten- und Wissensbanken arbeiten. Insbesondere den jüngeren Nachwuchswissenschaftlern soll der Workshop Gelegenheit bieten, in zwangloser Umgebung Ideen, Ansätze und Ergebnisse auszutauschen und zu diskutieren. Die Vielfalt der Anmeldungen zeigt, daß für Workshops dieser Art - und dieser Thematik - ein großer Bedarf besteht.

[Ehrich et al., 1989b]
Hans-Dieter Ehrich, Martin Gogolla, and Udo Walter Lipeck. Algebraische Spezifikation Abstrakter Datentypen - Eine Einführung in die Theorie. Leitfäden und Monographien der Informatik. Teubner, Stuttgart, 1989.
Dieses Buch ist aus der Überarbeitung und Erweiterung von Notizen zu Vorlesungen entstanden, die seit 1977 zunächst vom ersten Autor an der Universität Dortmund, seit 1982 dann von allen drei Autoren in wechselnder Folge an der Technischen Universität Braunschweig gehalten wurden. Der Schwerpunkt des Buches liegt bei den theoretischen Grundlagen, jedoch haben die Möglichkeiten und Grenzen praktischer Anwendung die Auswahl und die Gestaltung des Stoffes stark beeinflußt. Das Buch richtet sich vornehmlich an Informatiker, die sich mit Grundlagen des Software-Entwurfs auseinandersetzen wollen, und an Mathematiker, die sich für Anwendungen der universellen Algebra und der Logik in der Informatik interessieren.

[Gogolla, 1989a]
Martin Gogolla. Algebraization and Integrity Constraints for an Extended Entity-Relationship Approach. In Josep Diaz and Fernando Orejas, editors, Proc. 3rd Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT'89), pages 259-274. Springer, Berlin, LNCS 351, 1989.
An extended Entity-Relationship model concentrating nearly all concepts of known ``semantic'' data models and especially allowing arbitrary user defined data types is introduced. The semantics of the model is described purely in algebraic terms mainly based on the notions of signature, algebra and extension. On this basis a calculus making intensive use of abstract data types is defined and employed for the formulation of typical integrity constaints like functional restrictions and key specifications.
(16 pages, gzipped PostScript: 70kb via HTTP, uncompressed PostScript: 186kb via HTTP)


[Gogolla, 1989b]
Martin Gogolla. Zur Übersetzung eines ER-Kalküls nach Prolog. In Hans-Dieter Ehrich, Gregor Engels, Martin Gogolla, and Gunter Saake, editors, Abstracts Workshop Grundlagen von Datenbanken (GvD'89). Technische Universität Braunschweig, Informatik-Bericht Nr. 89-02, 1989.
Auf der Basis eines erweiterten ER Modells werden sowohl Schemata als auch die zugehörigen Datenbanzustände mittels Prolog-Fakten dargestellt. Es wird ein Verfahren angegeben, das es gestattet, Terme eines auf dem erweiterten ER Modell aufbauenden Kalküls in äquivalente Prolog-Prädikate zu übersetzen. Mit Hilfe dieser Terme bzw. der entsprechenden Prolog-Prädikate lassen sich einerseits Anfragen bzgl. des gegebenen Datenbankzustands formulieren und auswerten. Andererseits dienen diese Terme bzw. die äquivalenten Prolog-Prädikate auch zur Überprüfung (statischer) Integritätsbedingengen im repräsentierten Zustand.

[Gogolla and Ehrich, 1989]
Martin Gogolla and Hans-Dieter Ehrich. Contributions to ``COMPASS - A Comprehensive Algebraic Approach to System Specification and Development''. In Bernd Krieg-Brückner, editor, COMPASS - A Comprehensive Algebraic Approach to System Specification and Development. Universität Bremen, Informatik-Bericht 6/89, 1989.
COMPASS is funded as a Basic Research Workong Group under the ESPRIT Programme of the European Communities. This document contains those three chapters of the original proposal that we believe to be of potential interest to a wider audience. The first chapter states the general objectives of the cooperation in the Working Group. The second chapter gives a summary of the State of the Art for and of our own work as we saw it in June 1988. Thus it is in many ways incomplete with respect to the work of others and does not claim full coverage. We believe, however, that it provides an overview that might be of interest for other researchers in the area of Formal Methods in Computing Science. The third chapter lists the references to work mentioned in the previous chapter. Again, it is by no means complete. Overall, chapter II and III can be regarded as a first approximation of an annotated bibliography of the area of algebraic specification.

[Ehrich et al., 1988]
Hans-Dieter Ehrich, Klaus Drosten, and Martin Gogolla. Towards an Algebraic Semantics for Database Specification. In Robert A. Meersman and Amilcar C. Sernadas, editors, Proc. 2nd IFIP 2.6 Working Conf. Database Semantics (DS-2'86), pages 119-135. North Holland, Amsterdam, 1988.
In the framework of a modal-algebraic approach to database semantics, the specification of abstract object types on the basis of abstract data types is studied. As a semantic framework for determining admissible states and state sequences, a standard universe of ``possible objects'' and their interrelationships has to be associated with a schema specification. This paper gives a construction of such a standard universe from a given key system including certain constraints. There is also an abstract algebraic characterisation of the universe (up to isomorphism) in the terms of final algebras. Within this framework, a general definition of admissible states and state sequences as the semantics of a schema specification is discussed briefly.

[Hohenstein and Gogolla, 1988a]
Uwe Hohenstein and Martin Gogolla. A Calculus for an Extended Entity-Relationship Model Incorporating Arbitrary Data Operations and Aggregate Functions. In Carlo Battini, editor, Proc. 7th Int. Conf. Entity-Relationship Approach (ER'88), pages 129-148. North-Holland, Amsterdam, 1988.
We propose a semantically well-founded Entity-Relationship calculus that takes into account data operations (especially arithmetic operations) on arbitrary defineable data types and aggregate functions, as well as multivalued terms allowing nested queries in a uniform and consistent manner. We define our calculus in a way that only allows the formulation of safe terms and queries (yielding a finite result) and that it is (at least) as powerful as the relational calculi. The calculus is based upon an extended ER model concentrating nearly all concepts of known so-called semantic data models to a few syntactical constructs. Moreover, we provide our extended ER model with a formal semantics, since otherwise the semantics of the calculus cannot be defined mathematically precise.

[Hohenstein and Gogolla, 1988b]
Uwe Hohenstein and Martin Gogolla. Towards a Semantic View of an Extended Entity-Relationship Model. Informatik-Bericht 88-02, Technische Universität Braunschweig, 1988.
This paper introduces an extended ER model concentrating nearly all concepts of known so-called semantic data models to a few syntactical constructs. Moreover, we provide our extended ER model with a formal mathematical semantics. On this basis a well-founded calculus is developed taking into account data operations on arbitrary user-defined data types and aggregate functions. We pay special attention to arithmetic operations as well as multivalued terms allowing nested queries in a uniform and consistent manner. We prove our calculus only allows the formulation of safe terms and queries yielding a finite result, and to be (at least) as expressive as the relational calculus.

[Gogolla, 1987]
Martin Gogolla. On Parametric Algebraic Specifications with Clean Error Handling. In Hartmut Ehrig, Robert Kowalski, and Giorgio Levi, editors, Proc. 2nd Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT'87), pages 81-95. Springer, Berlin, LNCS 249, 1987.
Usual algebraic specification techniques can be extended to treat partially ordered sorts. This allows the introduction of sub- and supersorts as well as overloaded operators, while pleasant features of the equational specification method (e.g. existence of initial algebras and equivalence of algebraic and operational semantics) are preserved. On this basis error and exception handling is studied. For each sort an ok and an error subsort is introduced and clean algebras (i.e. algebras which are ok-error-consistent and ok-error-complete) are considered. This new approach allows to prove an extension lemma for persistent parametric specifications which permit error handling.

[Ehrich et al., 1986]
Hans-Dieter Ehrich, Klaus Drosten, Martin Gogolla, and Udo Walter Lipeck, editors. Abstracts 4th Int. Workshop Abstract Data Types (WADT'86). Technische Universität Braunschweig, Informatik-Bericht Nr. 86-09, 1986.
Here are the abstracts of talks presented at the 4th Workshop on Specification of Abstract Data Types which was held at Burg Warberg near Braunschweig, May 20-23, 1986. About 70 participants attended the workshop, more than ever before in this series of workshops, starting in Langscheid 1982 and going on in Passau 1983 and in Bremen 1984. We all look forward to the next meeting in Edinburgh which is scheduled to take place in fall 1987 and will be organized by Don Sannella.

[Gogolla, 1986a]
Martin Gogolla. Exception Handling and Subsorts. In Hans-Dieter Ehrich, Klaus Drosten, Martin Gogolla, and Udo Walter Lipeck, editors, Abstracts 4th Int. Workshop Abstract Data Types (WADT'86). Technische Universität Braunschweig, Informatik-Bericht Nr. 86-09, 1986.
Usual algebraic specification techniques can be extended to treat partially ordered sorts. This allows the introduction of sub- and supersorts as well as overloaded operators, while pleasant features of the equational specification method (e.g. existence of initial algebras and equivalence of algebraic and operational semantics) are preserved. Partially ordered sorts can also be used as a basis for exception and error handling. We discuss three different, but closey related methods: (1) Ok-subsorts, (2) error-subsorts, and (3) disjoint ok- and error-subsorts. In particular, the three approaches are considered with respect to error introduction, error propagation and error recovery.

[Gogolla, 1986b]
Martin Gogolla. Über Partiell Geordnete Sortenmengen und deren Anwendung zur Fehlerbehandlung in Abstrakten Datentypen. PhD thesis, Technische Universität Braunschweig, Naturwissenschaftliche Fakultät, 1986. Mainly material from the CAAP'84, TCS'84, WADT'84 and TAPSOFT'87 papers.
Algebraische Spezifikationen von Datentypen werden um Ausdrucksmittel zur Darstellung von Halbordnungen auf den Trägern erweitert. Dies ermöglicht insbesondere die Behandlung von Unter- und Obersorten. Neben Gleichungen werden auch Deklarationen in Spezifikationen zugelassen, die es gestatten, einem Term eine neue Sorte zuzuweisen. Als Semantik ergibt sich stets eine initiale Algebra. Auf dieser Basis werden verschiedene Methoden zur Behandlung von Fehlern und Ausnahmen in abstrakten Datentypen vorgestellt, und ein Vorschlag zu deren Parametrisierung wird diskutiert.

[Gogolla, 1985a]
Martin Gogolla. A Final Algebra Semantics for Errors and Exceptions. Informatik-Bericht 85-06, Technische Universität Braunschweig, 1985.
Algebraic specifications allowing equations and inequations are studied. A characterisation of the existence of models and initial algebras as well as a criterion for the existence of final algebras for such specifications are given. As an application it is shown, how the result can be applied to yield maximal error propagation preserving error recovery in abstract data types.

[Gogolla, 1985b]
Martin Gogolla. A Final Algebra Semantics for Errors and Exceptions. In Hans-Jörg Kreowski, editor, Proc. 3rd Int. Workshop Abstract Data Types (WADT'84), pages 89-103. Springer Berlin, Informatik Fachberichte 116, 1985.
Algebraic specifications allowing equations and inequations are studied. A characterisation of the existence of models and initial algebras as well as a criterion for the existence of final algebras for such specifications are given. As an application it is shown, how the result can be applied to yield maximal error propagation preserving error recovery in abstract data types.

[Lipeck et al., 1985]
Udo Walter Lipeck, Hans-Dieter Ehrich, and Martin Gogolla. Specifying Admissibility of Dynamic Database Behaviour Using Temporal Logic. In Amilcar Sernadas, Janis Bubenko, and Antoni Olive, editors, Proc. IFIP Working Conf. Theoretical and Formal Aspects of Information Systems (TFAIS'85), pages 145-157. North Holland, Amsterdam, 1985.
This work uses temporal logic as a calculus for expressing integrity constraints that specify admissibility of dynamic database behaviour. Formulas are interpreted in state sequences representing dynamic behaviour. Our approach incorporates temporal quantifications by ``always'' and ``sometime'', and quantifiers bounded by intervals in state sequences. Moreover, dynamically changing domains of database values are considered. We then use special kinds of formulas as a language for dynamic constraints and give some hints how to specify in typical situations. For such formulas, a frame for monitoring constraints during runtime of a database is discussed which allows to characterize admissibility operationally.
(13 pages, gzipped PostScript: 1606kb via HTTP, uncompressed PostScript: 20511kb via HTTP)


[Ehrich et al., 1984]
Hans-Dieter Ehrich, Udo Walter Lipeck, and Martin Gogolla. Specification, Semantics and Enforcement of Dynamic Database Constraints. In Umeshwar Dayal, Gunter Schlageter, and Lim Huat Seng, editors, Proc. 10th Int. Conf. Very Large Data Bases (VLDB'84), pages 310-318. Morgan Kaufmann, San Mateo, 1984.
In order to specify dynamic constraints, we present a simplified version of temporal logic based on the temporal quantifiers ``always'' and ``sometime'' as well as their bounded versions ``always..until'' and ``sometime..before''. We show that, in most practical cases, the bounded temporal quantifiers can be expressed by appropriate formulas with unbounded temporal quantifiers. We then use special kinds of temporal formulas as a language to specify dynamic constraints. The problem of enforcing such constraints is then reduced to the problem of enforcing dynamically changing sets of two kinds of static constraints, called universal and existential constraints. While universal constraints can be enforced strictly in principle, violation of existential constraints cannot be detected in each case at the earliest moment. We give a sufficient criterion for detecting violation of existential constraints.
(8 pages, gzipped PostScript: 1153kb via HTTP, uncompressed PostScript: 12773kb via HTTP)


[Gogolla, 1984a]
Martin Gogolla. A Final Algebra Semantics for Errors and Exceptions. In Hans-Jörg Kreowski and Anne Wilharm, editors, Abstracts 3rd Int. Workshop Abstract Data Types (WADT'84). Universität Bremen, Informatik-Bericht 9/84, 1984.
Algebraic specifications allowing equations and inequations are studied. A characterisation of the existence of models and initial algebras as well as a criterion for the existence of final algebras for such specifications are given. As an application it is shown, how the result can be applied to yield maximal error propagation preserving error recovery in abstract data types.

[Gogolla, 1984b]
Martin Gogolla. Partially Ordered Sorts in Algebraic Specifications. In Bruno Courcelle, editor, Proc. 9th Int. Colloquium Trees in Algebra and Programming (CAAP'84), pages 139-153. Cambridge University Press, Cambridge, 1984.
Conventional algebraic specification techniques cannot express relationships between sorts formally. The approach presented here puts more structure into the specification by allowing a partial ordering on the set of sorts to describe that one sort is a subsort of another sort. This concept implies that one function can occur more than one time in the signature with different domains and codomains. The initial algebra semantics of our specifications with a partial ordering on the set of sorts are studied.
(15 pages, gzipped PostScript: 1584kb via HTTP, uncompressed PostScript: 20309kb via HTTP, PDF: 1179kb via HTTP)


[Gogolla et al., 1984]
Martin Gogolla, Klaus Drosten, Udo Lipeck, and Hans-Dieter Ehrich. Algebraic and Operational Semantics of Specifications Allowing Exceptions and Errors. Theoretical Computer Science, 34:289-313, 1984.
The specification of abstract data types requires the possibility to treat exceptions and errors. We present an approach allowing all forms of error handling: error introduction, error propagation and error recovery. The algebraic semantics of our method and a new correctness criterion are given. We also introduce an operational semantics of a subclass of our specifications which coincides with the algebraic semantics.
(25 pages, gzipped PostScript: 1749kb via HTTP, uncompressed PostScript: 22673kb via HTTP)


[Gogolla, 1983a]
Martin Gogolla. Algebraic Specification of Subsorts. In Manfred Broy and Martin Wirsing, editors, Abstracts 2nd Int. Workshop Abstract Data Types (WADT'83). Universität Passau, Informatik-Bericht, 1983.
A method for the algebraic specification of subsorts and overloaded operators is presented. In this approach algebras are described by equations and declarations. A declaration is a construct, which assures that an expression has a certain type. It is shown that every specification consisting of equations and declarations has an initial model. Furthermore it is proved that declarations can be expressed only by equations using hidden sorts and functions. An as application it is shown how errors and exceptions in abstract data types can be treated by using declarations. For every sort an ok subsort representing the non error elements is introduced and by the use of declarations the functions are divided into those which may introduce errors and those which return ok values when applied to such ones. By this, error introduction and error propagation as well as error recovery is possible.

[Gogolla, 1983b]
Martin Gogolla. Algebraic Specifications with Partially Ordered Sorts and Declarations. Forschungsbericht 169, Universität Dortmund, Abteilung Informatik, 1983.
Conventional algebraic specification techniques cannot express relationships between sorts formally. The approach presented here puts more structure into the specification by allowing a partial ordering on the set of sorts to describe that one sort is a subsort of another sort. This concept implies that one function can occur more than one time in the signature with different domains and codomains. Apart from equations our specifications allow declarations to type a term of a certain sort to a subsort of the given one. The initial algebra semantics of our specifications with a partial ordering on the set of sorts are studied.

[Gogolla and Ehrich, 1983]
Martin Gogolla and Hans-Dieter Ehrich. Algebraic Specifications with Subsorts Using Declarations. Bulletin of the EATCS, 21:31-38, 1983.
Conventional algebraic specifications describe data types some times only implicit with hidden sorts and functions. A more powerful and elegant technique can be achived by putting more structure into the specification. Our approach distinguishes between basis sorts and subsorts. The subsorts, whose carriers are included in the basis sort carriers, are described by declarations, i.e. a list of terms possibly with variables of basis as well as subsorts. We study the initial algebra semantics of our specifications, which include declarations and equations.

[Drosten et al., 1982]
Klaus Drosten, Martin Gogolla, Hans-Dieter Ehrich, and Udo Lipeck. A Hierarchical Approach to an Operational Semantics for Conditional Algebraic Specifications. Forschungsbericht 144, Universität Dortmund, Abteilung Informatik, 1982.
For the specification of abstract data types, it is most convenient in many cases not only to have pure equations, but conditional ones. We present a hierarchical approach where conditions have to be evaluated on underlying levels. An operational semantics is obtained via term rewriting systems. In order to guarantee its well-definedness, we provide sufficient syntactical criteria for the Church-Rosser property. Moreover, these criteria are sufficient for the termination of the full substitution reduction strategy, as well.

[Gogolla et al., 1982a]
Martin Gogolla, Klaus Drosten, Udo Lipeck, and Hans-Dieter Ehrich. Algebraic and Operational Semantics of Exceptions and Errors. In Armin B. Cremers and Hans-Peter Kriegel, editors, Proc. 6th GI Conf. Theoretical Computer Science, pages 141-151. Springer, Berlin, LNCS 145, 1982.
The specification of abstract data types requires the possibility to treat exceptions and errors. We present an approach allowing all forms of error handling: error introduction, error propagation and error recovery. The algebraic semantics of our method and a new correctness criterion are given. We also introduce an operational semantics of a subclass of our specifications which coincides with the algebraic semantics.

[Gogolla et al., 1982b]
Martin Gogolla, Klaus Drosten, Udo Lipeck, and Hans-Dieter Ehrich. Algebraic and Operational Semantics of Specifications Allowing Exceptions and Errors. Forschungsbericht 140, Universität Dortmund, Abteilung Informatik, 1982.
The specification of abstract data types requires the possibility to treat exceptions and errors. We present an approach allowing all forms of error handling: error introduction, error propagation and error recovery. The algebraic semantics of our method and a new correctness criterion are given. We also introduce an operational semantics of a subclass of our specifications which coincides with the algebraic semantics.

[Gogolla, 1980]
Martin Gogolla. Eine Charakterisierung von nicht-strukturierten Flußdiagrammen. Master's thesis, Universität Dortmund, Abteilung Informatik, 1980.
In dieser Arbeit wird eine Formalisierung der Begriffe Flußdiagramm und Strukturiertheit eines Flußdiagramms angegeben, und es werden nicht-strukturierte Flußdiagramme über bestimmte Teilgraphen beschrieben. Flußdiagramme geben den Kontrollfluß von Programmen wieder, und Analysen des Programmablaufs können unter anderem zur Optimierung in Compilern, Umkehrübersetzung von maschinennahen Programmen und Umwandlung von unstrukturierten Programmen in lesebare Form dienen. Fragestellungen nach der Ursache der Unstrukturiertheit sind sicherlich auch im Hinblick auf die Methodik der Programmierung von Interesse.

[Coy et al., 1979]
Wolfgang Coy, Claudio Moraga, Friedrich Abraham, Angelika Beese, Werner Bielefeld, Magdalena Bonsiepen, Martin Gogolla, Michael Land, and Manfred Siebert. Adaptive und Lernende Systeme - Bericht einer Projektgruppe Wintersemester 1978 - Sommersemester 1979. Interne Berichte und Skripten, Universität Dortmund, Abteilung Informatik, 1979.
In der Projektgruppe ``Adaptive und Lernende Systeme'' wollten die Veranstalter eine Möglichkeit anbieten, das Problem des Lernens im Gebiet der formalen Sprachinferenz zu untersuchen. Nach einer einheitlichen Verarbeitung von Grundbeiträgen aus der Literatur ist die Gruppe in der Lage, sich mit Inferenzalgorithmen zu beschäftigen, einige zu entwickeln, in Form eines Programms zu testen und zu bewerten. Schließlich bietet sich die Möglichkeit, Algorithmen für Inferenz über verschiedenen Sprachen der Chomsky-, Petri- oder Lindenmayer-Sprachfamilien weiter zu untersuchen.


Home|People|Teaching|Publications
Last change: 22.06.2017