%%% ==================================================================== %%% @BibTeX-source-file{ %%% filename = "brucker.bib", %%% date = "Thu Apr 19 08:45:21 CEST 2012", %%% author = "Achim D. Brucker", %%% URL = "http://www.brucker.ch/", %%% source = "http://www.brucker.ch/bibliography/bib/brucker.bib", %%% abstract = "This BibTeX database contains the publication of %%% Achim D. Brucker.", %%% copyright = "Copyright 2001-2011 Achim D. Brucker", %%% license = "Unlimited copying and redistribution of this file %%% are permitted as long as this file is not %%% modified. Modifications, and distribution of %%% modified versions, are permitted, but only if %%% the resulting file is renamed.", %%% } %%% ==================================================================== @MastersThesis{ brucker:verifikation:2000, bibkey = {brucker:verifikation:2000}, language = {german}, author = {Achim D. Brucker}, title = {{Verifikation von Dividierern mit Word-Level-Decision-Diagrams}}, school = {{Albert-Ludwigs-Universit{\"a}t Freiburg}}, month = apr, year = {2000}, address = {Freiburg}, public = {yes}, type = {Diplomarbeit}, keywords = {formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division}, classification= {thesis}, areas = {formal methods, hardware}, pdf = {http://www.brucker.ch/bibliography/download/2000/diplomathesis.pdf}, abstract = {Late detection of design errors typically results in higher costs, therefore the importance of design verification and validation increases. This was especially shown in 1994 by the ``Pentium bug''. Since then the effort put into the verification of arithmetic circuits, particularly division, has increased.\\ In the area of the hardware verification decision diagrams are the most important data structures for the representation of boolean functions. However, in 1998 was shown that the representational power of any known decision diagram ist too weak to efficiently represent division.\\ In this work a new approach for the verification of divider circuits is introduced, which by a transformation avoids the representation of the division operation as decision diagram. With this approach it was the first time possible to verify the nonrestoring division automatically only by the application of decision diagrams.}, abstract_de = {Da die sp{\"a}te Entdeckung von Fehlern in einem Schaltkreisdesign hohe Kosten verursacht, nimmt die Bedeutung der Verifikation und Validierung zu. Deutlich wurde dies 1994 mit dem \glqq Pentium Bug\grqq. Seit dieser Zeit werden verst{\"a}rkt Verfahren zur Verifikation von arithmetischen Schaltkreisen, insbesondere der Division, untersucht. \\ Im Bereich der Hardwareverifikation sind Entscheidungsdiagramme die wichtigsten Datenstrukturen zur Repr{\"a}sentation boolescher Funktionen. Allerdings konnte 1998 gezeigt werden, dass die Berechnungsst{\"a}rke der bekannten Entscheidungsdiagramme nicht ausreicht, um die Division effizient darstellen zu k{\"o}nnen.\\ In dieser Arbeit wird ein neuer Ansatz zur Verifikation von Dividiererschaltkreisen vorgestellt, bei dem durch eine Transformation vermieden wird, die Division als Entscheidungsdiagramm darstellen zu m{\"u}ssen. Mit diesem Verfahren ist erstmals eine vollst{\"a}ndig automatische Verifikation der nonrestoring Division nur durch den Einsatz von Entscheidungsdiagrammen m{\"o}glich.}, url = {http://www.brucker.ch/bibliography/abstract/brucker-verifikation-2000} } @Article{ brucker.ea:case:2003, author = {Achim D. Brucker and Burkhart Wolff}, title = {A Case Study of a Formalized Security Architecture}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {80}, note = {Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03)}, editor = {Thomas Arts and Wan Fokkink}, publisher = {Elsevier Science Publishers}, address = {Amsterdam}, location = {R{\o}ros, Norway}, year = {2003}, pages = {24--40}, language = {USenglish}, categories = {security,cvsserver}, classification= {workshop}, areas = {security, formal methods, software}, keywords = {security, access control, POSIX, Unix, CVS, Z}, abstract = {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 outline of a formal security analysis of a CVS-Server architecture performed in~\cite{brucker.ea:cvs-server:2002}. The analysis is based on an abstract architecture (enforcing a role-based access control on the repository), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as framework to formulate access control and confidentiality properties. Both the abstract as well as the concrete architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for some security properties. Thus, we present a case study for the security analysis of realistic models over an off-the-shelf system by formal machine-checked proofs.}, pdf = {http://www.brucker.ch/bibliography/download/2003/brucker.ea-case-2003.pdf}, doi = {10.1016/S1571-0661(04)80807-7}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-case-2003} } @TechReport{ brucker.ea:checking:2001, author = {Achim D. Brucker and Burkhart Wolff}, institution = {Albert-Ludwigs-Universit{\"a}t Freiburg}, language = {USenglish}, month = jul, title = {Checking {OCL} Constraints in Distributed Systems Using {J2EE/EJB}}, categories = {testing,holocl}, areas = {software}, classification= {unrefereed}, 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 runtime checking of components in J2EE/EJB is automatically generated. Thus, a UML--model for a component can be used in a black--box test for the component. Further we introduce different design patterns for EJBs, which are motivated by different levels of abstraction, and show that these patterns work smoothly together with our OCL constraint checking. A prototypic implementation of the code generator, supporting our design patterns with OCL support, has been integrated into a commercial software development tool.}, keywords = {OCL, Constraint checking, EJB, J2EE, Design by Contract, Design Pattern, Distributed Systems}, year = {2001}, number = {157}, num_pages = {46}, contributions = {Using OCL Constrains in a EJB environment and Design Patterns for EJBs.}, pdf = {http://www.brucker.ch/bibliography/download/2001/tr01.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-checking-2001} } @InCollection{ brucker.ea:cvs-server:2002, author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff}, categories = {security,cvsserver}, classification= {workshop}, areas = {security, formal methods, software}, title = {The {CVS}-Server Case Study: {A} Formalized Security Architecture}, editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, booktitle = {FM-TOOLS 2002}, year = {2002}, pages = {47--52}, month = jul, organization = {University Augsburg}, address = {Augsburg}, pdf = {http://www.brucker.ch/bibliography/download/2002/brucker.ea-cvs-server-2002.pdf}, language = {USenglish}, abstract = {CVS is a widely known version management system. Configured in server mode, it can be used for the distributed development of software as well as its distribution from a central database called the \emph{repository}. In this setting, a number of security mechanisms have to be integrated into the CVS-server architecture. We present an abstract formal model of the access control aspects of a CVS-server architecture enforcing a role-based access control on the data in the repository. This abstract architecture is refined to an implementation architecture, which represents (an abstraction of) a concrete CVS-server configuration running in a POSIX/UNIX environment. Both the abstract as well as the concrete architecture are specified in the language Z. The specification is compiled to HOL-Z, such that refinement proofs for this case study can be done in Isabelle/HOL.}, project = {FSA}, note = {Available as Technical Report, University Augsburg, number 2002--11.}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002} } @TechReport{ brucker.ea:cvs-server:2002-b, author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff}, institution = {Albert-Ludwigs-Universit{\"a}t Freiburg}, language = {USenglish}, number = {182}, categories = {security}, classification= {unrefereed}, areas = {security, formal methods, software}, title = {A {CVS-Server} Security Architecture --- Concepts and Formal Analysis}, abstract = {We present a secure architecture of a CVS-server, its implementation (i.e. mainly its configuration) and its formal analysis. Our CVS-server is uses cvsauth, that provides protection of passwords and protection of some internal data of the CVS repository. In contrast to other (security oriented) CVS-architectures, our approach allows the CVS-server run on an open filesystem, i.e. a filesystem where users can have direct access both by CVS-commands and by standard UNIX/POSIX commands such as \texttt{mv}. For our secure architecture of the CVS-server, we provide a formal specification and security analysys. The latter is based on a refinement mapping high-level security requirements on the architecture on low-level security mechanisms on the UNIX/POSIX filesystem level. The purpose of the formal analysis of the secure CVS-server architecture is twofold: First, it is the bases for the specification of mutual security properties such as non-repudiation, authentication and access control for this architecture. Second, the mapping of the architecture on standard security implementation technology is described. Thus, our approach can be seen as a method to give a formal underpinning for the usually tricky business of system administrators.}, keywords = {security architecture, Concurrent Versions System (CVS), Z, formal methods, refinement}, year = {2002}, num_pages = {100}, pdf = {http://www.brucker.ch/bibliography/download/2002/cvs_arch.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002-b} } @InCollection{ brucker.ea:embedding:2003, abstract = {Tools for a specification language can be implemented \emph{directly} (by building a special purpose theorem prover) or \emph{by a conservative embedding} into a typed meta-logic, which allows their safe and logically consistent implementation and the reuse of existing theorem prover engines. For being useful, the conservative extension approach must provide derivations for several thousand ``folklore'' theorems. In this paper, we present an approach for deriving the mass of these theorems mechanically from an existing library of the meta-logic. The approach presupposes a structured \emph{theory morphism} mapping library datatypes and library functions to new functions of the specification language while uniformly modifying some semantic properties; for example, new functions may have a different treatment of undefinedness compared to old ones.}, keywords = {Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL}, location = {Nijmegen}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Types for Proof and Programs}, language = {USenglish}, pages = {59--77}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {2646}, isbn = {3-540-14031-X}, editor = {Herman Geuvers and Freek Wiedijk}, pdf = {http://www.brucker.ch/bibliography/download/2003/brucker.ea-embedding-2003.pdf}, project = {CSFMDOS}, title = {Using Theory Morphisms for Implementing Formal Methods Tools}, doi = {10.1007/3-540-39185-1_4}, issn = {0302-9743}, categories = {holocl}, classification= {workshop}, areas = {formal methods}, year = {2003}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-embedding-2003} } @InCollection{ brucker.ea:hol-ocl:2002, abstract = {Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic~\cite{brucker.ea:proposal:2002}, we explore several key issues of the design of a formal semantics of the OCL. These issues comprise the question of the interpretation of invariants, pre- and postconditions, their transformation, an executable sub-language and the possibilities of refinement notions. A particular emphasize is put on the issue of mechanized deduction in UML/OCL specification.}, keywords = {OCL, Formal semantics, Constraint languages, Refinement, higher-order logic}, location = {Dresden}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {UML 2002: Model Engineering, Concepts and Tools}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {2460}, pages = {196--211}, editor = {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and Stephen Cook}, pdf = {http://www.brucker.ch/bibliography/download/2002/brucker.ea-hol-ocl-2002.pdf}, project = {CSFMDOS}, title = {{HOL-OCL}: Experiences, Consequences and Design Choices}, categories = {holocl}, doi = {10.1007/3-540-45800-X_17}, classification= {conference}, areas = {formal methods, software}, isbn = {3-540-44254-5}, issn = {0302-9743}, year = {2002}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2002} } @InCollection{ brucker.ea:hol-z:2002, author = {Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff}, title = {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications}, editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, booktitle = {FM-TOOLS 2002}, year = {2002}, pages = {33--38}, month = jul, organization = {University Augsburg}, address = {Augsburg}, pdf = {http://www.brucker.ch/bibliography/download/2002/fmtools_holz_02.pdf}, language = {USenglish}, abstract = {We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a \LaTeX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus and structural Z proofs.}, categories = {holz}, classification= {workshop}, areas = {formal methods, software}, note = {Available as Technical Report, University Augsburg, number 2002--11.}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2002} } @Article{ brucker.ea:hol-z:2003, 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 embedding, new proof support for the Z schema calculus and for proof structuring are developed. Thus, we integrate Z into a well-known and trusted theorem prover with advanced deduction technology such as higher-order rewriting, tableaux-based provers and arithmetic decision procedures. A further achievement of this work is the integration of our embedding into a new tool-chain providing a Z-oriented type checker, documentation facilities and macro support for refinement proofs; as a result, the gap has been closed between a logical embedding proven correct and a \emph{tool} suited for applications of non-trivial size.}, author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff}, journal = {Journal of Universal Computer Science}, language = {USenglish}, title = {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications}, volume = {9}, number = {2}, pages = {152--172}, month = feb, year = {2003}, pdf = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf}, keywords = {Theorem Proving, Refinement, Z}, copyright = {J.UCS}, copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2}, categories = {holz}, doi = {10.3217/jucs-009-02-0152}, issn = {0948-6968}, classification= {ejournal}, areas = {formal methods, software}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003} } @InCollection{ brucker.ea:proposal:2002, 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 the OMG; our work is an attempt to accompany this process by a proposal solving open questions in a consistent way and exploring alternatives of the language design. Moreover, our encoding gives the foundation for tool supported reasoning over OCL specifications, for example as basis for test case generation.}, keywords = {Isabelle, OCL, UML, shallow embedding, testing}, location = {Hampton, VA, USA}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, editor = {V{\'\i}ctor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and Sophi{\`e}ne Tahar}, language = {USenglish}, pdf = {http://www.brucker.ch/bibliography/download/2002/brucker.ea-proposal-2002.pdf}, filelabel = {Extended Version}, file = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic_extended.pdf}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {2410}, pages = {99--114}, project = {CSFMDOS}, doi = {10.1007/3-540-45685-6_8}, title = {A Proposal for a Formal {OCL} Semantics in {Isabelle/HOL}}, categories = {holocl}, classification= {conference}, areas = {formal methods, software}, isbn = {3-540-44039-9}, issn = {0302-9743}, year = {2002}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002} } @InProceedings{ brucker.ea:testing:2001, author = {Achim D. Brucker and Burkhart Wolff}, title = {Testing Distributed Component Based Systems Using {UML/OCL}}, language = {USenglish}, booktitle = {Informatik 2001}, pages = {608--614}, year = {2001}, editor = {K. Bauknecht and W. Brauer and Th. M{\"u}ck}, volume = {1}, number = {157}, series = {Tagungsband der GI/{\"O}CG Jahrestagung}, address = {Wien}, month = nov, organization = {{\"O}sterreichische Computer Gesellschaft}, 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 runtime checking of components in J2EE/EJB is automatically generated. Thus, a UML--model for a component can be used in a black--box test for the component. Further we introduce different design patterns for EJBs, which are motivated by different levels of abstraction, and show that these patterns work smoothly together with our OCL constraint checking. A prototypic implementation of the code generator, supporting our patterns with OCL support, has been integrated into a commercial software development tool.}, isbn = {3-85403-157-2}, pdf = {http://www.brucker.ch/bibliography/download/2001/info2001.pdf}, categories = {testing,holocl}, classification= {workshop}, areas = {software}, keywords = {Keywords: OCL, Constraint checking, EJB, J2EE, Design by Contract, Design pattern}, extended = {\cite{brucker.ea:checking:2001}.}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-testing-2001} } @TechReport{ brucker.ea:note:2002, author = {Achim D. Brucker and Burkhart Wolff}, institution = {Albert-Ludwigs-Universit{\"a}t Freiburg}, language = {USenglish}, month = jan, public = {yes}, title = {A Note on Design Decisions of a Formalization of the {OCL}}, abstract = {We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL). This comparison reveals a number of minor and major design problems to be settled in upcoming versions of the OCL standard. We review these problems in the context of our work of providing a formal semantics of OCL through an conservative embedding in HOL using the Isabelle theorem prover.}, keywords = {UML, OCL, formal semantics, HOL, Isabelle}, categories = {holocl}, classification= {unrefereed}, areas = {formal methods, software}, year = {2002}, number = {168}, pdf = {http://www.brucker.ch/bibliography/download/2002/ocl_note.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-note-2002} } @TechReport{ brucker.ea:symbolic:2004, author = {Achim D. Brucker and Burkhart Wolff}, institution = {ETH Zurich}, language = {USenglish}, month = jun, title = {Symbolic Test Case Generation for Primitive Recursive Functions}, categories = {testing,holtestgen}, classification= {unrefereed}, myareas = {formal methods, software}, abstract = {We present a method for the automatic generation of test cases for HOL formulae containing primitive recursive predicates. These test cases may be used for the animation of specifications as well as for black-box-testing of external programs. Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (CNF). Second, the test cases are analyzed for ground instances satisfying the premises of the clauses. Particular emphasis is put on the control of test hypothesis' and test hierarchies to avoid intractability. We applied our method to several examples, including AVL-trees and the red-black implementation in the standard library from SML/NJ.}, keywords = {symbolic test case generations, black box testing, theorem proving, Isabelle/HOL}, year = {2004}, number = {449}, num_pages = {21}, pdf = {http://www.brucker.ch/bibliography/download/2004/brucker.ea-symbolic-2004.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2004} } @InCollection{ brucker.ea:symbolic:2005, 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 well as for black-box testing of external programs. Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (HCNF). Second, the test cases are analyzed for instances with constant terms satisfying the premises of the clauses. Particular emphasis is put on the control of test hypotheses and test hierarchies to avoid intractability. We applied our method to several examples, including AVL-trees and the red-black tree implementation in the standard library from SML/NJ. }, keywords = {symbolic test case generations, black box testing, theorem proving, Isabelle/HOL }, location = {Linz}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Formal Approaches to Testing of Software}, language = {USenglish}, pages = {16--32}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {3395}, isbn = {3-540-25109-X}, doi = {10.1007/b106767}, editor = {Jens Grabowski and Brian Nielsen}, pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-symbolic-2005.pdf}, project = {CSFMDOS}, title = {Symbolic Test Case Generation for Primitive Recursive Functions}, classification= {workshop}, areas = {formal methods, software}, categories = {holtestgen}, year = {2004}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2005} } @Article{ brucker.ea:verification:2005, author = {Achim D. Brucker and Burkhart Wolff}, title = {A Verification Approach for Applied System Security}, journal = {International Journal on Software Tools for Technology (STTT)}, year = {2005}, publisher = {Springer-Verlag}, address = {Heidelberg}, pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-verification-2005.pdf}, language = {USenglish}, keywords = {verification, security, access control, refinement, POSIX, CVS, Z }, classification= {journal}, areas = {security, formal methods, software}, issn = {1433-2779}, doi = {10.1007/s10009-004-0176-3}, volume = {7}, number = {3}, pages = {233--247}, abstract = {We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture. The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the \posix{} environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties. Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-verification-2005} } @TechReport{ brucker.ea:hol-testgen:2005, author = {Achim D. Brucker and Burkhart Wolff}, institution = {ETH Zurich}, language = {USenglish}, month = apr, title = {{HOL-TestGen} 1.0.0 User Guide}, categories = {testing,holtestgen}, classification= {unrefereed}, areas = {formal methods, software}, keywords = {symbolic test case generations, black box testing, theorem proving, Isabelle/HOL}, year = {2005}, number = {482}, num_pages = {50}, pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-hol-testgen-2005.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2005} } @TechReport{ brucker.ea:hol-testgen:2010, author = {Achim D. Brucker and Lukas Br{\"u}gger and Matthias P. Krieger and Burkhart Wolff}, institution = {ETH Zurich}, language = {USenglish}, month = apr, title = {{HOL-TestGen} 1.5.0 User Guide}, categories = {testing,holtestgen}, classification= {unrefereed}, areas = {formal methods, software}, keywords = {symbolic test case generations, black box testing, theorem proving, Isabelle/HOL}, year = {2010}, number = {670}, num_pages = {248}, pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-hol-testgen-2010.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2010} } @InCollection{ brucker.ea:interactive:2005, keywords = {symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing}, abstract = {HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant Isabelle/HOL\@. While there is considerable skepticism with regard to interactive theorem provers in testing communities, we argue that they are a natural choice for (automated) symbolic computations underlying systematic tests. This holds in particular for the development on non-trivial formal test plans of complex software, where some parts of the overall activity require inherently guidance by a test engineer. In this paper, we present the underlying methods for both black box and white box testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit test techniques in a logically consistent way. }, location = {Edinburgh}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Formal Approaches to Testing of Software}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {3997}, doi = {10.1007/11759744_7}, isbn = {3-540-25109-X}, editor = {Wolfgang Grieskamp and Carsten Weise}, pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf}, project = {CSFMDOS}, title = {Interactive Testing using {HOL}-{TestGen}}, classification= {workshop}, areas = {formal methods, software}, categories = {holtestgen}, year = {2005}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005} } @InCollection{ brucker.ea:transformation:2006, 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 with arbitrary design modeling languages. We present a semantics for SecureUML in terms of a model transformation to standard UML/OCL. The transformation scheme is used as part of an implementation of a tool chain ranging from front-end visual modeling tools over code-generators to the interactive theorem proving environment \holocl. The methodological consequences for an analysis of the generated \OCL formulae are discussed.}, keywords = {security, SecureUML, UML, OCL, HOL-OCL, model-transformation}, location = {Genova}, author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff}, booktitle = {{MoDELS} 2006: Model Driven Engineering Languages and Systems}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, doi = {10.1007/11880240_22}, number = {4199}, pages = {306--320}, editor = {Oscar Nierstrasz and Jon Whittle and David Harel and Gianna Reggio}, project = {CSFMDOS}, title = {A Model Transformation Semantics and Analysis Methodology for {SecureUML}}, categories = {holocl}, classification= {conference}, areas = {security, formal methods, software}, file = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006-b.pdf}, filelabel = {Extended Version}, year = {2006}, public = {yes}, pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006.pdf}, note = {An extended version of this paper is available as ETH Technical Report, no. 524.}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006} } @TechReport{ brucker.ea:transformation:2006-b, author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff}, institution = {ETH Zurich}, language = {USenglish}, title = {A Model Transformation Semantics and Analysis Methodology for {SecureUML}}, categories = {holocl}, classification= {unrefereed}, areas = {security, formal methods, software}, 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 with arbitrary design modeling languages. We present a semantics for SecureUML in terms of a model transformation to standard UML/OCL. The transformation scheme is used as part of an implementation of a tool chain ranging from front-end visual modeling tools over code-generators to the interactive theorem proving environment \holocl. The methodological consequences for an analysis of the generated \OCL formulae are discussed.}, keywords = {security, SecureUML, UML, OCL, HOL-OCL, model-transformation}, year = {2006}, number = {524}, public = {yes}, num_pages = {18}, pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006-b} } @InCollection{ brucker.ea:package:2006, author = {Achim D. Brucker and Burkhart Wolff}, title = {A Package for Extensible Object-Oriented Data Models with an Application to {IMP++}}, editor = {Abhik Roychoudhury and Zijiang Yang}, booktitle = {International Workshop on Software Verification and Validation (SVV 2006)}, year = {2006}, month = aug, address = {Seattle, USA}, pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf}, language = {USenglish}, abstract = {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 data model to a theory containing object-universes, constructors, and accessor functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for an object-oriented core-language called \IMPOO, for which correctness of a Hoare logic with respect to an operational semantics is proven.}, categories = {holocl}, public = {yes}, classification= {workshop}, areas = {formal methods, software}, keywords = {datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-package-2006} } @TechReport{ brucker.ea:hol-ocl-book:2006, author = {Achim D. Brucker and Burkhart Wolff}, institution = {ETH Zurich}, language = {USenglish}, title = {The {HOL-OCL} Book}, classification= {unrefereed}, areas = {formal methods, software}, categories = {holocl}, year = {2006}, number = {525}, abstract = {HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle. HOL-OCL defines a machine-checked formalization of the semantics as described in the standard for OCL 2.0. This conservative, shallow embedding of UML/OCL into Isabelle/HOL includes support for typed, extensible UML data models supporting inheritance and subtyping inside the typed lambda-calculus with parametric polymorphism. As a consequence of conservativity with respect to higher-order logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOL-OCL provides several derived calculi for UML/OCL that allow for formal derivations establishing the validity of UML/OCL formulae. Elementary automated support for such proofs is also provided top }, bibkey = {brucker.ea:hol-ocl-book:2006}, pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf}, keywords = {security, SecureUML, UML, OCL, HOL-OCL, model-transformation}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006} } @InCollection{ brucker.ea:test-sequence:2007, 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 partitioned into test cases by transformation into a normal form. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs. Although originally designed for black-box unit-tests, HOL-TestGen's underlying logic and deduction engine is powerful enough to be used in test-sequence generation, too. We develop the theory for test-sequence generation with HOL-TestGen and describe its use in a substantial case-study in the field of computer security, namely the black-box test of configured firewalls. }, keywords = {security, model-based testing, specification-based testing, firewall testing}, location = {Zurich}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {{TAP} 2007: Tests And Proofs}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {4454}, editor = {Bertrand Meyer and Yuri Gurevich}, project = {CSFMDOS}, title = {Test-Sequence Generation with {HOL-TestGen} -- With an Application to Firewall Testing }, categories = {holtestgen}, classification= {conference}, areas = {security, formal methods, software}, public = {yes}, year = {2007}, doi = {10.1007/978-3-540-73770-4_9}, pages = {149--168}, isbn = {978-3-540-73769-8}, pdf = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007} } @Article{ krieger.ea:objective-functions:2011, abstract = {We explore the potential of adding objective functions to OCL operation contracts. If an operation contract includes an objective function, the operation has the obligation to yield results that make the objective function assume an optimal value. Thus, an objective function expresses a preference among the possible operation results that conform to the postconditions of the operation contract and any class invariants. Objective functions strictly increase the expressiveness of OCL operation contracts. While objective functions arise naturally in application domains like operations research, we argue that objective functions are a useful general-purpose specification instrument and discuss several application examples. As tool support for operation contracts with objective functions, we present an animator for OCL operation contracts with optimization capabilities. We ensure tool interoperability by specifying objective functions in a UML profile.}, author = {Matthias P. Krieger and Achim D. Brucker}, title = {Extending OCL Operation Contracts with Objective Functions}, language = {USenglish}, public = {yes}, categories = {holocl}, classification= {ejournal}, areas = {formal methods, software}, year = {2011}, keywords = {OCL, UML, objective functions}, url = {http://www.brucker.ch/bibliography/abstract/krieger.ea-objective-functions-2011} , editor = {Jordi Cabot, Tony Clark, Manuel Clavel, Martin Gogolla}, issn = {1863-2122}, copyright = {ECEASST}, copyrighturl = {http://journal.ub.tu-berlin.de/eceasst/article/view/662}, journal = {Electronic Communications of the EASST}, volume = {44}, volumetitle = {Proceedings of the Workshop on OCL and Textual Modelling (OCL 2011)}, pdf = {http://www.brucker.ch/bibliography/download/2011/krieger.ea-objective-functions-2011.pdf} } @Article{ wahler.ea:model-driven:2006-b, 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, the task of constraint development is time-consuming and error-prone because constraints can be arbitrarily complex in real-world models.To overcome this problem, we propose a solution that we call model-driven constraint engineering. In our solution, we define constraint patterns, add structure and develop a taxonomy for them. The constraint patterns integrate into the UML meta-model. These computation-independent, parameterized patterns are transformed into platform-independent constraints by a model transformation. In addition, we show how our approach can be supported by a tool.}, author = {Michael Wahler and Jana Koehler and Achim D. Brucker}, language = {USenglish}, public = {yes}, classification= {ejournal}, areas = {software}, keywords = {constraint, pattern, model-driven engineering, UML, OCL}, title = {Model-Driven Constraint Engineering}, editor = {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos Warmer}, issn = {1863-2122}, volume = {5}, year = {2006}, journal = {Electronic Communications of the EASST}, copyright = {ECEASST}, copyrighturl = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/44} , pdf = {http://www.brucker.ch/bibliography/download/2006/wahler.ea-model-driven-2006-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/wahler.ea-model-driven-2006-b} } @Article{ brucker.ea:mda:2006-b, 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 development, e.g., code generation. Overall, our tool-chain provides support for software modeling using UML/OCL and guides the user from type-checking and model transformations to code generation and formal analysis of the UML/OCL model. We conclude with a report on our experiences in using a functional language for implementing MDA tools. }, author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff}, language = {USenglish}, public = {yes}, categories = {holocl}, classification= {ejournal}, areas = {security, formal methods, software}, keywords = {MDE , MDA , OCL, model transformation, code-generation, verification}, title = {An {MDA} Framework Supporting{ OCL}}, editor = {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos Warmer}, issn = {1863-2122}, volume = {5}, year = {2006}, journal = {Electronic Communications of the EASST}, copyright = {ECEASST}, copyrighturl = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/45} , pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-mda-2006-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-mda-2006-b} } @Article{ brucker.ea:semantic:2006-b, 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, machine-checked semantic basis for a theorem proving environment for OCL (as an example for an object-oriented specification formalism) which is as faithful as possible to the original informal semantics. We report on various (minor) inconsistencies of the OCL semantics, discuss the more recent attempt to align the OCL semantics with UML 2.0 and suggest several extensions which make, in our view, OCL semantics more fit for future extensions towards programming-like verifications and specification refinement, which are, in our view, necessary to make OCL more fit for future extensions. }, author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff}, language = {USenglish}, public = {yes}, categories = {holocl}, classification= {ejournal}, areas = {formal methods, software}, keywords = {HOL-OCL, UML/OCL, formal semantics}, title = {Semantic Issues of {OCL}: Past, Present, and Future}, editor = {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos Warmer}, issn = {1863-2122}, volume = {5}, year = {2006}, journal = {Electronic Communications of the EASST}, copyright = {ECEASST}, copyrighturl = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/46} , pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-semantic-2006-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-semantic-2006-b} } @PhDThesis{ brucker:interactive:2007, author = {Achim D. Brucker}, title = {An Interactive Proof Environment for Object-oriented Specifications}, school = {ETH Zurich}, year = {2007}, public = {yes}, month = mar, classification= {thesis}, areas = {formal methods, software}, categories = {holocl}, keywords = {OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL}, note = {ETH Dissertation No. 17097.}, abstract = {We present a semantic framework for object-oriented specification languages. We develop this framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions guarantees by construction the consistency of our formalization. Moreover, we show how our framework can be used to build an interactive proof environment, called HOL-OCL, for object-oriented specifications in general and for UML/OCL in particular. Our main contributions are an extensible encoding of object-oriented data structures in HOL, a datatype package for object-oriented specifications, and the development of several equational and tableaux calculi for object-oriented specifications. Further, we show that our formal framework can be the basis of a formal machine-checked semantics for OCL that is compliant to the OCL 2.0 standard. }, abstract_de = {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r objektorientierte Spezifikationen vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch die Beschr{\"a}nkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL f{\"u}r objektorientierte Spezifikationen im Allgemeinen und insbesondere f{\"u}r UML/OCL zu entwickeln. Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r objektorientierte Spezifikationen und die Entwicklung verschiedener Kalk{\"u}le f{\"u}r objektorientierte Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale, maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die konform zum Standard f{\"u}r OCL 2.0 ist.}, pdf = {http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007} } @InCollection{ brucker.ea:metamodel:2007, author = {Achim D. Brucker and J{\"u}rgen Doser}, title = {Metamodel-based UML Notations for Domain-specific Languages}, editor = {Jean Marie Favre and Dragan Gasevic and Ralf L{\"a}mmel and Andreas Winter}, booktitle = {4th International Workshop on Software Language Engineering (ATEM 2007)}, year = {2007}, month = oct, pdf = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-metamodel-2007.pdf}, address = {Nashville, USA}, language = {USenglish}, 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 using metamodels. We provide a generic integration of these two methods supporting arbitrary UML profiles and metamodels. Our approach provides a bi-directional mapping between the UML notation and the metamodel of the domain specific language. We use OCL constraints that are embedded into the metamodel, for describing the mapping between the UML notation and the metamodel. Moreover, we describe an implementation, as ArgoUML-plugin, for arbitrary SecureUML dialects.}, public = {yes}, classification= {workshop}, areas = {security, software}, keywords = {DSL, UML, OCL, UML Profile, Metamodel, MOF, SecureUML}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-metamodel-2007} } @InCollection{ brucker.ea:hol-ocl:2008, abstract = {We present the theorem proving environment HOL-OCL that is integrated in a MDE framework. HOL-OCL allows to reason over UMLclass models annotated with OCL specifications. Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. HOL-OCL provides several derived proof calculi that allow for formal derivations establishing the validity of UML/OCL formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.}, keywords = {HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement}, location = {Budapest, Hungary}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Fundamental Approaches to Software Engineering {(FASE08)}}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {4961}, doi = {10.1007/978-3-540-78743-3_8}, pages = {97--100}, editor = {Jos{\'e} Fiadeiro and Paola Inverardi}, title = {{HOL-OCL} -- {A Formal Proof Environment for {UML}/{OCL}}}, categories = {holocl}, classification= {conference}, areas = {formal methods, software}, year = {2008}, pdf = {http://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008} } @Article{ brucker.ea:verifying:2008, abstract = {HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/\acs{hol}. The HOL-TestGen method is two-staged: first, the original formula, called \emph{test specification}, is partitioned into \emph{test cases} by transformation into a normal form called \emph{test theorem}. Second, the test cases are analyzed for ground instances (the \emph{test data}) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs. As such, explicit test hypotheses establish a logical link between validation by test and by proof. Since HOL-TestGen generates explicit test hypotheses and makes them amenable to formal proof, the system is in a unique position to explore the relations between them at an example.}, keywords = {symbolic test case generations, black box testing, theorem proving, formal verification, Isabelle/HOL}, location = {Budapest, Hungary}, author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {220}, number = {1}, issn = {1571-0661}, note = {Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008)}, publisher = {Elsevier Science Publishers}, address = {Amsterdam}, language = {USenglish}, editor = {Bernd Finkbeiner and Yuri Gurevich and Alexander K. Petrenko}, title = {Verifying Test-Hypotheses: An Experiment in Test and Proof}, categories = {holtestgen}, pages = {15--27}, classification= {workshop}, areas = {formal methods, software}, year = {2008}, pdf = {http://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf}, public = {yes}, doi = {10.1016/j.entcs.2008.11.003}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008} } @InCollection{ brucker.ea:extensible:2008, abstract = {We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, and accessors functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for an object-oriented core-language called IMP++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven. }, location = {Paphos, Cyprus}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {ECOOP 2008 -- Object-Oriented Programming}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, doi = {10.1007/978-3-540-70592-5_19}, title = {Extensible Universes for Object-oriented Data Models}, categories = {holocl}, number = {5142}, pages = {438--462}, classification= {conference}, areas = {formal methods, software}, keywords = {object-oriented data models, HOL, formal methods, UML, OCL}, year = {2008}, editor = {Jan Vitek}, pdf = {http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008} } @InCollection{ brucker.ea:model-based:2008, abstract = {Firewalls are a cornerstone of todays security infrastructure for networks. Their configuration, implementing a firewall policy, is inherently complex, hard to understand, and difficult to validate. We present a substantial case study performed with the model-based testing tool HOL-TestGen. Based on a formal model of firewalls and their policies in HOL, we first present a derived theory for simplifying policies. We discuss different test plans for test specifications. Finally, we show how to integrate these issues to a domain-specific firewall testing tool HOL-TestGen/FW.}, editor = {Kenji Suzuki and Teruo Higashino}, location = {Tokyo, Japan}, author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff}, booktitle = {Testcom/FATES 2008}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {5047}, doi = {10.1007/978-3-540-68524-1_9}, pages = {103--118}, title = {Model-based Firewall Conformance Testing}, categories = {holtestgen}, classification= {conference}, areas = {security, formal methods}, keywords = {Security Testing, Model-based Testing, Firewall, Conformance Testing}, year = {2008}, pdf = {http://www.brucker.ch/bibliography/download/2008/brucker.ea-model-based-2008.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2008} } @Article{ brucker.ea:extensible:2008-b, abstract = {We present an extensible encoding of object-oriented data models into HOL. Our encoding is supported by a datatype package that leverages the use of the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model, i.e., a class model, to a theory containing object-universes, constructors, accessor functions, coercions (casts) between dynamic and static types, characteristic sets, and co-inductive class invariants. The package is conservative, i.e., all properties are derived entirely from constant definitions, including the constraints over object structures. As an application, we use the package for an object-oriented core-language called IMP++, for which we formally prove the correctness of a Hoare-Logic with respect to a denotational semantics.}, author = {Achim D. Brucker and Burkhart Wolff}, language = {USenglish}, public = {yes}, classification= {journal}, areas = {formal methods, software}, keywords = {object-oriented data models, HOL, theorem proving, verification}, title = {An Extensible Encoding of Object-oriented Data Models in HOL}, year = {2008}, journal = {Journal of Automated Reasoning}, volume = {41}, issue = {3}, pages = {219--249}, issn = {0168-7433}, doi = {10.1007/s10817-008-9108-3}, categories = {holocl}, publisher = {Springer-Verlag}, address = {Heidelberg}, pdf = {http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b} } @Article{ wahler.ea:efficient:2010, author = {Michael Wahler and David Basin and Achim D. Brucker and Jana Koehler}, title = {Efficient Analysis of Pattern-Based Constraint Specifications}, journal = {Software and Systems Modeling}, classification= {journal}, publisher = {Springer-Verlag}, address = {Heidelberg}, areas = {formal methods, software}, keywords = {UML, OCL, Constraints, Patterns, Consistency}, year = {2010}, abstract = {Precision and consistency are important prerequisites for class models to conform to their intended domain semantics. Precision can be achieved by augmenting models with design constraints and consistency can be achieved by avoiding contradictory constraints. However, there are different views of what constitutes a contradiction for design constraints. Moreover, state-of-the-art analysis approaches for proving constrained models consistent either scale poorly or require the use of interactive theorem proving. In this paper, we present a heuristic approach for efficiently analyzing constraint specifications built from constraint patterns. This analysis is based on precise notions of consistency for constrained class models and exploits the semantic properties of constraint patterns, thereby enabling syntax-based consistency checking in polynomial-time. We introduce a consistency checker implementing these ideas and we report on case studies in applying our approach to analyze industrial-scale models. These studies show that pattern-based constraint development supports the creation of concise specifications and provides immediate feedback on model consistency.}, public = {yes}, issn = {1619-1366}, volume = {9}, number = {2}, month = apr, doi = {10.1007/s10270-009-0123-6}, pages = {225--255}, pdf = {http://www.brucker.ch/bibliography/download/2010/wahler.ea-efficient-2010.pdf}, url = {http://www.brucker.ch/bibliography/abstract/wahler.ea-efficient-2010} } @Article{ brucker.ea:semantics:2009, author = {Achim D. Brucker and Burkhart Wolff}, title = {Semantics, Calculi, and Analysis for Object-oriented Specifications}, journal = {Acta Informatica}, classification= {journal}, areas = {formal methods, software}, keywords = {UML, OCL, object-oriented specification, refinement, formal methods}, abstract = {We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/HOL and the language is oriented towards OCL formulae in the context of UML class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.}, year = {2009}, language = {USenglish}, public = {yes}, issn = {0001-5903}, doi = {10.1007/s00236-009-0093-8}, categories = {holocl}, pages = {255--284}, month = jul, volume = {46}, number = {4}, publisher = {Springer-Verlag}, address = {Heidelberg}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-semantics-2009.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009} } @InCollection{ brucker.ea:hol-testgen:2009, abstract = {We present HOL-TestGen, an extensible test environment for specification-based testing build upon the proof assistant Isabelle. HOL-TestGen leverages the semi-automated generation of test theorems (a form of a partition), and their refinement to concrete test data, as well as the automatic generation of a test driver for the execution and test result verification. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit and sequence test techniques in a logically consistent way. }, keywords = {symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing}, location = {York, UK}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Fundamental Approaches to Software Engineering {(FASE09)}}, language = {USenglish}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {5503}, doi = {10.1007/978-3-642-00593-0_28}, pages = {417--420}, editor = {Marsha Chechik and Martin Wirsing}, title = {{HOL-TestGen}: An Interactive Test-case Generation Framework}, categories = {holtestgen}, classification= {conference}, areas = {formal methods, software}, year = {2009}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009} } @InCollection{ brucker.ea:extending:2009, author = {Achim D. Brucker and Helmut Petritsch}, title = {Extending Access Control Models with Break-glass}, booktitle = {ACM symposium on access control models and technologies (SACMAT)}, year = {2009}, isbn = {978-1-60558-537-6}, pages = {197--206}, publisher = {ACM Press}, address = {New York, NY, USA}, editor = {Barbara Carminati and James Joshi}, location = {Stresa, Italy}, doi = {10.1145/1542207.1542239}, abstract = {Access control models are usually static, i.e., permissions are granted based on a policy that only changes seldom. Especially for scenarios in health care and disaster management, a more flexible support of access control, i.e., the underlying policy, is needed. Break-glass is one approach for such a flexible support of policies which helps to prevent system stagnation that could harm lives or otherwise result in losses. Today, break-glass techniques are usually added on top of standard access control solutions in an ad-hoc manner and, therefore, lack an integration into the underlying access control paradigm and the systems' access control enforcement architecture. We present an approach for integrating, in a fine-grained manner, break-glass strategies into standard access control models and their accompanying enforcement architecture. This integration provides means for specifying break-glass policies precisely and supporting model-driven development techniques based on such policies.}, categories = {security}, copyright = {ACM}, copyrighturl = {http://dl.acm.org/authorize?175073}, classification= {conference}, areas = {security, software}, keywords = {disaster management, access-control, break-glass, model-driven security}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-extending-2009.pdf}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-extending-2009} } @InProceedings{ brucker.ea:delegation:2009, author = {Achim D. Brucker and Helmut Petritsch and Andreas Schaad}, title = {Delegation Assistance}, booktitle = {IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY)}, categories = {security}, year = {2009}, month = jul, classification= {conference}, areas = {security}, keywords = {delegation and revocation, policy enforcement, security services, security architecture}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, abstract = {Today's IT systems typically comprise a fine-grained access control mechanism based on complex policies. The strict enforcement of these policies, at runtime, always contains the risk of hindering people in their regular work. An efficient support for assisted delegation can help in resolving the conflict between too tight access control and the required flexibility as well as support the resolution of conflicts. Here, assisted delegation means that, additional to denying the access, a user is informed about a list of users that could either grant him access to the requested resource or which could execute this task in behalf of the user. In this paper, we present an approach for determining a set of users which are able to resolve an access control conflict. This set is based on various information sources and are ordered with respect to different distance functions. We show that one distance function can be used to serve different types of contextual input, e. g., role hierarchies, geospatial information as well as shared business object structure data or social network graphs.}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-delegation-2009.pdf}, doi = {10.1109/POLICY.2009.35}, pages = {84--91}, isbn = {978-0-7695-3742-9}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-delegation-2009} } @Article{ brucker.ea:modellierung:2009, author = {Achim D. Brucker and Andreas Schaad and Christian Wolter}, title = {{Prozessmodellierung}: {Einbinden} von {Sicherheitsregeln} in {Gesch\"aftsprozesse}}, journal = {iX}, year = {2009}, volume = {3}, classification= {popular}, areas = {security, software}, language = {german}, month = mar, pages = {118--121}, issn = {0935-9680}, publisher = {Heise Zeitschriften Verlag}, address = {Hannover, Germany}, public = {yes}, note_de = {Eine aktualisierte Version des Artikels ist im \glqq iX special -- Sicher im Netz\grqq{} (Oktober 2010) erschienen.}, note = {An updated version of this article was published in the \glqq iX special -- Sicher im Netz\grqq{} (October 2010).}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-modellierung-2009} } @Article{ brucker.ea:modellierung:2010, author = {Achim D. Brucker and Andreas Schaad and Christian Wolter}, title = {{Prozessmodellierung}: {Einbinden} von {Sicherheitsregeln} in {Gesch\"aftsprozesse}}, journal = {iX special -- Sicher im Netz}, year = {2010}, volume = {3}, classification= {popular}, areas = {security, software}, language = {german}, month = oct, pages = {152--155}, issn = {0935-9680}, publisher = {Heise Zeitschriften Verlag}, address = {Hannover, Germany}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-modellierung-2010} } @InCollection{ kohler.ea:proactive:2009, author = {Mathias Kohler and Achim D. Brucker and Andreas Schaad}, title = {{ProActive} {Caching}: Generating Caching Heuristics for Business Process Environments}, booktitle = {International Conference on Computational Science and Engineering (CSE)}, doi = {10.1109/CSE.2009.177}, pages = {207--304}, volume = {3}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, location = {Vancouver, Kandada}, year = {2009}, month = aug, classification= {conference}, abstract = {Today's complex and multi-layered enterprise systems demand fine-grained access control mechanisms supporting dynamic security policies for large and distributed repositories. Thus, the efficient evaluation of security policies becomes an important factor for the overall system performance, specifically with respect to systems with a high degree of user interaction like workflow systems. Caching approaches may help to address this situation. We propose ProActive Caching, a two-phased caching approach: in an offline phase, we automatically determine a workflow-specific heuristic for pre-computing cache entries. In an online phase, we use the previously determined heuristic for the cache management. The latter includes also the pre-computation of cache entries which already provides a performance improvement while evaluating a policy object for the first time. In this paper, we present a method for the automatic generation of a workflow specific caching heuristic, i.e., the offline phase.}, areas = {security}, keywords = {access control, proactive caching, process models}, public = {yes}, pdf = {http://www.brucker.ch/bibliography/download/2009/kohler.ea-proactive-2009.pdf}, url = {http://www.brucker.ch/bibliography/abstract/kohler.ea-proactive-2009} } @InCollection{ brucker.ea:integrating:2009, title = {Integrating Automated and Interactive Protocol Verification}, author = {Achim D. Brucker and Sebastian A. M{\"o}dersheim}, booktitle = {Workshop on Formal Aspects in Security and Trust (FAST 2009)}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {5983}, categories = {isabelleofmc}, pages = {248--262}, doi = {10.1007/978-3-642-12459-4_18}, editor = {Pierpaolo Degano and Joshua Guttman}, year = {2009}, classification= {workshop}, keywords = {protocol verification, model-checking, theorem proving}, areas = {security, formal methods}, public = {yes}, abstract = {A number of current automated protocol verification tools are based on abstract interpretation techniques and other over-approximations of the set of reachable states or traces. The protocol models that these tools employ are shaped by the needs of automated verification and require subtle assumptions. Also, a complex verification tool may suffer from implementation bugs so that in the worst case the tool could accept some incorrect protocols as being correct. These risks of errors are also present, but considerably smaller, when using an LCF-style theorem prover like Isabelle. The interactive security proof, however, requires a lot of expertise and time. We combine the advantages of both worlds by using the representation of the over-approx\-imated search space computed by the automated tools as a ``proof idea'' in Isabelle. Thus, we devise proof tactics for Isabelle that generate the correctness proof of the protocol from the output of the automated tools. In the worst case, these tactics fail to construct a proof, namely when the representation of the search space is for some reason incorrect. However, when they succeed, the correctness only relies on the basic model and the Isabelle core.}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf}, note = {An extended version of this paper is available as IBM Research Technical Report, RZ3750.}, filelabel = {Extended Version}, file = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009} } @TechReport{ brucker.ea:integrating:2009-b, title = {Integrating Automated and Interactive Protocol Verification (Extended Version)}, author = {Achim D. Brucker and Sebastian A. M{\"o}dersheim}, year = {2009}, classification= {unrefereed}, categories = {isabelleofmc}, keywords = {protocol verification, model-checking, theorem proving}, areas = {security, formal methods}, public = {yes}, abstract = {A number of current automated protocol verification tools are based on abstract interpretation techniques and other over-approximations of the set of reachable states or traces. The protocol models that these tools employ are shaped by the needs of automated verification and require subtle assumptions. Also, a complex verification tool may suffer from implementation bugs so that in the worst case the tool could accept some incorrect protocols as being correct. These risks of errors are also present, but considerably smaller, when using an LCF-style theorem prover like Isabelle. The interactive security proof, however, requires a lot of expertise and time. We combine the advantages of both worlds by using the representation of the over-approx\-imated search space computed by the automated tools as a ``proof idea'' in Isabelle. Thus, we devise proof tactics for Isabelle that generate the correctness proof of the protocol from the output of the automated tools. In the worst case, these tactics fail to construct a proof, namely when the representation of the search space is for some reason incorrect. However, when they succeed, the correctness only relies on the basic model and the Isabelle core.}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf}, number = {RZ3750}, institution = {IBM Research Zurich}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009-b} } @InCollection{ brucker.ea:ocl-null:2009, author = {Achim D. Brucker and Matthias P. Krieger and Burkhart Wolff}, wsbooktitle = {The Pragmatics of OCL and Other Textual Specification Languages}, note = {Selected best papers from all satellite events of the MoDELS 2009 conference.}, booktitle = {Models in Software Engineering}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {6002}, editor = {Sudipto Gosh}, pages = {261--275}, doi = {10.1007/978-3-642-12261-3_25}, language = {USenglish}, title = {Extending OCL with Null-References}, year = {2009}, classification= {workshop}, categories = {holocl}, location = {Denver, Colorado, USA}, areas = {formal methods, software}, public = {yes}, abstract = {From its beginnings, OCL is based on a strict semantics for undefinedness, with the exception of the logical connectives of type Boolean that constitute a three-valued propositional logic. Recent versions of the OCL standard added a second exception element, which, similar to the null references in object-oriented programming languages, is given a non-strict semantics. Unfortunately, this extension has been done in an ad hoc manner, which results in several inconsistencies and contradictions. In this paper, we present a consistent formal semantics (based on our HOL-OCL approach) that includes such a non-strict exception element. We discuss the possible consequences concerning class diagram semantics as well as deduction rules. The benefits of our approach for the specification-pragmatics of design level operation contracts are demonstrated with a small case-study.}, bibkey = {brucker.ea:ocl-null:2009}, pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.pdf}, keywords = {HOL-OCL, UML, OCL, null reference, formal semantics}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009} } @InCollection{ brucker.ea:efficient:2010, author = {Achim D. Brucker and Helmut Petritsch}, booktitle = {International Symposium on Engineering Secure Software and Systems (ESSoS)}, language = {USenglish}, editor = {F. Massacci and D. Wallach and N. Zannone}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, title = {Idea: Efficient Evaluation of Access Control Constraints}, year = {2010}, pages = {157--165}, number = {5965}, doi = {10.1007/978-3-642-11747-3_12}, isbn = {978-3-642-11746-6}, classification= {conference}, areas = {security, software}, public = {yes}, abstract = {Business requirements for modern enterprise systems usually comprise a variety of dynamic constraints, i.e., constraints that require a complex set of context information only available at runtime. Thus, the efficient evaluation of dynamic constraints, e.g., expressing separation of duties requirements, becomes an important factor for the overall performance of the access control enforcement. Especially in highly distributed systems, e.g., systems based on the service-oriented architecture (SOA) paradigm, the time for evaluating access control constraints depends significantly on the protocol between the central policy decision point (PDP) and the distributed policy enforcement points (PEP). In this paper, we present an policy-driven approach for generating customized protocol for the communication between the PDP and the pep. Moreover, we provide a detailed comparison of several approaches for querying context information during the evaluation of access control constraints.}, keywords = {distributed policy enforcement, XACML, access control}, pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-efficient-2010.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-efficient-2010} } @InCollection{ brucker.ea:information:2010, author = {Achim D. Brucker and Dieter Hutter}, booktitle = {International Conference on Availability, Reliability and Security (ARES)}, language = {USenglish}, title = {Information Flow in Disaster Management Systems}, year = {2010}, classification= {conference}, areas = {security}, public = {yes}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, pages = {156--163}, isbn = {978-0-7695-3965-2}, doi = {10.1109/ARES.2010.107}, abstract = {Collaborations between organizations in the public sector, e.g., fire brigades, polices, military units, is often done via liaison officers. A liaison officer liaises between two organizations by providing a single point of contact and ensuring the efficient communication and coordination of their activities. Usually an organization embeds a liaison officer in another organization to provide face-to-face coordination. Liaison officers demand special requirements to the security mechanism of the IT infrastructure of the organization that act as host for a liaison officer. This holds, in particular, for Disaster Management Information Systems (DMIS). Such systems need, on the one hand, to support various ways of communication in a flexible and ad hoc manner. On the other hand, these systems need to protect, by law, the leakage of sensitive data. In this paper, we present a novel mechanism, based on role-based access control (RBAC), for supporting the flexible and secure information exchange between organizations using liaison officers. Our mechanism enables liaison officers to decide on their own authority which information they wants share with their home organizations while allowing the host organization to limit the access of liaisons officers to their system in a fine-grained manner.}, keywords = {disaster management, information flow, access control, liaison officer}, pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-information-2010.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-information-2010} } @InCollection{ brucker.ea:firewall:2010, author = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney and Burkhart Wolff}, booktitle = {Third International Conference on Software Testing, Verification, and Validation (ICST)}, language = {USenglish}, title = {Verified Firewall Policy Transformations for Test-Case Generation}, year = {2010}, categories = {holtestgen}, classification= {conference}, areas = {security, formal methods}, public = {yes}, isbn = {978-0-7695-3990-4}, location = {Paris, France}, pages = {345--354}, doi = {10.1109/ICST.2010.50}, abstract = {We present an optimization technique for model-based generation of test cases for firewalls. Based on a formal model for firewall policies in higher-order logic, we derive a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/HOL. Finally, we use the normalized policies to generate test cases with the domain-specific firewall testing tool HOL-TestGen/FW. The resulting procedure is characterized by a gain in efficiency of two orders of magnitude and can handle configurations with hundreds of rules as occur in practice. Our approach can be seen as an instance of a methodology to tame inherent state-space explosions in test case generation for security policies.}, keywords = {security testing, model-based testing}, pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-firewall-2010.pdf}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-firewall-2010} } @InCollection{ brucker.ea:attribute-based:2010, author = {Achim D. Brucker and Helmut Petritsch and Stefan G. Weber}, booktitle = {Workshop In Information Security Theory And Practice (WISTP)}, fullbooktitle = {Information Security Theory and Practice. Security and Privacy of Pervasive Systems and Smart Devices}, language = {USenglish}, title = {Attribute-based Encryption with Break-glass}, year = {2010}, editor = {Pierangela Samarati and Michael Tunstall and Joachim Posegga}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, doi = {10.1007/978-3-642-12368-9_18}, number = {6033}, pages = {237--244}, abstract = {Attribute-based Encryption (ABE) allows for implementing fine-grained decentralized access control based on properties or attributes a user has. Thus, there is no need for writing detailed, user-based policies in advance. This makes ABE in particular interesting for implementing se- curity mechanisms in dynamic environments such as ubiquitous comput- ing, disaster management, or health-care. For supporting the latter two application areas, common ABE approaches lack one important feature: break-glass, i. e., the controlled overruling of access control restrictions. In this paper we present an integration of break-glass into an approach for end-to-end secure information sharing using ABE techniques.}, classification= {workshop}, areas = {security}, pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-attribute-based-2010.pdf}, public = {yes}, keywords = {access control, break-glass, attribute-based encryption, disaster management, trusted computing plattform}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-attribute-based-2010} } @InCollection{ altenhofen.ea:issues:2010, author = {Michael Altenhofen and Achim D. Brucker}, booktitle = {International Workshop on Formal Methods for Industrial Critical Systems (FMICS)}, language = {USenglish}, title = {Practical Issues with Formal Specifications: Lessons Learned from an Industrial Case Study}, year = {2010}, abstract = {Many software companies still seem to be reluctant to use formal specifications in their development processes. Nevertheless, the trend towards implementing critical business applications in distributed environments makes such applications an attractive target for formal methods. Additionally, the rising complexity also increases the willingness of the development teams to apply formal techniques. In this paper, we report on our experiences in formally specifying several core components of one of our commercially available products. While writing the formal specification, we experienced several issues that had a noticeable consequences on our work. While most of these issues can be attributed to the specific method and tools we have used, we do consider some of the problems as more general, impeding the practical application of formal methods, especially by non-experts, in large scale industrial development.}, keywords = {ASM, industrial case study, formal specification}, editor = {Stefan Kowalewski and Marco Roveri}, publisher = {Springer-Verlag}, address = {Heidelberg}, doi = {10.1007/978-3-642-15898-8_2}, series = {Lecture Notes in Computer Science}, number = {6371}, pages = {17--32}, pdf = {http://www.brucker.ch/bibliography/download/2010/altenhofen.ea-issues-2010.pdf}, classification= {workshop}, areas = {formal methods}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/altenhofen.ea-issues-2010} } @InCollection{ kohler.ea:caching:2010, author = {Mathias Kohler and Achim D. Brucker}, booktitle = {International Workshop on Security Measurements and Metrics (MetriSec)}, language = {USenglish}, title = {Caching Strategies: An Empirical Evaluation}, year = {2010}, copyright = {ACM}, copyrighturl = {http://dl.acm.org/authorize?399969}, classification= workshop, areas = {security, software}, public = {yes}, pdf = {http://www.brucker.ch/bibliography/download/2010/kohler.ea-caching-2010.pdf}, abstract = {Modern enterprise systems comprise a fine-grained enforcement of complex access control policies. Consequently, the efficient evaluation of security policies is a significant factor for the overall system performance. Moreover, modern enterprise systems are inherently based on process and workflow models. These models enable new approaches for improving the performance of security evaluations. Caching is widely used for improving the performance and the reliability of systems. The dynamic nature of today's workflow systems, both in terms of changing workflows and in terms of dynamic security policies impose particular challenges on the caching of access control decisions. We present a caching strategy that exploits business process models for avoiding cache misses. Moreover, we provide a detailed performance analysis of different caching strategies for static and dynamic aspects of access control policies, providing the required metrics for informed design decisions.}, isbn = {978-1-4503-0340-8}, pages = {1--8}, location = {Bolzano, Italy}, doi = {10.1145/1853919.1853930}, publisher = {ACM Press}, address = {New York, NY, USA}, url = {http://www.brucker.ch/bibliography/abstract/kohler.ea-caching-2010} } @InCollection{ brucker.ea:ocl-testing:2010, abstract = {Automated test data generation is an important method for the verification and validation of UML/OCL specifications. In this paper, we present an extension of DNF-based test case generation methods to cyclic class-diagrams and recursive query operations on them. A key feature of our approach is a implicit representation of object graphs avoiding a representation based on object-id's; thus, our approach avoids the generation of isomorphic object graphs by using a concise and still human-readable symbolic representation.}, author = {Achim D. Brucker and Matthias P. Krieger and Delphine Longuet and Burkhart Wolff}, booktitle = {MoDELS Workshops}, language = {USenglish}, public = {yes}, publisher = {Springer-Verlag}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, number = {6627}, classification= workshop, areas = {formal methods, software}, year = {2010}, note = {Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.}, categories = {holocl,holtestgen}, keywords = {OCL, UML, test case generation, specification-based testing}, pages = {334--348}, title = {A Specification-based Test Case Generation Method for {UML}/{OCL}}, editor = {J{\"u}rgen Dingel and Arnor Solberg}, isbn = {978-3-642-21209-3}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-testing-2010} , pdf = {http://www.brucker.ch/bibliography/download/2010/brucker.ea-ocl-testing-2010.pdf}, doi = {10.1007/978-3-642-21210-9_33} } @InProceedings{ brucker.ea:framework:2011, author = {Achim D. Brucker and Helmut Petritsch}, title = {A Framework for Managing and Analyzing Changes of Security Policies}, booktitle = {IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY)}, classification= {conference}, areas = {security}, year = {2011}, month = jun, abstract = {Modern enterprise systems need to comply to complex security policies. Due to legal regulations such as Basel II or HIPAA, the enforcement of these security policies needs to be carefully monitored and analyzed. The monitoring of complex and often dynamic access control requirements results in a vast amount of information that needs to be analyzed both in case of incidents and during regular audits. We present an extensible framework for managing and analyzing security policies during their whole life cycle. Our framework integrates versioning of policies and logfiles with policy animation, static analysis, and debugging techniques. For example, this combination allows for comparing different versions of security policies or the replaying and animation of system traces based on logfiles.}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, keywords = {security policies, versioning, runtime monitoring}, pdf = {http://www.brucker.ch/bibliography/download/2011/brucker.ea-framework-2011.pdf}, doi = {10.1109/POLICY.2011.47}, pages = {105--112}, isbn = {978-0-7695-4330-7/11}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-framework-2011} } @InProceedings{ braune.ea:service-oriented:2011, author = {Stephan Braune and Achim D. Brucker and Gerald Kleser and Keqin Li and Theo Dirk Meijler and Heiko Paulheim and Florian Probst}, title = {A Service-Oriented Architecture for Emergency Management Systems}, booktitle = {Software Engineering 2011 -- Workshopband}, note = {Innovative Systeme zur Unterst{\"u}tzung der zivilen Sicherheit: Architekturen und Gestaltungskonzepte.}, year = {2011}, editor = {Ralf Reussner and Alexander Pretschner and Stefan J{\"a}hnichen}, classification= {workshop}, month = feb, areas = {software}, url = {http://www.brucker.ch/bibliography/abstract/braune.ea-service-oriented-2011} , publisher = {GI}, address = {GI}, abstract = {The complexity and openness of today's modern societies result in the threat of serious cascading effects when natural disasters or terrorist attacks strike. Thus, there is a high demand for state of the art IT support in the field of emergency management systems. In this paper, we identify the core requirements of future emergency management systems and present a new generation of modular, service-oriented and semantic-web-based architecture for emergency management systems. Our emergency management system offers innovative functionality in the context of distributed information sources, collaborative work environments, and consistent situation pictures.}, pdf = {http://www.brucker.ch/bibliography/download/2011/braune.ea-service-oriented-2011.pdf}, series = {Lecture Notes in Informatics}, isbn = {978-3-88579-278-9}, volume = {P-184}, pages = {225--232}, public = {yes} } @InProceedings{ probst.ea:soknos:2010, title = {{SoKNOS} -- {I}nformationsdienste f{\"u}r das {K}atastrophenmanagement}, title_en = {{SoKNOS} -- Information Services Supporting Disaster Management}, author = {Florian Probst and Heiko Paulheim and Achim D. Brucker and Stefan Schulte}, year = {2010}, booktitle = {VDE-Kongress 2010 -- E-Mobility}, month = nov, location = {Congress Center Leipzig}, isbn = {978-3-8007-3304-0}, classification= {invited}, areas = {software}, public = {yes}, language = {german}, abstract = {Dieser Beitrag gibt einen {\"U}berblick {\"u}ber das vom BMBF gef{\"o}rderte Forschungsprojekt SoKNOS (Service-orientierte ArchiteKturen zur Unterst{\"u}tzung von Netzwerken im Rahmen {\"O}ffentlicher Sicherheit). Im SoKNOS Projekt wurden Konzepte entwickelt, die beteiligten Organisationen im Umfeld {\"o}ffentlicher Sicherheit im Katastrophenfall darin unterst{\"u}tzen, schnell und sicher agieren zu k{\"o}nnen. Dies beinhaltet unter anderem neue Methoden zur flexiblen Integration heterogener Informationen und Systeme, zur situations- und benutzergerechten Darstellung und Auswertung dieser Informationen, zum teilautomatisierten Austausch relevanter Nachrichten, zur Kooperation zwischen Organisationen und zum Dom{\"a}nen-spezifischen Design von IT-Sicherheitsmechanismen. In SoKNOS wurden die Forschungsbereiche IT-Sicherheit, Service-orientierte Architekturen (SOA), Arbeitsplatz der Zukunft und moderne Benutzerschnittstellen, Integration Geographischer Informationssysteme (GIS), sowie semantische Technologien adressiert. Im Folgenden werden exemplarisch Ergebnisse vorgestellt, welche durch die Kapselung einzelner Systemfunktionen in Dienste dazu beitragen, das Katastrophenmanagement flexibler und modularer zu gestalten.}, abstract_en = {In this paper, we provide an overview of the research project SoKNOS (Service-Oriented ArchiteCtures Supporting Networks of Public Security) which was funded by the German Federal Ministery of Education and Research (BMBF). The SoKNOS project developed concepts for IT systems supporting both public and private organizations in effectively and safely managing disasters and large incidents. This includes, among other things, the development of new methods for the flexible integration of heterogeneous information sources and legacy systems, the situation- and user-oriented presentation and analysis of the integrated information, the efficient exchange of information, and the efficient and secure cooperation between different organizations. SoKNOS particularly addressed the research areas IT security, ser- vice-oriented architectures (SOA), workplace of the future and modern user interface, integration of geographic information systems (GIS), and semantic technologies. In this paper, we will present exemplary results that, by providing an encapsulation of system functions into services, increase the modularity and flexibility of future disaster management solutions.}, pdf = {http://www.brucker.ch/bibliography/download/2010/probst.ea-soknos-2010.pdf}, publisherurl = {http://www.vde-verlag.de/proceedings-de/453304016.html}, url = {http://www.brucker.ch/bibliography/abstract/probst.ea-soknos-2010} } @InProceedings{ brucker.ea:model-based:2011, title = {An Approach to Modular and Testable Security Models of Real-world Health-care Applications}, author = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney and Burkhart Wolff}, booktitle = {ACM symposium on access control models and technologies (SACMAT)}, language = {USenglish}, publisher = {ACM Press}, address = {New York, NY, USA}, location = {Innsbruck, Austria}, categories = {holtestgen}, classification= {conference}, areas = {security, formal methods}, year = {2011}, copyright = {ACM}, copyrighturl = {http://dl.acm.org/authorize?431936}, public = {yes}, pages = {133--142}, pdf = {http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf}, abstract = {We present a generic modular policy modelling framework and instantiate it with a substantial case study for model-based testing of some key security mechanisms of applications and services of the NPfIT. NPfIT, the National Programme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the NHS in England. Consisting of heterogeneous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features. We model the four information governance principles, comprising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed envelopes and legitimate relationship. The model is given in HOL and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular emphasis is put on the modular description of security policies and their generic combination and its consequences for model-based testing.}, doi = {10.1145/1998441.1998461}, isbn = {978-1-4503-0688-1}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2011} } @Article{ brucker.ea:theorem-prover:2012, author = {Achim D. Brucker and Burkhart Wolff}, journal = {Formal Aspects of Computing}, publisher = {Springer-Verlag}, address = {Heidelberg}, language = {USenglish}, categories = {holtestgen}, title = {On Theorem Prover-based Testing}, year = {2012}, issn = {0934-5043}, classification= journal, areas = {formal methods, software}, public = {yes}, doi = {10.1007/s00165-012-0222-y}, keywords = {test case generation, domain partitioning, test sequence, theorem proving, HOL-TestGen}, abstract = {HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies. }, pdf = {http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf}, note = {To appear.}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012} } @InCollection{ marienfeld.ea:usdl-security:2012, author = {Florian Marienfeld and Edzard H{\"o}fig and Michele Bezzi and Matthias Fl{\"u}gge and Jonas Pattberg and Gabriel Serme and Achim D. Brucker and Philip Robinson and Stephen Dawson and Wolfgang Theilmann}, editor = {Alistair Barros and Daniel Oberle}, booktitle = {Handbook of Service Description: {USDL} and its Methods}, title = {Service levels, Security, and Trust}, chapter = {12}, isbn = {978-1-4614-1864-1}, pages = {295--326}, publisher = {Springer-Verlag}, address = {New York, NY, USA}, year = {2012}, doi = {10.1007/978-1-4614-1864-1_12}, classification= {invited}, areas = {security, software}, public = {yes}, abstract = {This chapter covers the scientific background for the Service Level Module of the Unified Service Description Language (USDL). In addition to general service level concepts, we expand on two specific service level fields: security and trust. For that end we first review the state of the art in service level modeling, then we explain the design of the Service Level Module and position it among the rest of USDL. For security, two possible perspectives, a high level business view and a low level engineering approach, are introduced. With regards to trust, USDL is suitable to specify how a service can be rated by its consumers and to ensure that ratings of competing services are comparable, and hence to determine trustworthiness. Additionally, we present a description of non-security-related elements that can be exploited for trust estimation. }, url = {http://www.brucker.ch/bibliography/abstract/marienfeld.ea-usdl-security-2012} } @InProceedings{ monakova.ea:securing:2012, author = {Ganna Monakova and Achim D. Brucker and Andreas Schaad}, title = {Security and Safety of Assets in Business Processes}, url = {http://www.brucker.ch/bibliography/abstract/monakova.ea-securing-2012} , booktitle = {ACM Symposium on Applied Computing (SAC)}, year = {2012}, classification= {conference}, areas = {software, security}, publisher = {ACM Press}, address = {New York, NY, USA}, abstract = {Business processes and service compositions are defined independent of the realizing systems. The visualization of security and safety constraints on the business process model level appears to be a promising approach to system independent specification of the security and safety requirements. Such requirements can be realized through business process annotation and used for communication or documentation, but they also can have an execution semantics that allows for automating the security and safety controls. In this paper, we present a tool-supported framework that extends modeling and execution of business processes with specification, execution and monitoring of the security and safety constraints that are used to protect business assets. We illustrate our approach on basis of a case study modeling a supply chain for perishable goods.}, public = {yes}, pdf = {http://www.brucker.ch/bibliography/download/2012/monakova.ea-securing-2012.pdf} } @InProceedings{ brucker.ea:securebpmn:2012, title = {{SecureBPMN}: Modeling and Enforcing Access Control Requirements in Business Processes}, author = {Achim D. Brucker and Isabelle Hang and Gero L{\"u}ckemeyer and Raj Ruparel}, booktitle = {ACM symposium on access control models and technologies (SACMAT)}, language = {USenglish}, publisher = {ACM Press}, address = {New York, NY, USA}, location = {Newark, USA}, classification= {conference}, areas = {security, software}, year = {2012}, copyright = {ACM}, mycopyrighturl= {http://dl.acm.org/authorize?}, public = {yes}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-securebpmn-2012} , pdf = {http://www.brucker.ch/bibliography/download/2012/brucker.ea-securebpmn-2012.pdf}, abstract = {Modern enterprise systems have to comply to regulations such as Basel III resulting in complex security requirements. These requirements need to be modeled at design-time and enforced at runtime. Moreover, modern enterprise systems are often business-process driven, i. e., the system behavior is described as high-level business processes that are executed by a business process execution engine. Consequently, there is a need for an integrated and tool-supported methodology that allows for specifying and enforcing compliance and security requirements for business process-driven enterprise systems. In this paper, we present a tool chain supporting both the design-time modeling as well as the run-time enforcement of security requirements for business process-driven systems.} } @Proceedings{ brucker.ea:tap:2012, editor = {Achim D. Brucker and Jacques Julliand}, title = {Tests and Proofs - 6th International Conference, TAP 2012, Praque, Czech Republic, Mai 31 -- June 1, 2012. Proceedings}, publisher = {Springer-Verlag}, address = {Heidelberg}, areas = {formal methods, software}, series = {Lecture Notes in Computer Science}, volume = {7305}, year = {2012}, isbn = {978-3-642-21767-8}, public = {yes}, classification= {editor}, url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-tap-2012} }