@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{DBLP:conf/vstte/FeliachiGW12,
author = {Abderrahmane Feliachi and
Marie-Claude Gaudel and
Burkhart Wolff},
title = {Isabelle/{C}ircus: A Process Specification and Verification Environment},
booktitle = {VSTTE},
year = {2012},
pages = {243-260},
series = {Lecture Notes in Computer Science},
volume = {7152},
isbn = {978-3-642-27704-7},
ee = {http://dx.doi.org/10.1007/978-3-642-27705-4_20},
doi = {10.1007/978-3-642-27705-4_20},
abstract = {The Circus specification language combines elements for complex data and behavior specifications,
using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and
He's unifying theories of programming (UTP). We develop a machine-checked, formal semantics based
on a "shallow embedding" of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL).
We derive proof rules from this semantics and imple- ment tactic support that finally allows for
proofs of refinement for Circus processes (involving both data and behavioral aspects).
This proof environment supports a syntax for the semantic definitions which is close to textbook
presentations of Circus. },
pdf = {http://www.lri.fr/~wolff/papers/conf/VSTTE-IsabelleCircus11.pdf},
classification = {conference},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@techreport{feliachi11rapport-lri,
author = {Abderrahmane Feliachi},
title = {Representing {C}ircus {O}perational {S}emantics in {I}sabelle/{HOL}},
institution = {LRI, http://www.lri.fr/Rapports-internes},
year = 2011,
number = 1544,
address = {Universit{\'e} Paris-Sud XI},
month = {August},
pdf = {http://www.lri.fr/~bibli/Rapports-internes/2011/RR1544.pdf},
x-equipes = {fortesse},
x-type = {article},
x-support = {rapport}
}
@article{DBLP:journals/eceasst/CabotCGW11,
author = {Jordi Cabot and
Robert Claris{\'o} and
Martin Gogolla and
Burkhart Wolff},
title = {Preface (OCL 2011 Proceedings)},
journal = {ECEASST},
volume = {44},
year = {2011},
ee = {http://journal.ub.tu-berlin.de/eceasst/article/view/666},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/pts/2011,
editor = {Burkhart Wolff and Fatiha Za\"{\i}di},
title = {Testing Software and Systems - 23rd IFIP WG 6.1 International
Conference, ICTSS 2011, Paris, France, November 7-10, 2011.
Proceedings},
booktitle = {ICTSS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7019},
year = {2011},
isbn = {978-3-642-24579-4},
ee = {http://dx.doi.org/10.1007/978-3-642-24580-0},
doi = {10.1007/978-3-642-24580-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tap/2011,
editor = {Martin Gogolla and Burkhart Wolff},
title = {Tests and Proofs - 5th International Conference, TAP 2011,
Zurich, Switzerland, June 30 - July 1, 2011. Proceedings},
booktitle = {TAP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6706},
year = {2011},
isbn = {978-3-642-21767-8},
bibsource = {DBLP, http://dblp.uni-trier.de},
url = {http://www.lri.fr/~wolff/papers/conf/2011-sacmat-mbtsec-npfit.pdf},
ee = {http://dx.doi.org/10.1007/978-3-642-21768-5},
doi = {10.1007/978-3-642-21768-5}
}
@incollection{2011-sacmat-mbtsec-npfit,
author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
title = {An Approach to Modular and Testable Security Models of Real-world Health-Care Applications},
pages = {133-142},
publisher = {ACM},
year = {2011},
series = {Proceedings of the ACM Symposium on Access control models and technologies},
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 National Health Service (NHS) in England. Consisting of heteroge- neous 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 en- velopes and legitimate relationships.
The model is given in Higher-order Logic (HOL) and processed together with suitable test specifications in
the HOL-TestGen system, that generates test sequences according to them. Particular em- phasis is put on the
modular description of security poli- cies and their generic combination and its consequences for
model-based testing.},
note = {SACMAT 2011},
doi = {10.1145/1998441.1998461},
pdf = {http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf}
}
@incollection{feliachi:uznifying-theories:2010,
title = {{U}nifying {T}heories in {I}sabelle/{HOL}},
abstract = { In this paper, we present various extensions of Isabelle/HOL by
theories that are essential for several formal methods. First, we
explain how we have developed an Isabelle/HOL theory for a part of
the Unifying Theories of Programming (UTP). It contains the
theories of alphabetized relations and designs. Then we explain how
we have encoded first the theory of reactive processes and then the UTP theory
for CSP. Our work takes advantage of the rich existing logical core
of HOL.
Our extension contains the proofs for most of the lemmas and
theorems presented in the UTP book. Our goal is to propose a
framework that will allow us to deal with formal methods that are
semantically based, partly or totally, on UTP, for instance CSP and
xsCircus . The theories presented here will allow us to make proofs about
such specifications and to apply verified transformations on them,
with the objective of assisting refinement and test generation.
\keywords{UTP, Theorem Proving, Isabelle/HOL, CSP, Circus}},
keywords = {UTP, Theorem Proving, Symbolic test case generations, Isabelle/HOL},
author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff},
booktitle = {Unifying Theories of Programming {(UTP2010)}},
language = {USenglish},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {6445},
classification = {conference},
ee = {http://dx.doi.org/10.1007/978-3-642-16690-7_9},
year = {2010},
doi = {10.1007/978-3-642-16690-7_9},
pdf = {http://www.lri.fr/~wolff/papers/conf/2010-utp-unifying-theories.pdf},
public = {yes}
}
@techreport{wolff:FMWettbebwerb:2009,
author = {Burkhart Wolff},
title = {Top-down vs. {B}ottom-up: {F}ormale {M}ethoden im wissenschaftlichen {W}ettbewerb. {E}in essayistischer {S}urvey \"uber den {S}tand der {K}unst.},
institution = {DFKI Technischer Bericht},
year = 2009,
pdf = {http://www.lri.fr/~wolff/papers/other/festschrift.pdf},
note = {Erschienen in der Festschrift zum 60. Geburtstag von Bernd Krieg-Br\"uckner.},
abtract = {In diesem Beitrag wird versucht, einen \"Uberblick \"uber
den Wettbewerb zweier konkurrierender
Forschungsprogramme --- genannt Top-down oder
Transformationelle Entwicklungsmethodik versus
Bottom-up oder post-hoc Programmverifikation ---
Bereich “For- maler Methoden” zu geben. Als
Einordnungsrahmen benutze ich Lakatos's Konzept
des "wissenschaftlichen Forschungsprogramms". Es
ergibt sich ein bewusst altmodischer Versuch --- im
Gegensatz zu modischen bibliometrischen Kriterien
(vulgo: Zahlen von Ver\"offentlichungen) ---
inhaltliche Kriterien f\"ur die Qualit\"at und damit
den Fortschritt der wissenschaftlichen Arbeit in
unserem Gebiet zu entwickeln.}
}
@inproceedings{Brucker.ea:SpecificationBased:2010,
author = {Achim D. Brucker and Matthias P. Krieger and Delphine Longuet and Burkhart Wolff},
title = {{A} {S}pecification-based {T}est {C}ase {G}eneration {M}ethod for {UML}/{OCL}},
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 class models and recursive query operations on
them. A key feature of our approach is an implicit
representation of object graphs avoiding a repre-
sentation 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.},
pdf = {http://www.lri.fr/~wolff/papers/workshop/ocl-testing.pdf},
booktitle = {Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010)},
classification = {conference},
year = 2010,
doi = {10.1007/978-3-642-21210-9_33},
note = {LNCS 6627}
}
@inproceedings{Krieger.ea:2010,
author = {Matthias P. Krieger and Alexander Knapp and Burkhart Wolff},
title = {{A}utomatic and {E}fficient {S}imulation of {O}peration {C}ontracts},
booktitle = {Ninth International Conference on Generative Programming and Component Engineering (GPCE'10)},
year = 2010,
publisher = {IEEE Computer Society},
copyright = {IEEE Computer Society},
editor = {Eelco Visser and Jaakko Jarvi and Giorgios Economopoulos},
isbn = {978-1-4503-0154-1},
doi = {10.1145/1868294.1868303},
classification = {conference},
pdf = {http://www.lri.fr/~wolff/papers/conf/2010-gpce-operation-contracts.pdf},
abstract = {Operation contracts consisting of pre- and
postconditions are a well-known means of specifying
operations. In this paper we deal with the problem
of operation contract simulation, i.e., determining
operation results satisfying the postconditions
based on input data supplied by the user; simulating
operation contracts is an important technique for
requirements validation and prototyping. Current
approaches to operation contract simulation exhibit
poor performance for large sets of input data or
require additional guidance from the user. We show
how these problems can be alleviated and describe an
efficient as well as fully automatic approach. It is
implemented in our tool OCLexec that generates from
UML/OCL operation contracts corresponding Java
implementations which call a constraint solver at
runtime. The generated code can serve as a
prototype. A case study demonstrates that our
approach can handle problem instances of
considerable size.}
}
@article{brucker.ea:2010,
author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
journal = {Software Testing, Verification, and Validation, 2010 International Conference on},
volume = {0},
title = {{V}erified {F}irewall {P}olicy {T}ransformations for {T}est {C}ase {G}eneration},
year = 2010,
isbn = {978-0-7695-3990-4},
pages = {345-354},
publisher = {IEEE Computer Society},
copyright = {IEEE Computer Society},
booktitle = {International Conference on Software Testing {(ICST10)}},
location = {Paris, France},
editor = {Ana Cavalli and Sudipto Ghosh},
classification = {conference},
doi = {10.1109/ICST.2010.50},
address = {Los Alamitos, CA, USA},
pdf = {http://www.lri.fr/~wolff/papers/conf/firewall-reloaded.pdf},
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/\acs{hol}. Finally, we use the normalized policies to
generate test cases with the domain-specific firewall testing tool
\testgenFW.
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.}
}
@article{brucker.ea:2012,
author = {Achim D. Brucker and Burkhart Wolff},
title = {On {T}heorem {P}rover-based {T}esting},
journal = {Formal Aspects of Computing (FAOC)},
year = 2012,
abstract = {\emph{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.lri.fr/~wolff/papers/journals/brucker.ea-hol-testgen-2008.rev-1.pdf},
keywords = {Isabelle/HOL, Theorem proving, Model-based Testing, Program-based Testing, Testcase Generation},
doi = {10.1007/s00165-012-0222-y},
classification = {journal}
}
@article{boehme.ea:2009,
author = {Sascha B\"ohme and Micha{\l} Moskal and Wolfram
Schulte and Burkhart Wolff},
title = {{HOL}-{B}oogie --- {A}n {I}nteractive {P}rover-{B}ackend for the {V}erified {C} {C}ompiler},
journal = {Journal of Automated Resoning (JAR)},
year = 2009,
abstract = {\emph{Boogie} is a verification condition generator for
an imperative core language. It has front-ends for
the programming languages C{\#} and C enriched by
annotations in first-order logic, ie pre- and
postconditions, assertions, and loop invariants.
Moreover, concepts like ghost fields, ghost
variables, ghost code and speci\-fication functions
have been introduced to support a specific modeling
methodology. Boogie's verification conditions ---
constructed via a $\mathit{wp}$ calculus from
annotated programs --- are usually transferred to
automated theorem provers such as \emph{Simplify} or
\emph{Z3}. This also comprises the expansion of
language-specific modeling constructs in terms of a
theory describing memory and elementary operations
on it; this theory is called \emph{machine/memory
model}. In this paper, we present a proof
environment, HOL-Boogie, that combines Boogie with
the interactive theorem prover Isabelle/\HOL, for a
specific C front-end and machine/memory model. In
particular, we present specific techniques combining
automated and interactive proof methods for code
verification. The main goal of our environment is to
help program verification engineers in their task to
``debug'' annotations and to find combined proofs
where purely automatic proof attempts fail. },
doi = {10.1007/s10817-009-9142-9},
volume = 44,
number = {1--2},
pages = {111--144},
pdf = {http://www.lri.fr/~wolff/papers/journals/hol-boogie.pdf},
keywords = {Isabelle/HOL, Theorem proving, Program verification, Memory models, Annotation languages},
classification = {journal}
}
@article{brucker.ea:2009,
author = {Achim D. Brucker and Burkhart Wolff},
title = {{S}emantics, {C}alculi, and {A}nalysis for {O}bject-{O}riented {S}pecifications},
journal = {Acta Informatica},
volume = 46,
number = 4,
pages = {255--284},
year = 2009,
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. },
pdf = {http://www.lri.fr/~wolff/papers/journals/acta-holocl.pdf},
keywords = {UML , OCL , object-oriented specification , refinement , formal methods},
doi = {10.1007/s00236-009-0093-8},
classification = {journal}
}
@article{daum.ea:fairness:2009,
author = {Matthias Daum and Jan D\"{o}rrenb\"{a}cher and Burkhart Wolff},
title = {{P}roving {F}airness and {I}mplementation {C}orrectness of a {M}icrokernel {S}cheduler},
journal = {Journal of Automated Reasoning (JAR)},
volume = 42,
number = {2--4},
year = 2009,
pdf = {http://www.lri.fr/~wolff/papers/journals/pre-fairness.pdf},
pages = {349--388},
publisher = {Springer Verlag},
abstract = {We report on the formal proof of a microkernel's key
property, namely the fairness property of its
multi-priority process scheduler. The proof
architecture links a layer of behavioral reasoning
over system-trace sets with a concrete, fairly
realistic implementation written in C. Our
microkernel provides an infra-structure for memory
virtualization, for communication with hardware
devices, for processes (represented as a sequence of
assembler instructions, which are executed
concurrently over an underlying, formally defined
processor), and for inter-process communication
(IPC) via synchronous message passing. The kernel
establishes process switches according to IPCs and
timer-events; however, the scheduling of process
switches follows a hierarchy of priorities,
favoring, e. g., system processes over application
processes over maintenance processes. Besides the
quite substantial models developed in Isabelle/HOL
and the formal clarification of their relationship,
we provide a detailed analysis what formal
requirements a microkernel imposes on the key
ingredients (hardware, timers, machine-dependent
code) in order to establish the correct operation of
the overall system. On the methodological side, we
show how early modeling with hindsight to the later
verification has substantially helped our project.},
doi = {10.1007/s10817-009-9119-8},
note = {G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008).},
keywords = {Microkernel, Formal verification, Interactive theorem proving, Isabelle/HOL},
classification = {journal}
}
@incollection{brucker.ea:hol-testgen:2009,
title = {{HOL-TestGen:} {A}n {I}nteractive {T}est-case {G}eneration {F}ramework},
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},
categories = {holtestgen},
classification = {conference},
year = {2009},
pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf},
ps = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.ps.gz},
public = {yes},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009}
}
@incollection{aspinall.ea:assisted:2005,
title = {{A}ssisted {P}roof {D}ocument {A}uthoring},
abstract = {Significant advances have been made in formalised
mathematical texts for large, demanding proofs. But
although such large developments are possible, they still
take an inordinate amount of effort and there is a
significant gap between the resulting formalised
machinecheckable proof scripts and the corresponding
human-readable mathematical texts. We present an authoring
system for formal proof which addresses these concerns. It
is based on a central document format which, in the
tradition of literate programming, allows one to extract
either a formal proof script or a human-readable document;
the two may have differing structure and detail levels, but
are developed together in a synchronised way. Additionally,
we introduce ways to assist production of the central
document, by allowing tools to contribute backflow to
update and extend it. Our authoring system builds on the
new PG Kit architecture for Proof General, bringing the
extra advantage that it works in a uniform interface,
generically across various interactive theorem provers.},
author = {David Aspinall and Christoph L\"uth and Burkhart Wolff},
booktitle = {Fourth International Conference on Mathematical Knowledge
Management (MKM 05)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/11618027_5},
language = {USenglish},
publisher = {Springer Verlag},
pdf = {http://www.lri.fr/~wolff/papers/conf/aspinall-authoring-mkm-06.pdf},
series = {LNCS 3863.},
year = 2005,
classification = {conference}
}
@article{basin.ea:berichte:2000,
author = {David Basin and Luca Vigan{\`o} and Burkhart Wolff},
classification = {conference},
file = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/overview.ps.gz},
filelabel = {English translation},
journal = {PIK (Praxis der Informationsverarbeitung und
Kommunikation)},
language = {german},
number = 4,
pages = {248--249},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/uebersicht.pdf},
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/uebersicht.ps.gz},
title = {Berichte aus den Instituten: Lehrstuhl f{\"u}r
Softwaretechnik und Softwareproduktionsumgebung, Freiburg},
volume = 23,
year = 2000
}
@techreport{basin.ea:specifying:2005,
abstract = {We report on a case-study in using the data-oriented
modeling language Z to formalize a security architecture
for administering digital signatures and its architectural
security requirements. Within an embedding of Z in the
higher-order logic Isabelle/HOL, we provide formal
machine-checked proofs of the correctness of the
architecture with respect to its requirements. A
formalization and verification of the same architecture has
been previously carried out using the process-oriented
modeling language PROMELA and the SPIN model checker. We
use this as a basis for comparing these two different
approaches to formalization (infinite state with rich data
types versus finite state) and verification (theorem
proving versus model checking).},
author = {David Basin and Hironobu Kuruma and Kazuo Takaragi and
Burkhart Wolff},
institution = {Computer Security Group, ETH Z\"urich},
language = {USenglish},
month = 1,
number = 471,
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2005/HSD.pdf},
title = {{S}pecifying and {V}erifying {H}ysteresis {S}ignature {S}ystem with {HOL-Z}},
year = 2005,
user = {wolff}
}
@proceedings{basin.ea:theorem:2003,
abstract = {This book constitutes the refereed proceedings of the 16th
International Conference on Theorem Proving in Higher Order
Logics, TPHOLs 2003, held in Rome, Italy in September 2003.
The 24 revised full papers presented together with an
invited paper were carefully reviewed and selected from 50
submissions. The papers are organized in topical sections
on hardware and Assembler languages, proof automation, fool
combination, logic extensions, theorem prover technology,
mathematical theories, and security. Among the theorem
proving systems discussed are HOL, Coq, MetaPRL, and
Isabelle/Isar.Geschrieben f\"ur:Researchers and
professionalsSchlagworte: automated deduction formal
methods formal verification hardware verification
higher-order logic logic design mathematical logic model
checking program verification proof theory theorem provers
theorem proving unification},
address = {Rome, Italy},
copyright = {\ Springer-Verlag},
doi = {10.1007/b11935},
editor = {David Basin and Burkhart Wolff},
language = {USenglish},
month = {Sep},
note = {LNCS 2758.},
publisher = {Springer-Verlag},
title = {{T}heorem {P}roving in {H}igher {O}rder {L}ogics, 16th {I}nternational {C}onference ({TPHOL}s 2003)},
year = 2003,
user = {wolff}
}
@incollection{basin.ea:verification:2005,
abstract = {We report on a case study in using HOL-Z, an embedding of
Z in higher-order logic, to specify and verify a security
architecture for administering digital signatures. We have
used HOL-Z to formalize and combine both data-oriented and
process-oriented architectural views. Afterwards, we
formalized temporal requirements in Z and carried out
verification in higher-order logic. The same architecture
has been previously verified using the SPIN model checker.
Based on this, we provide a detailed comparison of these
two di erent approaches to formalization (infinite state
with rich data types versus finite state) and verification
(theorem proving versus model checking). Contrary to common
belief, our case study suggests that Z is well suited for
temporal reasoning about process models with rich data.
Moreover, our comparison highlights the advantages of this
approach and provides evidence that, in the hands of
experienced users, theorem proving is neither substantially
more time-consuming nor more complex than model checking.},
author = {David Basin and Hironobu Kuruma and Kazuo Takaragi and
Burkhart Wolff },
booktitle = {Formal Methods 2005},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/11526841_19},
language = {USenglish},
pages = {269--285},
publisher = {Springer Verlag},
series = {LNCS 3582},
title = {{V}erification of a {S}ignature {A}rchitecture with {HOL-Z}},
pdf = {http://www.lri.fr/~wolff/papers/conf/Basin-Verification-FM05.pdf},
year = 2005,
user = {wolff}
}
@article{basin.ea:verifying:2007,
abstract = {We report on a case study in applying different formal
methods to model and verify an architecture for
administrating digital signatures. The architecture
comprises several concurrently executing systems that
authenticate users and generate and store digital
signatures by passing security relevant data through a
tightly controlled interface. The architecture is
interesting from a formal-methods perspective as it
involves complex operations on data as well as process
coordination and hence is a candidate for both
data-oriented and process-oriented formal methods.We have
built and verified two models of the signature architecture
using two representative formal methods. In the first, we
specify a data model of the architecture in Z that we
extend to a trace model and interactively verify by theorem
proving. In the second, we model the architecture as a
system of communicating processes that we verify by
finite-state model checking. We provide a detailed
comparison of these two different approaches to
formalization (infinite state with rich data types versus
finite state) and verification (theorem proving versus
model checking). Contrary to common belief, our case study
suggests that Z is well suited for temporal reasoning about
process models with complex operations on data. Moreover,
our comparison highlights the advantages of proving
theorems about such models and provides evidence that, in
the hands of an experienced user, theorem proving may be
neither substantially more time-consuming nor more complex
than model checking.},
author = {David Basin and Hironobu Kuruma and Kunihiko Miyazaki and
Kazuo Takaragi and Burkhart Wolff},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/s00165-006-0012-5},
journal = {Formal Aspects of Computing},
language = {USenglish},
month = {March},
note = {http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0},
number = 1,
pages = {63--91},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2007/fac.submit.pdf},
title = {Verifying a signature architecture: a comparative case study},
volume = 19,
year = 2007,
user = {lukasbru}
}
@article{basin.ea:z:2007,
abstract = {Z is a standardized and well-established formal
specification language originally developed in the 80ies by
researchers at oxford University. Although the original
emphasis of Z is on specification, the semantics for Z can
be expressed within higher-order logic (HOL). On this
basis, a theorem-proving environment such as Isabelle/HOL-Z
can be built. In this paper, we show how properties over
specifications can be formally proven in HOL-Z. Particular
emphasis is put on proving relationships between
specification such as refinement.},
author = {David Basin and Hironobu Kuruma and Shin Nakajima and
Burkhart Wolff},
url = {http://www.jstage.jst.go.jp/browse/jssst/24/2/_contents},
journal = {Computer Software --- Journal of the Japanese Society for
Software Science and Technology},
language = {USenglish},
month = {April},
note = {In Japanese. },
number = 2,
pages = {21--26},
title = {{T}he {Z} {S}pecification {L}anguage and the {P}roof {E}nvironment {Isabelle/HOL-Z}},
volume = 24,
year = 2007,
user = {wolff}
}
@incollection{bohme.ea:hol-boogie:2008,
abstract = {Boogie is a program verification condition generator for
animperative core language. It has front-ends for the
programming languagesC# and C enriched by annotations in
first-order logic.Its verification conditions --- constructed
via a wp calculus from these annotations --- are usually
transferred to automated theorem proverssuch as Simplify or
Z3. In this paper, however, we present a
proof-environment,HOL-Boogie, that combines Boogie with the
interactivetheorem prover Isabelle/HOL. In particular, we
present specific techniquescombining automated and
interactive proof methods for code-verification.We will
exploit our proof-environment in two ways: First, we
present scenariosto \"debug\" annotations (in particular:
invariants) by interactiveproofs. Second, we use our
environment also to verify \"background theories\",i.e.
theories for data-types used in annotations as well as
memoryand machine models underlying the verification method
for C.},
address = {Montreal, Canada},
author = {Sascha B\"ohme and Rustan Leino and Burkhart Wolff},
booktitle = {21th International Conference on Theorem proving in
Higher-Order Logics (TPHOLs 2008)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/978-3-540-71067-7_15},
editor = {Sofiene Tahar and Otmane Ait Mohamed and C{\'e}sar
Mu{\~n}oz},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/boehme_tphols_2008.pdf},
publisher = {Springer-Verlag},
series = {LNCS 5170},
title = {{HOL-Boogie} --- {A}n {I}nteractive {P}rover for the {B}oogie {P}rogram {V}erifier},
year = 2008,
user = {lukasbru}
}
@techreport{brucker.ea:checking:2001,
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-checking-2001},
author = {Achim D. Brucker and Burkhart Wolff},
institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
language = {USenglish},
month = jul,
classification = {unrefereed},
title = {{Checking OCL Constraints in Distributed Systems Using
J2EE/EJB}},
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},
ps = {http://www.brucker.ch/bibliography/download/2001/tr01.ps.gz}
}
@incollection{brucker.ea:cvs-server:2002,
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002},
author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
title = {The {CVS}-Server Case Study: A Formalized Security
Architecture},
editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang
Reif},
booktitle = {FM-TOOLS 2002},
classification = {conference},
year = 2002,
series = {Technical Report},
number = {2002--11},
pages = {47--52},
month = jul,
organization = {University Augsburg},
address = {Augsburg},
pdf = {http://www.brucker.ch/bibliography/download/2002/fmtools_cvs_02.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}
}
@techreport{brucker.ea:cvs-server:2002-b,
url = {http://www.brucker.ch/bibliography/abstract/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,
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 \unixcmd{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,
classification = {unrefereed},
num_pages = 100,
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.pdf},
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.ps.gz}
}
@article{brucker.ea:extensible:2008,
abstract = {We present an extensible encoding of object-oriented data
models into higher-order logic (HOL). Our encoding is
supported by a datatype package that 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},
journal = {Journal of Automated Reasoning (JAR)},
classification = {journal},
language = {USenglish},
note = {Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds)},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/0_brucker.ea-datatype-2007.pdf},
title = {{A}n {E}xtensible {E}ncoding of {O}bject-oriented {D}ata {M}odels in {HOL} with an {A}pplication to {IMP++}},
volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
doi = {10.1007/s10817-008-9108-3},
pages = {219-249},
volume = 41,
number = {3--4},
year = 2008
}
@incollection{brucker.ea:extensible:2008-b,
abstract = {We present a datatype package that enables the shallow
embedding technique to object-oriented specification and
programming languages. This datatype package incrementally
compiles an object-oriented data model to a theory
containing object-universes, constructors, 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. },
address = {Paphos, Cyprus},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Proceedings of the European Conference of Object-Oriented
Programming (ECOOP 2008)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/978-3-540-70592-5_19},
editor = {Jan Vitek},
isbn = {0302-9743},
language = {USenglish},
classification = {conference},
month = {July},
pages = {438--462},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/brucker.ea-datatype-2008.pdf},
publisher = {Springer-Verlag},
series = {LNCS 5142},
title = {Extensible Universes for Object-Oriented Data Models },
url = {http://www.springerlink.com/content/416483625116hw37/?p=b2e4cfb4996441a9b171c4594f015499&pi=18},
year = 2008,
user = {lukasbru}
}
@inproceedings{brucker.ea:formal:2008,
title = {{A} {F}ormal {P}roof {E}nvironment for {UML/OCL}},
abstract = {We present the theorem proving environment HOL-OCL that is
integrated in a MDE framework. HOL-OCL allows to reason
over UML class models annotated with OCL
specifications. Thus, HOL-OCL strengthens a crucial part of
the UML to an object-oriented formal method. \holocl
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.},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Proceedings of Formal Aspects of Software Engineering
(FASE 2008)},
isbn = {0302-9743},
language = {USenglish},
classification = {conference},
pages = {97--101},
doi = {10.1007/978-3-540-78743-3_8},
pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/2008-fase-hol-ocl.pdf},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
volume = 4961,
year = 2008
}
@techreport{brucker.ea:hol-ocl-book:2006,
author = {Achim D. Brucker and Burkhart Wolff},
institution = {ETH Z{\"u}rich},
language = {USenglish},
title = {The {HOL-OCL} {B}ook},
classification = {unrefereed},
categories = {holocl},
year = 2006,
number = 525,
pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
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},
keywords = {security, SecureUML, UML, OCL, HOL-OCL,
model-transformation}
}
@incollection{brucker.ea:hol-ocl:2002,
title = {{HOL-OCL}: Experiences, Consequences and Design Choices},
url = {http://www.brucker.ch/bibliography/abstract/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},
paddress = {Heidelberg},
address = {Dresden},
author = {Achim D. Brucker and Burkhart Wolff},
classification = {conference},
booktitle = {UML 2002: Model Engineering, Concepts and Tools},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/3-540-45800-X_17},
language = {USenglish},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
number = 2460,
editor = {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and
Stephen Cook},
pdf = {http://www.brucker.ch/bibliography/download/2002/holocl_experiences.pdf},
project = {CSFMDOS},
year = 2002
}
@techreport{brucker.ea:hol-testgen:2005,
author = {Achim D. Brucker and Burkhart Wolff},
institution = {Computer Security Group, ETH Z\"urich},
language = {USenglish},
month = {apr},
number = 482,
title = {{HOL-TestGen} 1.0.0 User Guide},
classification = {unrefereed},
year = 2005,
user = {wolff}
}
@incollection{brucker.ea:hol-z:2002,
url = {http://www.brucker.ch/bibliography/abstract/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 = {FMTOOLS 2002},
classification = {conference},
year = 2002,
series = {Technical Report},
pages = {33--38},
month = jul,
number = {2002--11},
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. },
project = {FSA}
}
@incollection{brucker.ea:interactive:2005,
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. },
address = {Edinburgh},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Formal Approaches to Testing of Software (FATES 05)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/11759744_7},
editor = {Wolfgang Grieskamp and Carsten Weise},
isbn = {3-540-25109-X},
language = {USenglish},
pages = {87--102},
publisher = {Springer-Verlag},
series = {LNCS 3997},
title = {{I}nteractive {T}esting using {HOL-TestGen}},
year = 2005,
classification = {workshop},
user = {wolff}
}
@inproceedings{brucker.ea:mda:2006,
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},
booktitle = {6th OCL Workshop at the UML/MoDELS Conference},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2006/OclApps-framework.pdf},
title = {An {MDA} Framework Supporting{ OCL}},
classification = {workshop},
year = 2006,
user = {wolff}
}
@article{brucker.ea:mda:2007,
abstract = {We present a model-driven architecture (MDA) framework
that integrates formal analysis techniques into an
industrial software development process model. This
comprises modeling using UML/OCL, processing models by
model transformations, code generation (including
runtime-test environments) and formal analysis using the
theorem proving environment HOL-OCL. Moreover, our
frameworks supports the verification of proof obligations
that are generated during model transformations.We show the
extensibility of our approach by providing a SecureUML
extension of the framework, which allows for an integrated
specification of security properties, their analysis and
their conversion to code.},
author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
journal = {Electronic Communications of the EASST},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2007/easst-framework.pdf},
title = {An {MDA} Framework Supporting {OCL}},
url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
volume = 5,
year = 2007,
classification = {workshop},
user = {doserj}
}
@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.},
address = {Tokyo, Japan},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
booktitle = {Testcom/FATES 2008},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/978-3-540-68524-1_9},
editor = {Kenji Suzuki and Teruo Higashino},
isbn = {0302-9743 (Print) 1611-3349 (Online)},
language = {USenglish},
pages = {103--118},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/2008-testcom-fw-test.pdf},
publisher = {Springer-Verlag},
series = {LNCS 5047},
title = {Model-based Firewall Conformance Testing},
url = {http://www.springerlink.com/content/5v5167t1216vlw7v/},
year = 2008,
classification = {conference},
user = {lukasbru}
}
@incollection{brucker.ea:model: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 \acs{uml}/\acs{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.},
address = {Genova},
author = {Achim D. Brucker and J{\"u}rgen Doser and Burkhart Wolff},
booktitle = {{MoDELS} 2006: Model Driven Engineering Languages and
Systems},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/11880240_22},
editor = {Oscar Nierstrasz and Jon Whittle and David Harel and
Gianna Reggio},
filelabel = {Extended Version},
language = {USenglish},
note = {An extended version of this paper is available as ETH
Technical Report, no. 524.},
pages = {306--320},
publisher = {Springer-Verlag},
series = {LNCS 4199},
title = {A Model Transformation Semantics and Analysis Methodology
for {SecureUML}},
year = 2006,
pdf = {http://www.lri.fr/~wolff/papers/conf/brucker-2.ea-transformation-2006.pdf},
user = {wolff},
classification = {conference}
}
@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,
series = {Computing Research Repository (CoRR)},
month = aug,
address = {Seattle, USA},
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},
ps = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.ps.gz},
pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf},
classification = {workshop},
keywords = {datatype package, extensible object-oriented data model,
object-oriented specification,shallow embedding}
}
@incollection{brucker.ea:proposal:2002,
url = {http://www.brucker.ch/bibliography/abstract/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},
paddress = {Heidelberg},
address = {Hampton, VA, USA},
author = {Achim D. Brucker and Burkhart Wolff},
classification = {conference},
booktitle = {Theorem Proving in Higher Order Logics},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/3-540-45685-6_8},
editor = {C{\'e}sar Mu{\~n}oz and Sophi{\`e}ne Tahar and V{\'\i}ctor
Carre{\~n}o},
language = {USenglish},
pdf = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic.pdf},
filelabel = {extended},
file = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic_extended.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
number = 2410,
pages = {99--114},
project = {CSFMDOS},
title = {A Proposal for a Formal {OCL} Semantics in
{Isabelle/HOL}},
year = 2002
}
@inproceedings{brucker.ea:semantic:2006,
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},
booktitle = {6th OCL Workshop at the UML/MoDELS Conference},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2006/OclApps-glitches.pdf},
title = {Semantic Issues of {OCL}: Past, Present, and Future},
year = 2006,
url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
classification = {conference},
user = {wolff}
}
@article{brucker.ea:semantic:2007,
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 program verifications and specification
refinement.},
author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
journal = {Electronic Communications of the EASST},
language = {USenglish},
url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2007/easst-glitches.pdf},
title = {Semantic Issues of {OCL}: Past, Present, and Future},
volume = 5,
year = 2007,
classification = {ejournal},
user = {doserj}
}
@techreport{brucker.ea:symbolic:2004,
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.},
author = {Achim D. Brucker and Burkhart Wolff},
institution = {Computer Security Group, ETH Z\"urich},
language = {USenglish},
month = {jun},
number = 449,
title = {Symbolic Test Case Generation for Primitive Recursive
Functions},
year = 2004,
classification = {unrefereed},
user = {wolff}
}
@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. },
address = {Linz 04},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Formal Approaches to Testing of Software (FATES 04)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/b106767},
editor = {Jens Grabowski and Brian Nielsen},
isbn = {3-540-25109-X},
language = {USenglish},
pages = {16--32},
publisher = {Springer-Verlag},
series = {LNCS 3395},
title = {Symbolic Test Case Generation for Primitive Recursive
Functions},
url = {http://springerlink.metapress.com/content/yqv0ajk1wb0ctllt/?p=4f2d15532c2c45e6a0673b2465e27f5e&pi=1},
year = 2005,
classification = {workshop},
user = {wolff}
}
@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},
paddress = {Heidelberg},
address = {Zurich},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {{TAP} 2007: Tests And Proofs},
copyright = {\copyright Springer-Verlag},
copyrighturl = {http://link.springer-ny.com/link/service/series/0558/},
language = {USenglish},
publisher = {Springer-Verlag},
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},
year = 2007,
doi = {10.1007/978-3-540-73770-4_9},
pages = {149--168},
isbn = {978-3-540-73769-8},
classification = {conference},
pdf = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf},
ps = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.ps.gz},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007}
}
@inproceedings{brucker.ea:testing:2001,
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-testing-2001},
author = {Achim D. Brucker and Burkhart Wolff},
classification = {proceedings},
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},
ps = {http://www.brucker.ch/bibliography/download/2001/info2001.ps.gz}
}
@incollection{brucker.ea:using: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.},
address = {Nijmegen},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Types 2002, Proceedings of the workshop Types for Proof
and Programs},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/3-540-45685-6_8},
editor = {Herman Geuvers and Freek Wiedijk},
isbn = {3-540-14031-X},
language = {USenglish},
publisher = {Springer-Verlag},
series = {LNCS 2646},
title = {Using Theory Morphisms for Implementing Formal Methods Tools},
year = 2003,
classification = {workshop},
user = {wolff}
}
@article{brucker.ea:verification:2005,
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.},
author = {Achim D. Brucker and Burkhart Wolff},
copyright = {\copyright Springer-Verlag},
issn = {1433-2779},
journal = {International Journal on Software Tools for Technology
Transfer (STTT)},
language = {USenglish},
number = 3,
doi = {10.1007/s10009-004-0176-3},
pages = {233--247},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2005/sttt_03.pdf},
title = {A Verification Approach for Applied System Security},
volume = 7,
year = 2005,
classification = {journal},
user = {wolff}
}
@inproceedings{brucker.ea:verifying:2008,
abstract = {HOL-TestGen is a specification and test case generation
environment extending the interactive theorem prover
Isabelle/HOL. 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.},
address = {Budapest, Hungary },
author = {Achim D. Brucker and Lukas Br\"ugger and Burkhart Wolff},
booktitle = {Model-based Testing (MBT) 2008 },
editor = {Bernd Finkbeiner and Yuri Gurevich and Alexander K.
Petrenko},
language = {USenglish},
pages = {15-28},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/brucker.ea-testhyps-2008.pdf},
publisher = {Elsevier Science Publishers },
series = {Electronic Notes in Theoretical Computer Science},
title = {Verifying Test-Hypotheses -- An Experiment in Test and
Proof},
year = 2008,
doi = {10.1016/j.entcs.2008.11.003},
volume = 202,
classification = {workshop},
user = {lukasbru}
}
@article{brucker.rittinger.ea:hol-z,
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},
classification = {journal},
language = {USenglish},
title = {{HOL-Z} 2.0: {A} {P}roof {E}nvironment for {Z}-{S}pecifications},
volume = 9,
year = 2003,
number = 2,
pages = {152--172},
month = feb,
issn = {0948-6968},
ps = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.ps.gz},
pdf = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf},
copyright = {\copyright J.UCS},
doi = {10.3217/jucs-009-02-0152},
copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2}
}
@inproceedings{brucker.wolff:case,
author = {Achim D. Brucker and Burkhart Wolff},
title = {A Case Study of a Formalized Security Architecture},
booktitle = {Eighth International Workshop onFormal Methods for
Industrial Critical Systems (FMICS'03)},
volume = 80,
classification = {workshop},
editor = {Thomas Arts and Wan Fokkink},
publisher = {Elsevier Science Publishers},
year = 2003,
language = {USenglish},
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/fmics_03.pdf},
ps = {http://www.brucker.ch/bibliography/download/2003/fmics_03.ps.gz}
}
@incollection{daum.ea:verification:2008,
abstract = {Though the verification of operating systems is an active
research field, a verification method is still missing that
provides both, the proximity to practically used
programming languages such as C and a realistic model of
concurrency, i.e. a model that copes with the granularity
of atomic operations actually used in a target machine.Our
approach serves as the foundation for the verification of
concurrent programs in C0 --- a C fragment enriched by kernel
communication primitives --- in a Hoare-Logic. C0 is compiled
by a verified compiler into assembly code representing a
cooperative concurrent transition system. For the latter,
it is shown that it can actually be executed in a true
concurrent way reflecting the C0 semantics.},
author = {Matthias Daum and Jan D\"orrenb\"acher and Mareike Schmidt
and Burkhart Wolff},
booktitle = {Verified Software: Theories, Tools, Experiments},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/978-3-540-87873-5_15},
language = {USenglish},
month = {September},
pages = {161--176},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/1_libvamos.pdf},
publisher = {Springer Berlin / Heidelberg},
series = {LNCS 5295},
title = {A Verification Approach for System-Level Concurrent Programs },
year = 2008,
classification = {conference},
user = {lukasbru}
}
@proceedings{garca.ea:proceedings:2006,
abstract = {This book constitutes the refereed proceedings of the
International Workshop on Formal Aspects of Testing and
Runtime Verification, FATES/RV 2006, held in Seattle, USA
in August 2006 in conjuction with FLoC.The 14 revised full
papers presented together with twoinvited papers were
carefully reviewed and selected from 34 submissions. },
address = {Seattle, USA},
copyright = {\ Springer-Verlag},
editor = {Manuel N{\'u}{\~n}ez Garc{\'\i}a and Klaus Havelund and
Grigore Rosu and Burkhart Wolff},
copyrighturl = {http://dx.doi.org/10.1007/11940197},
doi = {10.1007/11940197},
language = {USenglish},
note = {LNCS 4262.},
publisher = {Springer Verlag},
title = {Proceedings of the International Workshop on Formal
Aspects of Testing and Runtime Verification (FATES/RV)},
year = 2006,
classification = {workshop},
user = {wolff}
}
@inproceedings{klmw96a,
author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
booktitle = {Proceedings of the User Interfaces for Theorem Provers
(UITP 96)},
editor = {N. Merriam},
publisher = {University of York},
series = {Technical Report},
title = {Generating Graphical User-Interfaces in a Functional
Setting},
year = 1996,
ps = {http://www.informatik.uni-bremen.de/~bu/papers/uitp96.ps.gz},
language = {USEnglish},
classification = {workshop}
}
@inproceedings{klmw97,
author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
booktitle = {TAPSOFT 97: Theory and Practice of Software Development },
editor = {M. Bidoit, M. Dauchet},
pages = {855--858},
publisher = {Springer Verlag},
series = {LNCS 1214},
doi = {10.1007/BFb0030646},
title = {TAS and IsaWin: Generic Interfaces for Transformational
Program Development and Theorem Proving},
year = 1997,
ps = {http://www.informatik.uni-bremen.de/~bu/papers/tapsoft.ps.gz},
language = {USEnglish},
classification = {conference}
}
@inproceedings{klmw97b,
author = {Kolyang and C. L{\"}uth and T. Meier and B. Wolff},
booktitle = {Proceedings of the ``International Workshop for Tool
Support in Verification and Validation{\'{}}{\'{}}},
editor = {K.Berghammer, J.Peleska, B. Buth},
publisher = {Shaker Verlag},
series = {BISS Monographs},
title = {Generic Interfaces for Transformation Systems and
Interactive Theorem Provers. },
year = 1997,
ps = {http://www.informatik.uni-bremen.de/~bu/papers/tsv.ps.gz},
language = {USEnglish},
classification = {workshop}
}
@inproceedings{klsw95,
author = {B. Krieg-Br{\"u}ckner and J. Liu and H. Shi and B. Wolff},
booktitle = {KORSO --- Methods, Languages, and Tools for the
Construction of Correct Software},
editor = {M. Broy and S. J{\"a}hnichen},
pages = {270--284},
publisher = {Springer Verlag},
series = {LNCS 1009},
title = {Towards Correct, Efficient and Re-usable Transformational
Developments},
year = 1995,
ps = {http://www.informatik.uni-bremen.de/~bu/papers/klsw37.kurz.ps.gz},
language = {USEnglish},
classification = {workshop}
}
@inproceedings{ksw96a,
author = {Kolyang and T. Santen and B. Wolff},
booktitle = {FME 96 --- Industrial Benefits and Advances in Formal
Methods},
editor = {M.-C. Gaudel and J. Woodcock},
pages = {629--648},
publisher = {Springer Verlag},
series = {LNCS 1051},
title = {Correct and User-Friendly Implementation of Transformation Systems},
year = 1996,
abstract = {We present an approach to integrate several existing tools
and methods to a technical framework for correctly
developing and executing program transformations. The
resulting systems enable program derivations in a
user-friendly way. We illustrate the approach by proving
and implementing the transformation Global Search on the
basis of the tactical theorem prover Isabelle. A graphical
user-interface based on the X-Window toolkit Tk provides
user friendly access to the underlying machinery.},
ps = {http://www.lri.fr/~wolff/papers/conf/yats.ps.gz},
pdf = {http://www.lri.fr/~wolff/papers/conf/yats.pdf},
language = {USEnglish},
doi = {10.1007/3-540-60973-3_111},
classification = {conference}
}
@inproceedings{ksw96b,
author = {Kolyang and T. Santen and B. Wolff},
booktitle = {Theorem Proving in Higher Order Logics --- 9th
International Conference},
editor = {J. von Wright and J. Grundy and J. Harrison},
pages = {283--298},
publisher = {Springer Verlag},
series = {LNCS 1125},
title = {A Structure Preserving Encoding of Z in Isabelle/HOL},
year = 1996,
comment = {The distributed version is slightly corrected w.r.t. the
original one.},
ps = {http://www.lri.fr/~wolff/papers/conf/SPEZ_HOL.R.23.ps.gz},
pdf = {http://www.lri.fr/~wolff/papers/conf/SPEZ_HOL.R.23.pdf},
language = {USEnglish},
abstract = {We present a semantic representation of the core concepts
of the specification language Z in higher-order logic.
Although it is a ``shallow embedding{\'{}}{\'{}} like the
one presented by Bowen and Gordon, our representation
preserves the structure of a Z specification and avoids
expanding Z schemas. The representation is implemented in
the higher- order logic instance of the generic theorem
prover Isabelle. Its parser can convert the concrete syntax
of Z schemas into their semantic representation and thus
spare users from having to deal with the representation
explicitly. Our representation essentially conforms with
the latest draft of the Z standard and may give both a
clearer understanding of Z schemas and inspire the
development of proof calculi for Z.},
classification = {conference}
}
@inproceedings{kw95,
author = {Kolyang and B. Wolff},
booktitle = {Beitr{\"a}ge der GI-Fachtagung ``Softwaretechnik
95{\'{}}{\'{}}, Braunschweig},
editor = {G. Snelting},
pages = {57--66},
publisher = {GI},
series = {Mitteilungen der Fachgruppen `Software Engineering{\'{}}
und `Requirements-Engineering{\'{}},Band 15, Heft 3, ISSN
0720-8928},
title = {Development by Refinement Revisited: Lessons learnt from an example.},
year = {1995},
ps = {http://www.informatik.uni-bremen.de/~bu/papers/LEX.ps.gz},
language = {USEnglish},
classification = {workshop}
}
@article{luth.ea:functional:1999,
author = {Christoph L{\"u}th and Burkhart Wolff},
title = {Functional Design and Implementation of Graphical User
Interfaces for Theorem Provers},
journal = {Journal of Functional Programming},
year = 1999,
volume = 9,
number = 2,
pages = {167-- 189},
classification = {journal},
doi = {10.1017/S0956796899003421},
month = march,
abstract = {This paper attempts to develop a metaphor suited to
visualize the LCF-style prover design, and a methodology
for the implementation of graphical user interfaces for
these provers and encapsulations of formal methods. In this
problem domain, particular attention has to be paid to the
need to construct a variety of objects, keep track of their
interdependencies and provide support for their
reconstruction as a consequence of changes. We present a
prototypical implementation of a generic and
open interface system architecture, and show how
it can be instantiated to an interface for Isabelle, called
IsaWin, as well as to a tailored tool for transformational
program development, called TAS.},
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.ps.gz},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.pdf}
}
@inproceedings{luth.ea:hol-z:1998,
author = {Chritoph L{\"u}th and Einar W. Karlsen and Kolyang and
Stefan Westmeier and Burkhart Wolff},
classification = {conference},
booktitle = {11. International Conference of Z Users ZUM'98},
editor = {J. Bowen},
pages = {116--134},
publisher = {Springer Verlag},
series = {LNCS 1493},
title = {{HOL-Z} in the {UniForM-Workbench} -- a Case Study in Tool
Integration for Z},
year = 1998,
doi = {10.1007/BFb0056029},
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1998/zinuniform.ps.gz},
abstract = {The UniForM-Workbench is an open tool-integration
environment providing type-safe communication, a toolkit
for graphical user-interfaces, version management and
configuration management. We demonstrate how to integrate
several tools for the Z specification language into the
workbench, obtaining an instantiation of the workbench
suited as a software development environment for Z. In the
core of the setting, we use the encoding HOL-Z of Z into
Isabelle as semantic foundation and for formal reasoning
with Z specifications. In addition to this, external tools
like editors and small utilities are integrated, showing
the integration of both self-developed and externally
developed tools. The resulting prototype demonstrates the
viability of our approach to combine public domain tools
into a generic software development environment using a
strongly typed functional language. }
}
@inproceedings{luth.ea:more:2000,
author = {Christoph L{\"u}th and Burkhart Wolff},
title = {More about {TAS} and {IsaWin}: Tools for Formal Program
Development},
editor = {T. Maibaum},
booktitle = {Fundamental Approaches to Software Engineering {FASE 2000}.
Joint European Conferences on Theory and Practice of
Software {ETAPS 2000}},
year = 2000,
language = {USenglish},
classification = {conference},
series = {Lecture Notes in Computer Science},
pages = {367-- 370},
publisher = {Springer Verlag},
number = 1783,
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/sysdesc.ps.gz},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/sysdesc.pdf.gz},
abstract = {We present a family of tools for program development and
verification, compris\- ing the transformation system TAS
and the theorem proving interface IsaWin. Both are based on
the theorem prover Isabelle, which is used as a generic
logical framework here. A graphical user interface, based
on the principle of di\- rect manipulation, allows the user
to interact with the tool without having to concern himself
with the details of the representation within the theorem
prover, leaving him to concentrate on the main design
decisions of program development or theorem proving. The
tools form an integrated system for formal program
development, in which TAS is used for transformational
program development, and IsaWin for discharging the
incurred proof obligations. However, both tools can be used
sep\- arately as well. Further, the tools are generic over
the formal method employed. In this extended abstract, we
will first give a brief overview over TAS and IsaWin. Since
TAS and IsaWin have been presented on previous ETAPS
conferences, the presentation will highlight the new
features as sketched out below. }
}
@techreport{luth.ea:smltk:2001,
abstract = {In this reference manual, we describe the SML-based
programming environment sml_tk for graphical user
interfaces, version 3.0. sml_tk is based on the highly
portable X-Window Toolkit Tk (and uses internally the
Tcl/Tk interpreter wish), but offers functional abstraction
over Tk and an own component library for graphical standard
widgets such as info-boxes, treelist-widgets, tabs and
tables. sml_tk is the basic library for a collection of
GUIs for formal method tools such as TAS and IsaWin.},
author = {Christoph L{\"u}th and Burkhart Wolff},
classification = {unrefereed},
institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
language = {english},
month = {July},
number = 158,
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2001/manual.pdf},
title = {sml\_tk: Functional Programming for GUIs -- Reference
Manual},
year = 2001
}
@inproceedings{luth.ea:tas:2000,
author = {Christoph L{\"u}th and Burkhart Wolff},
title = {{TAS} --- A Generic Window Inference System},
editor = {J. Harrison and M. Aagaard},
booktitle = {Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000},
year = 2000,
classification = {conference},
series = {Lecture Notes in Computer Science},
pages = {405--422},
publisher = {Springer Verlag},
number = 1869,
pdf = {http://www.lri.fr/~wolff/papers/conf/TAS-tphols00.pdf},
language = {USenglish},
abstract = {This paper presents work on technology for
transformational proof and program development, as used by
window inference calculi and transformation systems. The
calculi are characterised by a certain class of theorems in
the underlying logic. Our transformation system TAS
compiles these rules to concrete deduction support,
complete with a graphical user interface with
command-language-free user interaction by gestures like
drag&drop and proof-by-pointing, and a development
management for transformational proofs. It is
generic in the sense that it is completely
independent of the particular window inference or
transformational calculus, and can be instantiated to many
different ones; three such instantiations are presented in
the paper.}
}
@inproceedings{lwkww98a,
author = {C. L{\"u}th and E. W. Karlsen and Kolyang and S. Westmeier
and B. Wolff},
booktitle = {Workshop on Tool Support for System Specification,
Development, and Verification},
editor = {Berghammer and Hoffmann},
title = {Tool integration in the UniForM Workbench},
year = 1998,
ps = {http://www.lri.fr/~wolff/papers/conf/tools.ps.gz},
language = {USEnglish},
abstract = {The UniForM-Workbench is an open tool-integration
environment providing type-safe communication, a toolkit
for graphical user-interfaces, version management and
configuration management. We demonstrate how to integrate
several tools for the Z specification language into the
workbench, obtaining an instantiation of the workbench
suited as a software development environment for Z. In the
core of the setting, we use the encoding HOL-Z of Z into
Isabelle as semantic foundation and for formal reasoning
with Z specifications. In addition to this, external tools
like editors and small utilities are integrated, showing
the integration of both self-developed and externally
developed tools. The resulting prototype demonstrates the
viability of our approach to combine public domain tools
into a generic software development environment using a
strongly typed functional language. },
classification = {workshop}
}
@techreport{lww96,
author = {C. L{\"u}th and S. Westmeier and B. Wolff},
institution = {Universit{\"a}t Bremen},
title = {sml_tk: Functional Programming for Graphical User
Interfaces},
number = {8/96},
year = 1996,
comment = {outdated version 2.1},
ps = {http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/Titel.ps.gz;
http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/DOC.ps.gz},
language = {USEnglish},
classification = {unrefereed}
}
@inproceedings{meyer.ea:correct:2000,
author = {T. Meyer and Burkhart Wolff},
title = {Correct Code-Generation in a Generic Framework},
editor = {M. Aargaard and J. Harrison and T. Schubert},
classification = {workshop},
booktitle = {TPHOLs 2000: Supplemental Proceedings},
year = 2000,
series = {OGI Technical Report CSE 00-009},
pages = {213--230},
month = jul,
organization = {Oregon Graduate Institute, Portland, USA},
ps = {http://www.lri.fr/~wolff/papers/conf/CodeGen.ps.gz},
pdf = {http://www.lri.fr/~wolff/papers/conf/CodeGen.pdf},
language = {USenglish},
abstract = {One major motivation for theorem provers is the
development of verified programs. In particular, synthesis
or transformational development techniques aim at a
formalised conversion of the original specification to a
final formula meeting some notion of executability. We
present a framework to describe such notions, a method to
formally investigate them and instantiate it for three
executable languages, based on three different forms of
recursion (two denotational and one based on well-founded
recursion) and develop their theory in Isabelle/HOL. These
theories serve as a semantic interface for a generic
code-generator which is set up for each program notion with
an individual code-scheme for SML.}
}
@incollection{meyer.ea:tactic-based:2005,
abstract = {Within a framework of correct code-generation from
HOLspecifications, we present a particular instance
concerned with the optimized compilation of a lazy language
(called MiniHaskell) to a strict language (called MiniML).
Both languages are defined as shallow embeddings into
denotational semantics based on Scott s cpo s, leading to a
derivation of the corresponding operational semantics in
order to cross-check the basic definitions. On this basis,
translation rules from one language to the other were
formally derived in Isabelle/HOL. Particular emphasis is
put on the optimized compilation of function applications
leading to the side-calculi inferring e.g. strictness of
functions. The derived rules were grouped and set-up as an
instance of our generic, tactic-based translator for
specifications to code.},
author = {Thomas Meyer and Burkhart Wolff},
booktitle = {Types for Proofs and Programs (TYPES 2004)},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/11617990_13},
editor = {Jean-Christophe Filliatre and Christine Paulin and Benjamin Werner},
language = {USenglish},
month = 8,
pages = {202--215},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2005/2_optcom.pdf},
publisher = {Springer Verlag},
series = {LNCS 3839},
title = {Tactic-based Optimized Compilation of Functional
Programs},
year = 2005,
classification = {workshop},
user = {wolff}
}
@inproceedings{rauch.ea:formalizing:2003,
abstract = {We present a formal model of the Java two's-complement
integral arithmetics. The model directly formalizes the
arithmetic operations as given in the Java Language
Specification (JLS). The algebraic properties of these
definitions are derived. Underspecifications and
ambiguities in the JLS are pointed out and clarified. The
theory is formally analyzed in Isabelle/HOL, that is,
machine-checked proofs for the ring properties and
divisor/remainder theorems etc. are provided. This work is
suited to build the framework for machine-supported
reasoning over arithmetic formulae in the context of Java
source-code verification.},
author = {Nicole Rauch and Burkhart Wolff},
booktitle = {Electronic Notes in Theoretical Computer Science},
language = {USenglish},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2003/0_fmics03.pdf},
classification = {workshop},
publisher = {Elsevier Science Publishers},
title = {Formalizing Java's Two's-Complement Integral Type in
Isabelle/HOL},
volume = 80,
year = 2003
}
@techreport{rauch.ea:formalizing:2004,
abstract = {We present a formal model of Java two’s-complement
integral arithmetics. The model directly formalizes the
artihmetic operations as given in the Java Language
Specification (JLS). The algebraic properties of these
definitions are derived. Underspecifications and
ambiguities in the JLS are pointed out and clarified. The
theory is formally analyzed in Isabelle/HOL that is,
machine-checked proofs for the ring properties and
divisor/remainder theorems etc. are provided. This work is
suited to build the framework for machine-supported
reasoning over arithmetic formulae in the context of Java
source-code verification. },
author = {Nicole Rauch and Burkhart Wolff},
institution = {ETH Z\"urich},
language = {USenglish},
month = 11,
number = 458,
pdf = {old papers},
title = {Formalizing Java's Two's-Complement Integral Type in
Isabelle/HOL},
year = 2004,
classification = {unrefereed},
user = {wolff}
}
@inproceedings{tw97,
author = {H. Tej and B. Wolff},
booktitle = {Proceedings of the FME 97 --- Industrial Applications and
Strengthened Foundations of Formal Methods},
editor = {J. Fitzgerald and C.B. Jones and P. Lucas},
pages = {318--337},
publisher = {Springer Verlag},
series = {LNCS 1313},
title = {A Corrected Failure-Divergence Model for CSP in
Isabelle/HOL},
year = 1997,
ps = {http://www.lri.fr/~wolff/papers/conf/CSP.ps.gz},
pdf = {http://www.lri.fr/~wolff/papers/conf/CSP.pdf},
language = {USEnglish},
doi = {10.1007/3-540-63533-5_17},
abstract = {We present a failure-divergence model for CSP following
the concepts of [BR 85]. Its formal representation within
higher order logic in the theorem prover Isabelle/HOL [Pau
94] revealed an error in the basic definition of CSP
concerning the treatment of the termination symbol tick. A
corrected model has been formally proven consistent with
Isabelle HOL. Moreover, the changed version maintains the
essential algebraic properties of CSP. As a result, there
is a proven correct implementation of a ``CSP
workbench{\'{}}{\'{}} within Isabelle. },
classification = {conference}
}
@unpublished{LTW98,
author = {Haykal Tej and Christoph L\"uth and Burkhart Wolff},
title = {Generic Transformational Program Development.},
note = {Unpublished Paper.},
pdf = {http://www.lri.fr/~wolff/papers/conf/gentraf.pdf},
year = 1998,
classification = {unrefereed}
}
@incollection{wenzel.ea:building:2007,
abstract = {We present the generic system framework of
Isabelle/Isarunderlying recent versions of Isabelle. Among
other things, Isar provides an infrastructure for Isabelle
plug-ins, comprising extensible state components and
extensible syntax that can be bound to tactical ML
programs. Thus the Isabelle/Isar architecture may be
understood as an extension and refinement of the
traditional "LCF approach", with explicit infrastructure
for building derivative systems. To demonstrate the
technical potential of the framework, we apply it to a
concrete formalmethods tool: the HOL-Z 3.0 environment,
which is geared towards the analysis of Z specifications
and formal proof of forward-refinements.},
author = {Makarius Wenzel and Burkhart Wolff},
booktitle = {TPHOLs 2007},
copyright = {\copyright Springer-Verlag},
doi = {10.1007/978-3-540-74591-4_26},
editor = {Klaus Schneider and Jens Brandt},
language = {USenglish},
pages = {351--366},
pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2007/tphols07.submission.pdf},
publisher = {Springer-Verlag},
series = {LNCS 4732},
title = {Building Formal Method Tools in the Isabelle/Isar Framework},
year = 2007,
classification = {conference},
user = {wolff}
}
@thesis{wolff05,
author = {Burkhart Wolff},
title = {Correct Tools for Formal Methods in Software Engineering},
publisher = {Universit{\"a}t Freiburg},
year = 2005,
language = {USEnglish},
abstract = {The development of \emph{tools} for program analysis,
verification and refinement is a prerequisite for the
proliferation of formal methods in industry and research.
While most tools were directly implemented in a programming
language, the ultimate goal of this work is to represent
widely known formal methods in a so-called \emph{logical
framework} \textbf{by their semantics} using a particular
representation technique --- called \emph{shallow
embedding} --- motivated by more efficient deduction. Based
on this representation, symbolic computations in tool
implementations can be based on formally proven correct
\emph{derived rules}. As such, this correctness-oriented
approach has been known for a while and has been criticized
for a number of shortcomings: \begin{enumerate} \item the
application range of embeddings in logical frameworks is
limited to very small and artificially designed languages,
\item their application is impossible when the formal
specification method is still under development, \item
embedding the semantics conservatively and deriving some
rules on this basis does not imply that there is a
comprehensive support of a method that is technically
powerful enough for applications, \item the integration in
a more global software engineering process and its
pragmatics is too difficult, and \item the usability of
embeddings is doubtful even if one is targeting at the
(fairly small market of) proof environments.
\end{enumerate} In contrast to this criticism, we claim
that our approach is feasible. We substantiate this by
developing: \begin{enumerate} \item suitable embeddings for
widely used formal methods, including process-oriented,
data-oriented and object-oriented specification methods
(CSP, Z, UML/OCL), \item abstractions and aspect-oriented
structuring techniques allowing for the quick development
of semantic variants enabling the study consequences of
changes in formal methods under development (like UML/OCL),
\item particular techniques for generating library
theories, for supporting particular deduction styles in
proofs, for specialized deduction support for concrete
development methodologies, \item different scenarios of the
integration of the developed tools in conventional tool
chains in software engineering, and \item front-ends for
light-weight integration into tool chains (like HOL-Z 2.0)
or prototypic encapsulation of logical embeddings into
generic graphical user-interfaces for a more comprehensive
encapsulation. \end{enumerate} Finally, we validate one of
these tool chains (HOL-Z 2.0) by a substantial case-study
in the field of computer security. },
note = {Habilitationsschrift},
classification = {book},
url = {http://www.lri.fr/~wolff/papers/other/habilschrift.pdf}
}
@phdthesis{wolff97,
author = {B. Wolff},
title = {A Generic Calculus of Transformations},
school = {Universit{\"a}t Bremen},
pubisher = {Shaker-Verlag},
address = {Aachen},
isbn = {3-8265-3654-1},
year = 1997,
ps = {http://www.lri.fr/~wolff/papers/other/diss.tar.gz},
language = {USEnglish},
abstract = {\textbf{Binding structures} enrich traditional abstract
syntax by providing support for representing binding
mechanisms (based on deBruijn indices), term-schemata and a
very clean algebraic theory of substitution. We provide the
following main results: \begin{itemize} \item The
establishment of a \emph{generic} binding structure with
the novel concept of effect-binding that enables the
representations of both signatures and formulas (i.e.
specifications) inside one term meta- language, \item The
foundation of a formal (machine-assisted) substitution
theory of effect-binding that is well-suited for
mechanisation. This may contribute to the construction of
tools such as theorem provers, program transformers, static
analysers, evaluators and optimising compilers, \item The
foundation of a rigorous meta-theory for rewriting on
effect- binding-structures. The resulting rewrite notion
transformation extends combinatory rewrite systems to
rewrites on specifications. \end{itemize} The corner stone
of this theory is a confluence proof for orthogonal
transformations (partly implemented in the proof assistant
Isabelle). },
classification = {book}
}
@techreport{wolff:ea:mixe:2002,
author = {Burkhart Wolff and Oliver Berthold and Sebastian Clau{\ss}
and Hannes Federrath and Stefan K{\"o}psell and Andreas
Pfitzmann},
title = {Towards a Formal Analysis of a Mix Network},
institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
year = 2002,
series = {Technical Report},
number = 171,
issn = 14341719,
pdf = {http://www.lri.fr/~wolff/papers/other/tr01.pdf},
language = {USEnglish},
classification = {unrefereed}
}
@inproceedings{wolff:verifying:2001,
abstract = {Binding structures enrich traditional abstract syntax by
provi-ding support for representing binding mechanisms
(based on deBruijn indices), term-schemata and a very clean
algebraic theory of substitution. Weprovide a novel binding
structure with the following main results: 1) The
formalisation of a generic binding structure with the novel
conceptof effect-binding that enables the explicit
representations of both contexts and terms inside one term
meta-language,2) The foundation of a formal
(machine-assisted) substitution theory of effect-binding
that is well-suited for mechanisation. This can be used for
thesystematic and correct development of new calculi with
explicit substitutions.The substitution theory is formally
proven in Isabelle/HOL; the implementation may serve as
(untyped) framework for deep embeddings.},
author = {Burkhart Wolff},
classification = {proceedings},
booktitle = {Workshop on Explicit Substitution Theory and Applications
(WESTAPP'01)},
editor = {Pierre Lescanne},
isbn = {90-393-2764-5},
language = {english},
month = {May},
pages = {58 -- 71},
ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2001/BiSE.ps.gz},
publisher = {Department of Philosophy - Utrecht University},
series = {Logic Group Preprint Series},
title = {Verifying Explicit Substitution Calculi in Binding
Structures with Effect Binding},
classification = {workshop},
volume = 210,
year = 2001
}
@incollection{brucker.ea:ocl-null:2009,
author = {Achim D. Brucker and Matthias P. Krieger and Burkhart
Wolff},
booktitle = {MODELS 2009 Workshops},
series = {LNCS 6002},
editor = {S. Ghosh},
pages = {261--275},
language = {USenglish},
publisher = {Springer Verlag, Heidelberg},
title = {Extending {OCL} with Null-References},
year = 2009,
classification = {workshop},
categories = {holocl},
location = {Denver, Colorado, \acs{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 \holocl 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},
ps = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.ps.gz},
keywords = {\holocl, UML, OCL, null reference, formal semantics},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009},
note = {Best-Paper Award at the OCL 2009 Workshop.},
ee = {http://dx.doi.org/10.1007/978-3-642-12261-3_25},
doi = {10.1007/978-3-642-12261-3_25}
}
@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 = {April},
number = 670,
pdf = {http://www.lri.fr/~wolff/papers/other/HOL-TestGen_UserGuide.pdf},
title = {{HOL-TestGen} 1.5.0 User Guide},
year = 2010
}
This file was generated by bibtex2html 1.94.