TY - THES AU - Brucker, Achim D. PY - 2000/apr/ TI - Verifikation von Dividierern mit Word-Level-Decision-Diagrams PB - Albert-Ludwigs-Universität Freiburg CY - Freiburg KW - formal verification, binary decision diagrams, K*BMD, BDD, nonrestoring division N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker-verifikation-2000 L1 - http://www.brucker.ch/bibliography/download/2000/diplomathesis.pdf ID - brucker:verifikation:2000 U1 - Masters thesis ER - TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2003// TI - A Case Study of a Formalized Security Architecture JO - Electronic Notes in Theoretical Computer Science SP - 24 EP - 40 VL - 80 PB - Elsevier Science Publishers CY - Amsterdam KW - security, access control, POSIX, Unix, CVS, Z N2 - 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 \citebrucker.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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-case-2003 L1 - http://www.brucker.ch/bibliography/download/2003/brucker.ea-case-2003.pdf UR - http://dx.doi.org/10.1016/S1571-0661(04)80807-7 N1 - Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS?03) ID - brucker.ea:case:2003 ER - TY - RPRT AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2001/jul/ TI - Checking OCL Constraints in Distributed Systems Using J2EE/EJB IS - 157 PB - Albert-Ludwigs-Universität Freiburg KW - OCL, Constraint checking, EJB, J2EE, Design by Contract, Design Pattern, Distributed Systems N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-checking-2001 L1 - http://www.brucker.ch/bibliography/download/2001/tr01.pdf ID - brucker.ea:checking:2001 ER - TY - CHAP AU - Brucker, Achim D. AU - Rittinger, Frank AU - Wolff, Burkhart ED - Haneberg, Dominik ED - Schellhorn, Gerhard ED - Reif, Wolfgang PY - 2002/jul/ TI - The CVS-Server Case Study: A Formalized Security Architecture BT - FM-TOOLS 2002 SP - 47 EP - 52 CY - Augsburg N2 - 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 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002 L1 - http://www.brucker.ch/bibliography/download/2002/brucker.ea-cvs-server-2002.pdf N1 - Available as Technical Report, University Augsburg, number 2002?11. ID - brucker.ea:cvs-server:2002 ER - TY - RPRT AU - Brucker, Achim D. AU - Rittinger, Frank AU - Wolff, Burkhart PY - 2002// TI - A CVS-Server Security Architecture ? Concepts and Formal Analysis IS - 182 PB - Albert-Ludwigs-Universität Freiburg KW - security architecture, Concurrent Versions System (CVS), Z, formal methods, refinement N2 - 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 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002-b L1 - http://www.brucker.ch/bibliography/download/2002/cvs_arch.pdf ID - brucker.ea:cvs-server:2002-b ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Geuvers, Herman ED - Wiedijk, Freek PY - 2003// TI - Using Theory Morphisms for Implementing Formal Methods Tools BT - Types for Proof and Programs T3 - Lecture Notes in Computer Science SP - 59 EP - 77 IS - 2646 PB - Springer-Verlag CY - Heidelberg KW - Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL N2 - Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed meta-logic, which allows their safe 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 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. SN - 3-540-14031-X UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-embedding-2003 L1 - http://www.brucker.ch/bibliography/download/2003/brucker.ea-embedding-2003.pdf UR - http://dx.doi.org/10.1007/3-540-39185-1_4 ID - brucker.ea:embedding:2003 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Jézéquel, Jean-Marc ED - Hussmann, Heinrich ED - Cook, Stephen PY - 2002// TI - HOL-OCL: Experiences, Consequences and Design Choices BT - UML 2002: Model Engineering, Concepts and Tools T3 - Lecture Notes in Computer Science SP - 196 EP - 211 IS - 2460 PB - Springer-Verlag CY - Heidelberg KW - OCL, Formal semantics, Constraint languages, Refinement, higher-order logic N2 - Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic \citebrucker.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. SN - 3-540-44254-5 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2002 L1 - http://www.brucker.ch/bibliography/download/2002/brucker.ea-hol-ocl-2002.pdf UR - http://dx.doi.org/10.1007/3-540-45800-X_17 ID - brucker.ea:hol-ocl:2002 ER - TY - CHAP AU - Brucker, Achim D. AU - Friedrich, Stefan AU - Rittinger, Frank AU - Wolff, Burkhart ED - Haneberg, Dominik ED - Schellhorn, Gerhard ED - Reif, Wolfgang PY - 2002/jul/ TI - HOL-Z 2.0: A Proof Environment for Z-Specifications BT - FM-TOOLS 2002 SP - 33 EP - 38 CY - Augsburg N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2002 L1 - http://www.brucker.ch/bibliography/download/2002/fmtools_holz_02.pdf N1 - Available as Technical Report, University Augsburg, number 2002?11. ID - brucker.ea:hol-z:2002 ER - TY - JOUR AU - Brucker, Achim D. AU - Rittinger, Frank AU - Wolff, Burkhart PY - 2003/feb/ TI - HOL-Z 2.0: A Proof Environment for Z-Specifications JO - Journal of Universal Computer Science SP - 152 EP - 172 VL - 9 IS - 2 KW - Theorem Proving, Refinement, Z N2 - 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 tool suited for applications of non-trivial size. SN - 0948-6968 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003 L1 - http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf UR - http://dx.doi.org/10.3217/jucs-009-02-0152 ID - brucker.ea:hol-z:2003 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Carreño, Víctor A. ED - Muñoz, César A. ED - Tahar, Sophiène PY - 2002// TI - A Proposal for a Formal OCL Semantics in Isabelle/HOL BT - Theorem Proving in Higher Order Logics (TPHOLs) T3 - Lecture Notes in Computer Science SP - 99 EP - 114 IS - 2410 PB - Springer-Verlag CY - Heidelberg KW - Isabelle, OCL, UML, shallow embedding, testing N2 - 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. SN - 3-540-44039-9 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002 L1 - http://www.brucker.ch/bibliography/download/2002/brucker.ea-proposal-2002.pdf L1 - //www.brucker.ch/bibliography/download/2002/ocl_semantic_extended.pdf UR - http://dx.doi.org/10.1007/3-540-45685-6_8 ID - brucker.ea:proposal:2002 ER - TY - CONF AU - Brucker, Achim D. AU - Wolff, Burkhart A2 - Österreichische Computer Gesellschaft ED - Bauknecht, K. ED - Brauer, W. ED - Mück, Th PY - 2001/nov/ TI - Testing Distributed Component Based Systems Using UML/OCL BT - Informatik 2001 T3 - Tagungsband der GI/ÖCG Jahrestagung SP - 608 EP - 614 VL - 1 IS - 157 CY - Wien KW - Keywords: OCL, Constraint checking, EJB, J2EE, Design by Contract, Design pattern N2 - 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. SN - 3-85403-157-2 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-testing-2001 L1 - http://www.brucker.ch/bibliography/download/2001/info2001.pdf ID - brucker.ea:testing:2001 ER - TY - RPRT AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2002/jan/ TI - A Note on Design Decisions of a Formalization of the OCL IS - 168 PB - Albert-Ludwigs-Universität Freiburg KW - UML, OCL, formal semantics, HOL, Isabelle N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-note-2002 L1 - http://www.brucker.ch/bibliography/download/2002/ocl_note.pdf ID - brucker.ea:note:2002 ER - TY - RPRT AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2004/jun/ TI - Symbolic Test Case Generation for Primitive Recursive Functions IS - 449 PB - ETH Zurich KW - symbolic test case generations, black box testing, theorem proving, Isabelle/HOL N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2004 L1 - http://www.brucker.ch/bibliography/download/2004/brucker.ea-symbolic-2004.pdf ID - brucker.ea:symbolic:2004 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Grabowski, Jens ED - Nielsen, Brian PY - 2004// TI - Symbolic Test Case Generation for Primitive Recursive Functions BT - Formal Approaches to Testing of Software T3 - Lecture Notes in Computer Science SP - 16 EP - 32 IS - 3395 PB - Springer-Verlag CY - Heidelberg KW - symbolic test case generations, black box testing, theorem proving, Isabelle/HOL N2 - 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. SN - 3-540-25109-X UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-symbolic-2005 L1 - http://www.brucker.ch/bibliography/download/2005/brucker.ea-symbolic-2005.pdf UR - http://dx.doi.org/10.1007/b106767 ID - brucker.ea:symbolic:2005 ER - TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2005// TI - A Verification Approach for Applied System Security JO - International Journal on Software Tools for Technology (STTT) SP - 233 EP - 247 VL - 7 IS - 3 PB - Springer-Verlag CY - Heidelberg KW - verification, security, access control, refinement, POSIX, CVS, Z N2 - 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. SN - 1433-2779 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-verification-2005 L1 - http://www.brucker.ch/bibliography/download/2005/brucker.ea-verification-2005.pdf UR - http://dx.doi.org/10.1007/s10009-004-0176-3 ID - brucker.ea:verification:2005 ER - TY - RPRT AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2005/apr/ TI - HOL-TestGen 1.0.0 User Guide IS - 482 PB - ETH Zurich KW - symbolic test case generations, black box testing, theorem proving, Isabelle/HOL UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2005 L1 - http://www.brucker.ch/bibliography/download/2005/brucker.ea-hol-testgen-2005.pdf ID - brucker.ea:hol-testgen:2005 ER - TY - RPRT AU - Brucker, Achim D. AU - Brügger, Lukas AU - Krieger, Matthias P. AU - Wolff, Burkhart PY - 2010/apr/ TI - HOL-TestGen 1.5.0 User Guide IS - 670 PB - ETH Zurich KW - symbolic test case generations, black box testing, theorem proving, Isabelle/HOL UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-hol-testgen-2010.pdf ID - brucker.ea:hol-testgen:2010 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Grieskamp, Wolfgang ED - Weise, Carsten PY - 2005// TI - Interactive Testing using HOL-TestGen BT - Formal Approaches to Testing of Software T3 - Lecture Notes in Computer Science IS - 3997 PB - Springer-Verlag CY - Heidelberg KW - symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing N2 - 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. SN - 3-540-25109-X UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005 L1 - http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf UR - http://dx.doi.org/10.1007/11759744_7 ID - brucker.ea:interactive:2005 ER - TY - CHAP AU - Brucker, Achim D. AU - Doser, Jürgen AU - Wolff, Burkhart ED - Nierstrasz, Oscar ED - Whittle, Jon ED - Harel, David ED - Reggio, Gianna PY - 2006// TI - A Model Transformation Semantics and Analysis Methodology for SecureUML BT - MoDELS 2006: Model Driven Engineering Languages and Systems T3 - Lecture Notes in Computer Science SP - 306 EP - 320 IS - 4199 PB - Springer-Verlag CY - Heidelberg KW - security, SecureUML, UML, OCL, HOL-OCL, model-transformation N2 - 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 ØCL formulae are discussed. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006 L1 - //www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006-b.pdf L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006.pdf UR - http://dx.doi.org/10.1007/11880240_22 N1 - An extended version of this paper is available as ETH Technical Report, no. 524. ID - brucker.ea:transformation:2006 ER - TY - RPRT AU - Brucker, Achim D. AU - Doser, Jürgen AU - Wolff, Burkhart PY - 2006// TI - A Model Transformation Semantics and Analysis Methodology for SecureUML IS - 524 PB - ETH Zurich KW - security, SecureUML, UML, OCL, HOL-OCL, model-transformation N2 - 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 ØCL formulae are discussed. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006-b L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-transformation-2006-b.pdf ID - brucker.ea:transformation:2006-b ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Roychoudhury, Abhik ED - Yang, Zijiang PY - 2006/aug/ TI - A Package for Extensible Object-Oriented Data Models with an Application to IMP++ BT - International Workshop on Software Verification and Validation (SVV 2006) CY - Seattle, USA KW - datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-package-2006 L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf ID - brucker.ea:package:2006 ER - TY - RPRT AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2006// TI - The HOL-OCL Book IS - 525 PB - ETH Zurich KW - security, SecureUML, UML, OCL, HOL-OCL, model-transformation N2 - 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 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006 L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf ID - brucker.ea:hol-ocl-book:2006 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Meyer, Bertrand ED - Gurevich, Yuri PY - 2007// TI - Test-Sequence Generation with HOL-TestGen ? With an Application to Firewall Testing BT - TAP 2007: Tests And Proofs T3 - Lecture Notes in Computer Science SP - 149 EP - 168 IS - 4454 PB - Springer-Verlag CY - Heidelberg KW - security, model-based testing, specification-based testing, firewall testing N2 - 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. SN - 978-3-540-73769-8 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007 L1 - http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf UR - http://dx.doi.org/10.1007/978-3-540-73770-4_9 ID - brucker.ea:test-sequence:2007 ER - TY - JOUR AU - Krieger, Matthias P. AU - Brucker, Achim D. PY - 2011// TI - Extending OCL Operation Contracts with Objective Functions JO - Electronic Communications of the EASST VL - 44 KW - OCL, UML, objective functions N2 - 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. SN - 1863-2122 UR - http://www.brucker.ch/bibliography/abstract/krieger.ea-objective-functions-2011 L1 - http://www.brucker.ch/bibliography/download/2011/krieger.ea-objective-functions-2011.pdf ID - krieger.ea:objective-functions:2011 ER - TY - JOUR AU - Wahler, Michael AU - Koehler, Jana AU - Brucker, Achim D. PY - 2006// TI - Model-Driven Constraint Engineering JO - Electronic Communications of the EASST VL - 5 KW - constraint, pattern, model-driven engineering, UML, OCL N2 - 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. SN - 1863-2122 UR - http://www.brucker.ch/bibliography/abstract/wahler.ea-model-driven-2006-b L1 - http://www.brucker.ch/bibliography/download/2006/wahler.ea-model-driven-2006-b.pdf ID - wahler.ea:model-driven:2006-b ER - TY - JOUR AU - Brucker, Achim D. AU - Doser, Jürgen AU - Wolff, Burkhart PY - 2006// TI - An MDA Framework Supporting OCL JO - Electronic Communications of the EASST VL - 5 KW - MDE , MDA , OCL, model transformation, code-generation, verification N2 - 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. SN - 1863-2122 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-mda-2006-b L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-mda-2006-b.pdf ID - brucker.ea:mda:2006-b ER - TY - JOUR AU - Brucker, Achim D. AU - Doser, Jürgen AU - Wolff, Burkhart PY - 2006// TI - Semantic Issues of OCL: Past, Present, and Future JO - Electronic Communications of the EASST VL - 5 KW - HOL-OCL, UML/OCL, formal semantics N2 - 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. SN - 1863-2122 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-semantic-2006-b L1 - http://www.brucker.ch/bibliography/download/2006/brucker.ea-semantic-2006-b.pdf ID - brucker.ea:semantic:2006-b ER - TY - THES AU - Brucker, Achim D. PY - 2007/mar/ TI - An Interactive Proof Environment for Object-oriented Specifications PB - ETH Zurich KW - OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007 L1 - http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf N1 - ETH Dissertation No. 17097. ID - brucker:interactive:2007 U1 - Ph.D. thesis ER - TY - CHAP AU - Brucker, Achim D. AU - Doser, Jürgen ED - Favre, Jean Marie ED - Gasevic, Dragan ED - Lämmel, Ralf ED - Winter, Andreas PY - 2007/oct/ TI - Metamodel-based UML Notations for Domain-specific Languages BT - 4th International Workshop on Software Language Engineering (ATEM 2007) CY - Nashville, USA KW - DSL, UML, OCL, UML Profile, Metamodel, MOF, SecureUML N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-metamodel-2007 L1 - http://www.brucker.ch/bibliography/download/2007/brucker.ea-metamodel-2007.pdf ID - brucker.ea:metamodel:2007 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Fiadeiro, José ED - Inverardi, Paola PY - 2008// TI - HOL-OCL ? A Formal Proof Environment for UML/OCL BT - Fundamental Approaches to Software Engineering (FASE08) T3 - Lecture Notes in Computer Science SP - 97 EP - 100 IS - 4961 PB - Springer-Verlag CY - Heidelberg KW - HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008 L1 - http://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf UR - http://dx.doi.org/10.1007/978-3-540-78743-3_8 ID - brucker.ea:hol-ocl:2008 ER - TY - JOUR AU - Brucker, Achim D. AU - Brügger, Lukas AU - Wolff, Burkhart PY - 2008// TI - Verifying Test-Hypotheses: An Experiment in Test and Proof JO - Electronic Notes in Theoretical Computer Science SP - 15 EP - 27 VL - 220 IS - 1 PB - Elsevier Science Publishers CY - Amsterdam KW - symbolic test case generations, black box testing, theorem proving, formal verification, Isabelle/HOL N2 - HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/\acshol. The HOL-TestGen method is two-staged: first, the original formula, called test specification, 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. 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. SN - 1571-0661 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008 L1 - http://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf UR - http://dx.doi.org/10.1016/j.entcs.2008.11.003 N1 - Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008) ID - brucker.ea:verifying:2008 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Vitek, Jan PY - 2008// TI - Extensible Universes for Object-oriented Data Models BT - ECOOP 2008 ? Object-Oriented Programming T3 - Lecture Notes in Computer Science SP - 438 EP - 462 IS - 5142 PB - Springer-Verlag CY - Heidelberg KW - object-oriented data models, HOL, formal methods, UML, OCL N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008 L1 - http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008.pdf UR - http://dx.doi.org/10.1007/978-3-540-70592-5_19 ID - brucker.ea:extensible:2008 ER - TY - CHAP AU - Brucker, Achim D. AU - Brügger, Lukas AU - Wolff, Burkhart ED - Suzuki, Kenji ED - Higashino, Teruo PY - 2008// TI - Model-based Firewall Conformance Testing BT - Testcom/FATES 2008 T3 - Lecture Notes in Computer Science SP - 103 EP - 118 IS - 5047 PB - Springer-Verlag CY - Heidelberg KW - Security Testing, Model-based Testing, Firewall, Conformance Testing N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2008 L1 - http://www.brucker.ch/bibliography/download/2008/brucker.ea-model-based-2008.pdf UR - http://dx.doi.org/10.1007/978-3-540-68524-1_9 ID - brucker.ea:model-based:2008 ER - TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2008// TI - An Extensible Encoding of Object-oriented Data Models in HOL JO - Journal of Automated Reasoning SP - 219 EP - 249 VL - 41 IS - 3 PB - Springer-Verlag CY - Heidelberg KW - object-oriented data models, HOL, theorem proving, verification N2 - 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. SN - 0168-7433 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b L1 - http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf UR - http://dx.doi.org/10.1007/s10817-008-9108-3 ID - brucker.ea:extensible:2008-b ER - TY - JOUR AU - Wahler, Michael AU - Basin, David AU - Brucker, Achim D. AU - Koehler, Jana PY - 2010/apr/ TI - Efficient Analysis of Pattern-Based Constraint Specifications JO - Software and Systems Modeling SP - 225 EP - 255 VL - 9 IS - 2 PB - Springer-Verlag CY - Heidelberg KW - UML, OCL, Constraints, Patterns, Consistency N2 - 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. SN - 1619-1366 UR - http://www.brucker.ch/bibliography/abstract/wahler.ea-efficient-2010 L1 - http://www.brucker.ch/bibliography/download/2010/wahler.ea-efficient-2010.pdf UR - http://dx.doi.org/10.1007/s10270-009-0123-6 ID - wahler.ea:efficient:2010 ER - TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2009/jul/ TI - Semantics, Calculi, and Analysis for Object-oriented Specifications JO - Acta Informatica SP - 255 EP - 284 VL - 46 IS - 4 PB - Springer-Verlag CY - Heidelberg KW - UML, OCL, object-oriented specification, refinement, formal methods N2 - 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. SN - 0001-5903 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-semantics-2009.pdf UR - http://dx.doi.org/10.1007/s00236-009-0093-8 ID - brucker.ea:semantics:2009 ER - TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Chechik, Marsha ED - Wirsing, Martin PY - 2009// TI - HOL-TestGen: An Interactive Test-case Generation Framework BT - Fundamental Approaches to Software Engineering (FASE09) T3 - Lecture Notes in Computer Science SP - 417 EP - 420 IS - 5503 PB - Springer-Verlag CY - Heidelberg KW - symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf UR - http://dx.doi.org/10.1007/978-3-642-00593-0_28 ID - brucker.ea:hol-testgen:2009 ER - TY - CHAP AU - Brucker, Achim D. AU - Petritsch, Helmut ED - Carminati, Barbara ED - Joshi, James PY - 2009// TI - Extending Access Control Models with Break-glass BT - ACM symposium on access control models and technologies (SACMAT) SP - 197 EP - 206 PB - ACM Press CY - New York, NY, USA KW - disaster management, access-control, break-glass, model-driven security N2 - 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. SN - 978-1-60558-537-6 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-extending-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-extending-2009.pdf UR - http://dx.doi.org/10.1145/1542207.1542239 ID - brucker.ea:extending:2009 ER - TY - CONF AU - Brucker, Achim D. AU - Petritsch, Helmut AU - Schaad, Andreas PY - 2009/jul/ TI - Delegation Assistance BT - IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY) SP - 84 EP - 91 PB - IEEE Computer Society CY - Los Alamitos, CA, USA KW - delegation and revocation, policy enforcement, security services, security architecture N2 - 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. SN - 978-0-7695-3742-9 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-delegation-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-delegation-2009.pdf UR - http://dx.doi.org/10.1109/POLICY.2009.35 ID - brucker.ea:delegation:2009 ER - TY - JOUR AU - Brucker, Achim D. AU - Schaad, Andreas AU - Wolter, Christian PY - 2009/mar/ TI - Prozessmodellierung: Einbinden von Sicherheitsregeln in Geschäftsprozesse JO - iX SP - 118 EP - 121 VL - 3 PB - Heise Zeitschriften Verlag CY - Hannover, Germany SN - 0935-9680 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-modellierung-2009 N1 - An updated version of this article was published in the \glqq iX special ? Sicher im Netz\grqq (October 2010). ID - brucker.ea:modellierung:2009 ER - TY - JOUR AU - Brucker, Achim D. AU - Schaad, Andreas AU - Wolter, Christian PY - 2010/oct/ TI - Prozessmodellierung: Einbinden von Sicherheitsregeln in Geschäftsprozesse JO - iX special ? Sicher im Netz SP - 152 EP - 155 VL - 3 PB - Heise Zeitschriften Verlag CY - Hannover, Germany SN - 0935-9680 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-modellierung-2010 ID - brucker.ea:modellierung:2010 ER - TY - CHAP AU - Kohler, Mathias AU - Brucker, Achim D. AU - Schaad, Andreas PY - 2009/aug/ TI - ProActive Caching: Generating Caching Heuristics for Business Process Environments BT - International Conference on Computational Science and Engineering (CSE) SP - 207 EP - 304 VL - 3 PB - IEEE Computer Society CY - Los Alamitos, CA, USA KW - access control, proactive caching, process models N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/kohler.ea-proactive-2009 L1 - http://www.brucker.ch/bibliography/download/2009/kohler.ea-proactive-2009.pdf UR - http://dx.doi.org/10.1109/CSE.2009.177 ID - kohler.ea:proactive:2009 ER - TY - CHAP AU - Brucker, Achim D. AU - Mödersheim, Sebastian A. ED - Degano, Pierpaolo ED - Guttman, Joshua PY - 2009// TI - Integrating Automated and Interactive Protocol Verification BT - Workshop on Formal Aspects in Security and Trust (FAST 2009) T3 - Lecture Notes in Computer Science SP - 248 EP - 262 IS - 5983 PB - Springer-Verlag CY - Heidelberg KW - protocol verification, model-checking, theorem proving N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf L1 - //www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf UR - http://dx.doi.org/10.1007/978-3-642-12459-4_18 N1 - An extended version of this paper is available as IBM Research Technical Report, RZ3750. ID - brucker.ea:integrating:2009 ER - TY - RPRT AU - Brucker, Achim D. AU - Mödersheim, Sebastian A. PY - 2009// TI - Integrating Automated and Interactive Protocol Verification (Extended Version) IS - RZ3750 PB - IBM Research Zurich KW - protocol verification, model-checking, theorem proving N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009-b L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf ID - brucker.ea:integrating:2009-b ER - TY - CHAP AU - Brucker, Achim D. AU - Krieger, Matthias P. AU - Wolff, Burkhart ED - Gosh, Sudipto PY - 2009// TI - Extending OCL with Null-References BT - Models in Software Engineering T3 - Lecture Notes in Computer Science SP - 261 EP - 275 IS - 6002 PB - Springer-Verlag CY - Heidelberg KW - HOL-OCL, UML, OCL, null reference, formal semantics N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009 L1 - http://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.pdf UR - http://dx.doi.org/10.1007/978-3-642-12261-3_25 N1 - Selected best papers from all satellite events of the MoDELS 2009 conference. ID - brucker.ea:ocl-null:2009 ER - TY - CHAP AU - Brucker, Achim D. AU - Petritsch, Helmut ED - Massacci, F. ED - Wallach, D. ED - Zannone, N. PY - 2010// TI - Idea: Efficient Evaluation of Access Control Constraints BT - International Symposium on Engineering Secure Software and Systems (ESSoS) T3 - Lecture Notes in Computer Science SP - 157 EP - 165 IS - 5965 PB - Springer-Verlag CY - Heidelberg KW - distributed policy enforcement, XACML, access control N2 - 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. SN - 978-3-642-11746-6 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-efficient-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-efficient-2010.pdf UR - http://dx.doi.org/10.1007/978-3-642-11747-3_12 ID - brucker.ea:efficient:2010 ER - TY - CHAP AU - Brucker, Achim D. AU - Hutter, Dieter PY - 2010// TI - Information Flow in Disaster Management Systems BT - International Conference on Availability, Reliability and Security (ARES) SP - 156 EP - 163 PB - IEEE Computer Society CY - Los Alamitos, CA, USA KW - disaster management, information flow, access control, liaison officer N2 - 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. SN - 978-0-7695-3965-2 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-information-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-information-2010.pdf UR - http://dx.doi.org/10.1109/ARES.2010.107 ID - brucker.ea:information:2010 ER - TY - CHAP AU - Brucker, Achim D. AU - Brügger, Lukas AU - Kearney, Paul AU - Wolff, Burkhart PY - 2010// TI - Verified Firewall Policy Transformations for Test-Case Generation BT - Third International Conference on Software Testing, Verification, and Validation (ICST) SP - 345 EP - 354 KW - security testing, model-based testing N2 - 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. SN - 978-0-7695-3990-4 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-firewall-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-firewall-2010.pdf UR - http://dx.doi.org/10.1109/ICST.2010.50 ID - brucker.ea:firewall:2010 ER - TY - CHAP AU - Brucker, Achim D. AU - Petritsch, Helmut AU - Weber, Stefan G. ED - Samarati, Pierangela ED - Tunstall, Michael ED - Posegga, Joachim PY - 2010// TI - Attribute-based Encryption with Break-glass BT - Workshop In Information Security Theory And Practice (WISTP) T3 - Lecture Notes in Computer Science SP - 237 EP - 244 IS - 6033 PB - Springer-Verlag CY - Heidelberg KW - access control, break-glass, attribute-based encryption, disaster management, trusted computing plattform N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-attribute-based-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-attribute-based-2010.pdf UR - http://dx.doi.org/10.1007/978-3-642-12368-9_18 ID - brucker.ea:attribute-based:2010 ER - TY - CHAP AU - Altenhofen, Michael AU - Brucker, Achim D. ED - Kowalewski, Stefan ED - Roveri, Marco PY - 2010// TI - Practical Issues with Formal Specifications: Lessons Learned from an Industrial Case Study BT - International Workshop on Formal Methods for Industrial Critical Systems (FMICS) T3 - Lecture Notes in Computer Science SP - 17 EP - 32 IS - 6371 PB - Springer-Verlag CY - Heidelberg KW - ASM, industrial case study, formal specification N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/altenhofen.ea-issues-2010 L1 - http://www.brucker.ch/bibliography/download/2010/altenhofen.ea-issues-2010.pdf UR - http://dx.doi.org/10.1007/978-3-642-15898-8_2 ID - altenhofen.ea:issues:2010 ER - TY - CHAP AU - Kohler, Mathias AU - Brucker, Achim D. PY - 2010// TI - Caching Strategies: An Empirical Evaluation BT - International Workshop on Security Measurements and Metrics (MetriSec) SP - 1 EP - 8 PB - ACM Press CY - New York, NY, USA N2 - 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. SN - 978-1-4503-0340-8 UR - http://www.brucker.ch/bibliography/abstract/kohler.ea-caching-2010 L1 - http://www.brucker.ch/bibliography/download/2010/kohler.ea-caching-2010.pdf UR - http://dx.doi.org/10.1145/1853919.1853930 ID - kohler.ea:caching:2010 ER - TY - CHAP AU - Brucker, Achim D. AU - Krieger, Matthias P. AU - Longuet, Delphine AU - Wolff, Burkhart ED - Dingel, Jürgen ED - Solberg, Arnor PY - 2010// TI - A Specification-based Test Case Generation Method for UML/OCL BT - MoDELS Workshops T3 - Lecture Notes in Computer Science SP - 334 EP - 348 IS - 6627 PB - Springer-Verlag CY - Heidelberg KW - OCL, UML, test case generation, specification-based testing N2 - 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. SN - 978-3-642-21209-3 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-testing-2010 L1 - http://www.brucker.ch/bibliography/download/2010/brucker.ea-ocl-testing-2010.pdf UR - http://dx.doi.org/10.1007/978-3-642-21210-9_33 N1 - Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling. ID - brucker.ea:ocl-testing:2010 ER - TY - CONF AU - Brucker, Achim D. AU - Petritsch, Helmut PY - 2011/jun/ TI - A Framework for Managing and Analyzing Changes of Security Policies BT - IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY) SP - 105 EP - 112 PB - IEEE Computer Society CY - Los Alamitos, CA, USA KW - security policies, versioning, runtime monitoring N2 - 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. SN - 978-0-7695-4330-7/11 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-framework-2011 L1 - http://www.brucker.ch/bibliography/download/2011/brucker.ea-framework-2011.pdf UR - http://dx.doi.org/10.1109/POLICY.2011.47 ID - brucker.ea:framework:2011 ER - TY - CONF AU - Braune, Stephan AU - Brucker, Achim D. AU - Kleser, Gerald AU - Li, Keqin AU - Meijler, Theo Dirk AU - Paulheim, Heiko AU - Probst, Florian ED - Reussner, Ralf ED - Pretschner, Alexander ED - Jähnichen, Stefan PY - 2011/feb/ TI - A Service-Oriented Architecture for Emergency Management Systems BT - Software Engineering 2011 ? Workshopband T3 - Lecture Notes in Informatics SP - 225 EP - 232 VL - P-184 PB - GI CY - GI N2 - 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. SN - 978-3-88579-278-9 UR - http://www.brucker.ch/bibliography/abstract/braune.ea-service-oriented-2011 L1 - http://www.brucker.ch/bibliography/download/2011/braune.ea-service-oriented-2011.pdf N1 - Innovative Systeme zur Unterstützung der zivilen Sicherheit: Architekturen und Gestaltungskonzepte. ID - braune.ea:service-oriented:2011 ER - TY - CONF AU - Probst, Florian AU - Paulheim, Heiko AU - Brucker, Achim D. AU - Schulte, Stefan PY - 2010/nov/ TI - SoKNOS ? Informationsdienste für das Katastrophenmanagement BT - VDE-Kongress 2010 ? E-Mobility N2 - Dieser Beitrag gibt einen Überblick über das vom BMBF geförderte Forschungsprojekt SoKNOS (Service-orientierte ArchiteKturen zur Unterstützung von Netzwerken im Rahmen Öffentlicher Sicherheit). Im SoKNOS Projekt wurden Konzepte entwickelt, die beteiligten Organisationen im Umfeld öffentlicher Sicherheit im Katastrophenfall darin unterstützen, schnell und sicher agieren zu kö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ä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. SN - 978-3-8007-3304-0 UR - http://www.brucker.ch/bibliography/abstract/probst.ea-soknos-2010 L1 - http://www.brucker.ch/bibliography/download/2010/probst.ea-soknos-2010.pdf ID - probst.ea:soknos:2010 ER - TY - CONF AU - Brucker, Achim D. AU - Brügger, Lukas AU - Kearney, Paul AU - Wolff, Burkhart PY - 2011// TI - An Approach to Modular and Testable Security Models of Real-world Health-care Applications BT - ACM symposium on access control models and technologies (SACMAT) SP - 133 EP - 142 PB - ACM Press CY - New York, NY, USA N2 - 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. SN - 978-1-4503-0688-1 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2011 L1 - http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf UR - http://dx.doi.org/10.1145/1998441.1998461 ID - brucker.ea:model-based:2011 ER - TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2012// TI - On Theorem Prover-based Testing JO - Formal Aspects of Computing PB - Springer-Verlag CY - Heidelberg KW - test case generation, domain partitioning, test sequence, theorem proving, HOL-TestGen N2 - 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. SN - 0934-5043 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012 L1 - http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf UR - http://dx.doi.org/10.1007/s00165-012-0222-y N1 - To appear. ID - brucker.ea:theorem-prover:2012 ER - TY - CHAP AU - Marienfeld, Florian AU - Höfig, Edzard AU - Bezzi, Michele AU - Flügge, Matthias AU - Pattberg, Jonas AU - Serme, Gabriel AU - Brucker, Achim D. AU - Robinson, Philip AU - Dawson, Stephen AU - Theilmann, Wolfgang ED - Barros, Alistair ED - Oberle, Daniel PY - 2012// TI - Service levels, Security, and Trust BT - Handbook of Service Description: USDL and its Methods SP - 295 EP - 326 PB - Springer-Verlag CY - New York, NY, USA N2 - 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. SN - 978-1-4614-1864-1 UR - http://www.brucker.ch/bibliography/abstract/marienfeld.ea-usdl-security-2012 UR - http://dx.doi.org/10.1007/978-1-4614-1864-1_12 ID - marienfeld.ea:usdl-security:2012 ER - TY - CONF AU - Monakova, Ganna AU - Brucker, Achim D. AU - Schaad, Andreas PY - 2012// TI - Security and Safety of Assets in Business Processes BT - ACM Symposium on Applied Computing (SAC) PB - ACM Press CY - New York, NY, USA N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/monakova.ea-securing-2012 L1 - http://www.brucker.ch/bibliography/download/2012/monakova.ea-securing-2012.pdf ID - monakova.ea:securing:2012 ER - TY - CONF AU - Brucker, Achim D. AU - Hang, Isabelle AU - Lückemeyer, Gero AU - Ruparel, Raj PY - 2012// TI - SecureBPMN: Modeling and Enforcing Access Control Requirements in Business Processes BT - ACM symposium on access control models and technologies (SACMAT) PB - ACM Press CY - New York, NY, USA N2 - 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. UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-securebpmn-2012 L1 - http://www.brucker.ch/bibliography/download/2012/brucker.ea-securebpmn-2012.pdf ID - brucker.ea:securebpmn:2012 ER - TY - CONF ED - Brucker, Achim D. ED - Julliand, Jacques PY - 2012// TI - Tests and Proofs - 6th International Conference, TAP 2012, Praque, Czech Republic, Mai 31 ? June 1, 2012. Proceedings BT - Lecture Notes in Computer Science VL - 7305 PB - Springer-Verlag CY - Heidelberg SN - 978-3-642-21767-8 UR - http://www.brucker.ch/bibliography/abstract/brucker.ea-tap-2012 ID - brucker.ea:tap:2012 ER -