1 Mission Theorem-prover based Testing with HOL-TestGen (Extended Abstract) (2009)
Achim D. Brucker, Burkhart Wolff
and software testing. As far as symbolic verification methods and modelbased testing techniques are concerned, the interest among researchers in the mutual fertilization of these fields is growing....
• Formalizing Class Diagrams (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
• Embedding OCL into Isabelle/HOL • Conclusion
Proof Environments for Formal Specification Languages (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Winter Term, Achim D. Brucker
Isabelle is not alone there are many successful theorem provers, e.g.: • Coq:
Metamodel-based UML Notations for Domain-specific Languages (2008)
Achim D. Brucker, Jürgen Doser
Abstract We present a metamodel-based approach for specifying uml notations for domain-specific modeling languages. Traditionally, domain specific languages are either defined by uml profiles or...
Extensible Object-oriented Data Models in Isabelle/HOL (2008)
Achim D. Brucker, Burkhart Wolff
Abstract We present an extensible encoding of object-oriented data models into higher-order logic (HOL). Our encoding is supported by a datatype package that enables the use of the shallow embedding...
Semantic Issues of OCL: Past, Present, and Future (2008)
Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Dan Chiorean, Birgit Demuth, ...
Abstract: We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...
HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2008)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
An MDA Framework Supporting OCL (2008)
Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Tiziana Margaria, Julia Padberg, ...
Abstract: We present a model-driven architecture (MDA) framework that integrates formal analysis techniques into an industrial software development process model. This comprises modeling using...
Metamodel-based UML Notations for Domain-specific Languages (2008)
Achim D. Brucker, Jürgen Doser
Abstract We present a metamodel-based approach for specifying uml notations for domain-specific modeling languages. Traditionally, domain specific languages are either defined by uml profiles or...
Achim D. Brucker, A Software, Engineering Problem
▸ Software systems ▸ are becoming more and more complex. ▸ used in safety and security critical applications. ▸ Formal methods are one way to ensure the correctness. ▸ But, formal methods...
A Software Engineering Problem ▸ Software systems ▸ are becoming more and more complex. ▸ used in safety and security critical applications. ▸ Formal methods are one way to ensure the...
Semantic Issues of OCL: Past, Present, and Future (2008)
Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Dan Chiorean, Birgit Demuth, ...
Abstract: We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...
Abstract A Case Study of a Formalized Security Architecture (2008)
Achim D. Brucker, Eth Zürich, Burkhart Wolff
CVS is a widely known version management system, which can be used for the distributed development of software as well as its distribution from a central database. In this paper, we provide an...
Achim D. Brucker, Burkhart Wolff
The date of receipt and acceptance will be inserted by the editor Abstract. We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by...
An MDA Framework Supporting OCL (2008)
Ocl For (meta-)models, Achim D. Brucker, Jürgen Doser, Burkhart Wolff, Tiziana Margaria, Julia Padberg, ...
Abstract: We present a model-driven architecture (MDA) framework that integrates formal analysis techniques into an industrial software development process model. This comprises modeling using...
Abstract A Case Study of a Formalized Security Architecture (2007)
Achim D. Brucker, Eth Zürich, Burkhart Wolff
CVS is a widely known version management system, which can be used for the distributed development of software as well as its distribution from a central database. In this paper, we provide an...
HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2007)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
Technical Report 157 Checking OCL Constraints in Distributed Component Based Systems (2007)
Achim D. Brucker, Burkhart Wolff
We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...
Achim D. Brucker, Burkhart Wol
CVS is a widely known version management system, which can be used for the distributed development of software as well as its distribution from a central database. In this paper, we provide an...
Test-sequence generation with HOL-TestGen – with an application to firewall testing (2007)
Achim D. Brucker, Burkhart Wolff
Abstract HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is...
Test-sequence generation with HOL-TestGen – with an application to firewall testing (2007)
Achim D. Brucker, Burkhart Wolff
Abstract HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is...
Software systems are becoming more and more complex and are used in safety and security critical applications. Formal methods are one way to increase their reliability. But, formal methods are hardly...
A Software Engineering Problem (2007)
▸ Software systems ▸ are becoming more and more complex.
Contributions Contributions (2007)
We formalize uml/ocl and provide tool support Our solution is formal Our solution is based on a standard widely used in industry Our solution has tool support
A Model Transformation Semantics and Analysis Methodology for SecureUML (2006)
Achim D. Brucker, Burkhart Wolff
Abstract SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a uml notation in terms of a uml profile, and can be combined...
Model-driven constraint engineering (2006)
Michael Wahler, Jana Koehler, Achim D. Brucker
Abstract. A high level of detail and well-formedness of models have become crucial ingredients in model-driven development. Constraints play a central role in model precision and validity. However,...
Model-driven constraint engineering (2006)
Tiziana Margaria, Julia Padberg, Gabriele Taentzer, Michael Wahler, Michael Wahler, Jana Koehler, ...
Abstract: Precise specification of meta-models is an important prerequisite for the successful application of a model-driven engineering (MDE) process. One means of precise specification are textual...
Achim D. Brucker, Joint Work, Jürgen Doser, Burkhart Wolff, A St, Ard Compliant, ...
The semantics of ocl 2.0 is spread over several places: Chapter 7 “ocl Language Description ” (informative): introduces ocl informally using examples, Chapter 10 “Semantics Described using uml...
An MDA Framework Supporting OCL (2006)
Achim D. Brucker, Jürgen Doser, Burkhart Wolff
Abstract We present an mda framework, developed in the functional programming language sml, that tries to bridge the gap between formal software development and the needs of industrial software...
Semantic issues of ocl: Past, present, and future (2006)
Achim D. Brucker, Jürgen Doser, Burkhart Wolff
Abstract We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized,...
A package for extensible object-oriented data models with an application to imp (2006)
Achim D. Brucker, Burkhart Wolff
with an Application to IMP++
Achim D. Brucker, Burkhart Wolff, Burkhart Wolff
Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies. Permission is granted to copy and...
Achim D. Brucker, Jürgen Doser, Burkhart Wolff
The semantics of ocl 2.0 is spread over several places: Chapter 7 “ocl Language Description ” (informative): introduces ocl informally using examples, Chapter 10 “Semantics Described using uml...
A Model Transformation Semantics and Analysis Methodology for SecureUML (2006)
Achim D. Brucker, Achim D. Brucker, Jürgen Doser, Jürgen Doser, Burkhart Wolff, Burkhart Wolff
Abstract SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a uml notation in terms of a uml profile, and can be combined...
A package for extensible object-oriented data models with an application to imp (2006)
Achim D. Brucker, Burkhart Wolff
We present a datatype package that enables the use of shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented...
Model-driven constraint engineering (2006)
Michael Wahler, Jana Koehler, Achim D. Brucker
Abstract. A high level of detail and well-formedness of models have become crucial ingredients in model-driven development. Constraints play a central role in model precision and validity. However,...
• Formalizing Class Diagrams (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Well-founded Orders
◦ Z and Data-Refinement,
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Scons X Y
We are still looking at how the different parts of mathematics are encoded in the Isabelle/HOL library.
Higher-Order Logic (HOL) is: (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, David Basin
Higher-Order Logic (HOL) is: • an expressive foundation for mathematics: analysis, algebra,... computer science: program correctness, hardware verification,...
HOL-TestGen 1.0.0 user guide (2005)
Achim D. Brucker, Burkhart Wolff, Burkhart Wolff
Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies. Permission is granted to copy and...
Symbolic test case generation for primitive recursive functions (2005)
Achim D. Brucker, Burkhart Wolff
Abstract We present a method for the automatic generation of test cases for HOL formulae containing primitive recursive predicates. These test cases can be used for the animation of specifications as...
Information Security Eth, W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, ...
specification of standard data structures (e.g. lists, sets) are stepwise refined to a concrete implementation. Security: access control (PAM authentication with iButton) Analysis of the state...
Why use Formal Methods in Software Development (2004)
W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, ...
Software systems are
W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, ...
safety critical applications, e.g. flight or railway control. security critical applications, e.g. access control. financial reasons (e.g. warranty), e.g. embedded devices. legal reasons, e.g....
Using theory morphisms for implementing formal methods tools (2003)
Achim D. Brucker, Burkhart Wol
Abstract Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed meta-logic, which allows their safe...
A case study of a formalized security architecture (2003)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
These days, the Concurrent Versions System (CVS) is a widely used tool for version management in many industrial software development projects, and plays a key role in open source projects usually...
A case study of a formalized security architecture (2003)
Achim D. Brucker, Frank Rittinger, Burkhart Wol
These days, the Concurrent Versions System (CVS) is a widely used tool for version management in many industrial software development projects, and plays a key role in open source projects usually...
A case study of a formalized security architecture (2003)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
These days, the Concurrent Versions System (CVS) is a widely used tool for version management in many industrial software development projects, and plays a key role in open source projects usually...
Using theory morphisms for implementing formal methods tools (2003)
Achim D. Brucker, Burkhart Wolff
Abstract Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed meta-logic, which allows their safe...
Proof Environment For, Achim D. Brucker, Frank Rittinger, Burkhart Wol, ...
We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the embedding,...
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wol
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wolff
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wol
Abstract: We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the...
HOL-OCL: Experiences, Consequences and Design Choices (2002)
Achim D. Brucker, Burkhart Wolff
Abstract Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [1], we explore several key issues of the design of a formal semantics of the OCL....
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wolff
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
HOL-OCL: Experiences, Consequences and Design Choices (2002)
Achim D. Brucker, Burkhart Wolff
Abstract Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [1], we explore several key issues of the design of a formal semantics of the OCL....
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wolff
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
Abstract: We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the...
Proof Environment For, Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wol
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wol# Albert-Ludwigs-Universitat Freiburg {brucker,friedric,rittinge,wolff}@informatik.uni-freiburg.de 1
A Note on Design Decisions of Formalization of the OCL - The View Freiburg (2002)
Achim D. Brucker, Burkhart Wolff
We compare several formal and informal approaches define the semantics the Object Constraint Language (OCL) [22]. This comparison reveals a number minor and major design problems settled upcoming...
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
Abstract: We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the...
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wolff
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
Technical Report 182 A CVS-Server Security Architecture Concepts and Formal Analysis (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
We would like to thank Nicole Rauch (Uni Kaiserslautern) for many valuable comments
A Note on Design Decisions of a Formalization of the OCL — The View of Freiburg — (2002)
Achim D. Brucker, Burkhart Wolff
We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL) [22]. This comparison reveals a number of minor and major design problems to be...
HOL-OCL: Experiences, Consequences and Design Choices (2002)
Achim D. Brucker, Burkhart Wolff
Abstract Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [1], we explore several key issues of the design of a formal semantics of the OCL....
-- Concepts and Formal Analysis (2002)
Achim D. Brucker, Frank Rittinger, Burkhart Wolff
This is based on a refinement, mapping a system architecture on an implementation architecture abstractly describing CVS in our implementation. The system architecture describes the abstract system...
A proposal for a formal OCL semantics in Isabelle/HOL (2002)
Achim D. Brucker, Burkhart Wolff
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within...
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly devided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
HOL-OCL: Experiences, Consequences and Design Choices (2002)
Achim Brucker And, Achim D. Brucker, Burkhart Wol
Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [1], we explore several key issues of the design of a formal semantics of the OCL. These...
Testing distributed component based systems using UML/OCL (2001)
Achim D. Brucker, Burkhart Wolff
We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...
Testing Distributed Component Based Systems Using UML/OCL (2001)
Achim Brucker Burkhart, Achim D. Brucker, Burkhart Wolff
We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...
Testing distributed component based systems using UML/OCL (2001)
Achim D. Brucker, Burkhart Wolff
We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...
Technical Report 157 Checking OCL Constraints in Distributed Component Based Systems (2001)
Achim D. Brucker, Burkhart Wolff
We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for runtime...
Component Based Systems (2001)
Achim D. Brucker, Burkhart Wolff
Abstract We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for...
Testing distributed component based systems using UML/OCL (2001)
Achim D. Brucker, Burkhart Wolff
Abstract We present a pragmatic approach using formal methods to increase the quality of distributed component based systems: Based on UML class diagrams annotated with OCL constraints, code for...