RoclET – A Tool for Wrestling with OCL Specifications (2008)
Cédric Jeanneret, Er Eyer, Thomas Baar
Abstract. In this paper, we describe the architecture and the functionality of our own OCL tool called RoclET 1. Besides standard features of OCL tools such as editing of class and object diagrams...
Noname manuscript No. (will be inserted by the editor) Semantics of OCL Specified with QVT ⋆ (2008)
The date of receipt and acceptance will be inserted by the editor Abstract The Object Constraint Language (OCL) has been for many years formalized both in its syntax and semantics in the language...
Alfred Strohmeier, Thomas Baar, Shane Sendall
The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exemplified on a case study, a...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
Tool support for OCL and related formalisms - needs and trends (2008)
Thomas Baar, Dan Chiorean, Re Correa, Martin Gogolla, Heinrich Hußmann, Octavian Patrascoiu, ...
Abstract. 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...
Refactoring OCL Annotated UML Class Diagrams (2008)
Marković, Slaviša, Baar, Thomas
Refactoring of UML class diagrams is an emerging research topic and heavily inspired by refactoring of program code written in objectoriented implementation languages. Current class diagram...
Thomas Baar, Und Reiner Hahnle
Abstract The main objectives of OCL are to restrict UML models by additional constraints and to clarify the denition of the UML meta model. For certain applications, however, it is crucial for the...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz
2, Wolfram Menzel 1, and Peter H. Schmitt 1 1
Thomas Baar, Bernd Fischer, Dirk Fuchs, Abt Softwaretechnologie, Tu Braunschweig, ...
Abstract. We describe a combination of the NORA/HAMMR software component retrieval tool and the ILF system which provides the necessary infrastructure to apply different first-order theorem provers...
Solving Software Reuse Problems with Theorem Provers (2007)
Thomas Baar, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Abstract. For a challenging application, the software component retrieval, we present a powerful solution by combining two systems. The NORA/HAMMR-tool handles all aspects concerning with the logical...
ILF and DAWN for Verifying Distributed Algorithms { An Idea for a Tool{ (2007)
Designing a proof in such a way that it can be automatically checked for correctness is a hard task. The task becomes even harder, if the proof should be intuitive and easily comprehensible. The...
Experiences with the UML/OCL-Approach in Practice and Strategies to Overcome Deciencies (2007)
Abstract. This paper is concerned with the practical usability of the Object Constraint Language (OCL). Pitfalls for untrained software developers are uncovered, and strategies for avoiding them are...
The Approach: Integrating Object Oriented Design and Formal Veri cation (2007)
Wolfgang Ahrendt Thomas, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
. This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verication. A distinctive feature of our approach is...
Solving Software Reuse Problems with Theorem Provers (2007)
Thomas Baar, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
In NORA/HAMMR, we investigate the application of automated theorem provers to retrieve software components based on their formal specifications. The problem pro le has major impacts on the problem...
Alfred Strohmeier, Thomas Baar, Shane Sendall
The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exemplified on a case study, a...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Thomas Baar, Bernhard Beckert, Peter H. Schmitt
Abstract. We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We...
Metamodels without Metacircularities (2007)
ABSTRACT. Although modeling languages as the UML (Unified Modeling Language) are primarily used in the context of software development, other application scenarios exist. A prominent example is the...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Synchronizing Refactored UML Class Diagrams and OCL Constraints (2007)
Marković, Slaviša, Baar, Thomas
UML class diagrams are usually annotated with OCL expressions that constrain their possible instantiation. In our work we have investigated how OCL annotations can be automatically updated each time...
On the usage of concrete syntax in model transformation rules (2007)
Abstract. Graph transformations are one of the best known approaches for defining transformations in model-based software development. They are defined over the abstract syntax of source and target...
On the usage of concrete syntax in model transformation rules (2007)
Thomas Baar, Thomas Baar, Jon Whittle, Jon Whittle
Abstract. Graph transformations are one of the best known approaches for defining model-to-model transformations in model-based software development. They are defined over the abstract syntax of...
OCL and Graph-Transformations – A Symbiotic Alliance to Alleviate the Frame Problem (2006)
Many popular methodologies are influenced by Design by Contract. They recommend to specify the intended behavior of operations in an early phase of the software development life cycle. Formal...
Definition and Correct Refinement of Operation Specifications (2006)
Baar, Thomas, Marković, Slaviša, Fondement, Frédéric, Strohmeier, Alfred
Modern incremental and iterative software engineering processes advocate to build software systems by first creating a highly simplified and abstract model of the system which is then moved by...
Correctly Defined Concrete Syntax for Visual Modeling Languages (2006)
The syntax of modeling languages is usually defined in two steps. The abstract syntax identifies modeling concepts whereas the concrete syntax clarifies how these modeling concepts are rendered by...
An OCL Semantics Specified with QVT (2006)
Marković, Slaviša, Baar, Thomas
Metamodeling became in the last decade a widely accepted tool to describe the (abstract) syntax of modeling languages in a concise, but yet precise way. For the description of the language's...
A Graphical Approach to Prove the Semantic Preservation of UML/OCL Refactoring Rules (2006)
Baar, Thomas, Marković, Slaviša
Refactoring is a powerful technique to improve the quality of software models including implementation code. The software developer applies successively so-called refactoring rules on the current...
RoclET – A Tool for Wrestling with OCL Specifications (2006)
Jeanneret, Cédric, Eyer, Leander, Marković, Slaviša, Baar, Thomas
In this paper, we describe the architecture and the functionality of our own OCL tool called RoclET. Besides standard features of OCL tools such as editing of class and object diagrams and parsing of...
RoclET– Refactoring OCL Expressions by Transformations (2006)
Jeanneret, Cédric, Eyer, Leander, Marković, Slaviša, Baar, Thomas
The role of UML models in software development has changed considerably over the last years. While UML was used in its early days mostly as a notation for sketching ideas, developers more and more...
On the Usage of Concrete Syntax in Model Transformation Rules (2006)
Graph transformations are one of the best known approaches for defining transformations in model-based software development. They are defined over the abstract syntax of source and target languages,...
A Graphical Approach to Prove the Semantic Preservation of UML/OCL Refactoring Rules (2006)
Baar, Thomas, Marković, Slaviša
Refactoring is a powerful technique to improve the quality of software models including implementation code. The software developer applies successively so-called refactoring rules on the current...
On the Usage of Concrete Syntax in Model Transformation Rules (2006)
Graph transformations are one of the best known approaches for defining model-to-model transformations in model-based software development. They are defined over the abstract syntax of source and...
A.: Definition and correct refinement of operation specification (2006)
Thomas Baar, Frédéric Fondement, Alfred Strohmeier, École Polytechnique
Abstract. Modern incremental and iterative software engineering processes advocate to build software systems by first creating a highly simplified and abstract model of the system which is then moved...
A Graphical Approach to Prove the Semantic (2006)
Thomas Baar, Refactoring Rules, Thomas Baar
Abstract. Refactoring is a powerful technique to improve the quality of software models including implementation code. The software developer applies successively so-called refactoring rules on the...
A graphical approach to prove the semantic preservation of UML/OCL refactoring rules (2006)
Abstract. Refactoring is a powerful technique to improve the quality of software models including implementation code. The software developer applies successively so-called refactoring rules on the...
An OCL Semantics Specified with QVT (2006)
Abstract. Metamodeling became in the last decade a widely accepted tool to describe the (abstract) syntax of modeling languages in a concise, but yet precise way. For the description of the...
Correctly defined concrete syntax for visual models (2006)
Abstract. The syntax of modeling languages is usually defined in two steps. The abstract syntax identifies modeling concepts whereas the concrete syntax clarifies how these modeling concepts are...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
OCL and Model Driven Engineering (2005)
Bézivin, Jean, Baar, Thomas, Gardner, Tracy, Gogolla, Martin, Hähnle, Reiner, Hussmann, Heinrich, ...
Precise modeling is essential to the success of the OMG's Model Driven Architecture initiative. At the modeling level (M1) OCL allows for the precision needed to write executable models. Can OCL be...
Non-deterministic Constructs in OCL -- What does any() Mean (2005)
The Object Constraint Language (OCL) offers so-called non-deterministic constructs which are often only poorly understood even by OCL experts. They are widely ignored in the OCL literature, their...
Refactoring OCL Annotated UML Class Diagrams (2005)
Marković, Slaviša, Baar, Thomas
Refactoring of UML class diagrams is an emerging research topic and heavily inspired by refactoring of program code written in object-oriented implementation languages. Current class diagram...
Making Metamodels Aware of Concrete Syntax (2005)
Fondement, Frédéric, Baar, Thomas
Language-centric methodologies, triggered by the success of Domain Specific Languages, rely on precise specifications of modeling languages. While the definition of the abstract syntax is...
OCL and Graph-Transformations – A Symbiotic Alliance to Alleviate the Frame Problem (2005)
Many popular methodologies are influenced by Design by Contract. They recommend to specify the intended behavior of operations in an early phase of the software development life cycle. In practice,...
This Technical Report comprises the final versions of the technical papers presented at the workshop 'Tool Support for OCL and Related Formalisms -- Needs and Trends' held in Montego Bay (Jamaica),...
Making Metamodels Aware of Concrete Syntax (2005)
Frédéric Fondement, Thomas Baar
Abstract. Language-centric methodologies, triggered by the success of Domain Specific Languages, rely on precise specifications of modeling languages. While the definition of the abstract syntax is...
Making Metamodels Aware of Concrete Syntax (2005)
Frédéric Fondement, Thomas Baar
Abstract. Language-centric methodologies, triggered by the success of Domain Specific Languages, rely on precise specifications of modeling languages. While the definition of the abstract syntax is...
OCL and graph transformations – a symbiotic alliance to alleviate the frame problem (2005)
Abstract. Many popular methodologies are influenced by Design by Contract. They recommend to specify the intended behavior of operations in an early phase of the software development life cycle. In...
Refactoring OCL Annotated UML Class Diagrams (2005)
Abstract. Refactoring of UML class diagrams is an emerging research topic and heavily inspired by refactoring of program code written in object-oriented implementation languages. Current class...
Refactoring OCL Annotated UML Class Diagrams (2005)
Abstract. Refactoring of UML class diagrams is an emerging research topic and heavily inspired by refactoring of program code written in object-oriented implementation languages. Current class...
Applying Fondue to Specify a Drink Vending Machine (2004)
Strohmeier, Alfred, Baar, Thomas, Sendall, Shane
The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exemplified on a case study, a...
UML 2004 - The Unified Modeling Language: Modeling Languages and Applications (2004)
Baar, Thomas, Strohmeier, Alfred, Moreira, Ana, Mellor, Stephen J.
In Formal Methods for Open Object-Based Distributed Systems (2004)
Abb Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
[AdB90] Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2):129– 162, 1990. [AdB94] Pierre America and Frank de Boer. Reasoning...
Applying Fondue to Specify a Drink Vending Machine (2003)
Strohmeier, Alfred, Baar, Thomas, Sendall, Shane
The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exempli ed on a case study, a Drink...
The Definition of Transitive Closure with OCL: Limitations and Applications (2003)
The Object Constraint Language (OCL) is based on first-order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the...
Applying Fondue to Specify a Drink Vending Machine (2003)
Strohmeier, Alfred, Baar, Thomas, Sendall, Shane
The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exemplified on a case study, a...
The Definition of Transitive Closure with OCL - Limitations and applications (2003)
The Object Constraint Language (OCL) is based on rst- order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the...
The Definition of Transitive Closure with OCL – Limitations and Applications (2003)
Abstract. The Object Constraint Language (OCL) is based on rstorder logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel....
The Definition of Transitive Closure with OCL – Limitations and Applications (2003)
Abstract. The Object Constraint Language (OCL) is based on firstorder logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel....
The KeY system: Integrating object-oriented design and formal methods (2002)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Elmar Habermalz, Wolfram Menzel, Wojciech Mostowski, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
How to ground meta-circular OCL descriptions – a set-theoretic approach (2002)
syntax of the Unied Modeling Language (UML) including the Object Constraint Language (OCL). In order to overcome inherent de-ciencies of meta-circular UML descriptions, the language MML based on an...
An Extension of Dynamic Logic (2001)
For Modelling Ocl's, Thomas Baar, Bernhard Beckert, Peter H. Schmitt
We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We extend this...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
An integrated metamodel for OCL types (2000)
Abstract The main objectives of OCL are to restrict UML models by additional constraints and to clarify the denition of the UML meta model. For certain applications, however, it is crucial for the...
The KEY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive...
Integrating deduction techniques in a software reuse application (1999)
Thomas Baar, Bernd Fischer, Dirk Fuchs
We investigate the application of automated deduction techniques to retrieve software components based on their formal specifications. The application profile has major impacts on the problem solving...
Verifying Intuition - ILF checks DAWN proofs (1999)
Thomas Baar, Ekkart Kindler, Hagen Völzer
The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal...
this article we investigate the service 'reliable data-transmission ' offered by DataLink-Layer. Realizing this service the DataLink-Layer can use only the service 'unreliable...
Semantics of OCL Specified with QVT
Marković, Slaviša, Baar, Thomas
The Object Constraint Language (OCL) has been for many years formalized both in its syntax and semantics in the language standard. While the official definition of OCL’s syntax is already widely...