@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}{} }}
@article{DBLP:journals/afp/BruckerMW24,
author = {Achim D. Brucker and
Nicolas M{\'{e}}ric and
Burkhart Wolff},
title = {Isabelle/DOF},
journal = {Arch. Formal Proofs},
volume = {2024},
year = {2024},
url = {https://www.isa-afp.org/entries/Isabelle\_DOF.html},
timestamp = {Mon, 27 May 2024 11:08:41 +0200},
biburl = {https://dblp.org/rec/journals/afp/BruckerMW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/zum/BallenghienW24,
author = {Beno{\^{\i}}t Ballenghien and
Burkhart Wolff},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Event-B as {DSL} in Isabelle and {HOL} Experiences from a Prototype},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {241--247},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_18},
doi = {10.1007/978-3-031-63790-2\_18},
timestamp = {Fri, 19 Jul 2024 23:15:46 +0200},
biburl = {https://dblp.org/rec/conf/zum/BallenghienW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
pdf = {http://www.lri.fr/~wolff/papers/conf/2024-ABZ-HOL-B.pdf}
}
@inproceedings{Brucker_2024_IsaWS,
author = {Brucker, Achim D. and Meric, Nicolas and Wolff, Burkhart},
title = {Isabelle/DOF -- Extended Abstract and Tool Demonstration},
booktitle = {Proceedings of the ISABELLE WORKSHOP 2024 as part of ITP 2024, TBlissi, Georgia},
series = {SKETIS '24},
year = {2024},
location = {TBlissi, Georgia},
pages = {19--24},
pdf = {http://www.lri.fr/~wolff/papers/workshop/Brucker_2024_IsaWS.pdf},
classification = {workshop}
}
@article{HOL-CSP_OpSem-AFP,
author = {Beno{\^{\i}}t Ballenghien and Burkhart Wolff},
title = {Operational Semantics formally proven in HOL-CSP},
journal = {Archive of Formal Proofs},
month = {December},
year = {2023},
note = {\url{https://isa-afp.org/entries/HOL-CSP_OpSem.html},
Formal proof development},
issn = {2150-914x}
}
@article{HOL-CSP-AFP,
author = {Safouan Taha and Lina Ye and Burkhart Wolff},
title = {HOL-CSP Version 2.0},
journal = {Archive of Formal Proofs},
month = {April},
year = {2019},
note = {\url{https://isa-afp.org/entries/HOL-CSP.html},
Formal proof development},
issn = {2150-914x}
}
@article{HOL-CSPM-AFP,
author = {Beno{\^{\i}}t Ballenghien and Safouan Taha and Burkhart Wolff},
title = {HOL-CSPM - Architectural operators for HOL-CSP},
journal = {Archive of Formal Proofs},
month = {December},
year = {2023},
note = {\url{https://isa-afp.org/entries/HOL-CSPM.html},
Formal proof development},
issn = {2150-914x}
}
@techreport{wolff:hal-03429597,
title = {{Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP}},
author = {Crisafulli, Paolo and Taha, Safouan and Wolff, Burkhart},
url = {hal-03627500},
type = {Research Report},
institution = {{University Paris-Saclay ; IRT SystemX, Palaiseau}},
year = {2021},
month = oct,
pdf = {https://www.lri.fr/~wolff/papers/other/MPSAC-HOL-CSP.pdf},
hal_id = {hal-03627500},
hal_version = {v3}
}
@article{RAS-CTW-CPSinCSP,
title = {Modeling and analysing {C}yber \– {P}hysical Systems in {HOL-CSP}},
journal = {Robotics and Autonomous Systems},
volume = {170},
pages = {104549},
year = {2023},
issn = {0921-8890},
doi = {https://doi.org/10.1016/j.robot.2023.104549},
url = {https://www.sciencedirect.com/science/article/pii/S0921889023001884},
author = {Paolo Crisafulli and Safouan Taha and Burkhart Wolff},
pdf = {https://www.lri.fr/~wolff/papers/journals/2023-RAS-CPS-HOL_CSP.pdf},
keywords = {Cyber–Physical Systems, Autonomous cars, Safety-critical systems, Process-algebra, Concurrency, Proof-based verification},
abstract = {Modelling and Analysing Cyber-Physical Systems (CPS) is a challenge for Formal Methods and therefore a
field of active research. It is characteristic of CPSs that models comprise aspects of Newtonian Physics
appearing in system environments, the difficulties of their discretization, the problems of communication
and interaction between actors in this environment as well as calculations respecting time-bounds. We present
a novel framework to address these problems developed with industrial partners involved in the Autonomous
Car domain. Based on HOL-CSP, we model time, physical evolution, "scenes” (global states) and "scenarios"
(traces) as well as the interaction of "actors" (vehicles, pedestrians, traffic lights) inside this framework.
In particular, discrete samplings are modelled by infinite internal choices. For several instances of the
modelling framework, we give formal proofs of a particular safety property for Autonomous Cars: if each car
follows the same driving strategy defined by the so-called Responsibility-Sensitive Safety (RSS), no collision
will occur. The proofs give rise to a number of variants of RSS and optimizations as well as a test-case
partitioning of abstract test cases and a test-strategy for integration tests.}
}
@inproceedings{bsmw2023,
author = {Achim D. Brucker and
Idir A{\"{\i}}t{-}Sadoune and
Nicolas M{\'{e}}ric and
Burkhart Wolff},
editor = {Uwe Gl{\"{a}}sser and
Jos{\'{e}} Creissac Campos and
Dominique M{\'{e}}ry and
Philippe A. Palanque},
title = {Using Deep Ontologies in Formal Software Engineering},
booktitle = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14010},
pages = {15--32},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-33163-3\_2},
doi = {10.1007/978-3-031-33163-3\_2},
timestamp = {Fri, 02 Jun 2023 21:23:53 +0200},
pdf = {https://www.lri.fr/~wolff/papers/conf/2023-ABZ-ontologies.pdf}
}
@proceedings{FosterWolffICECCS2023,
editor = {Yamine Ait-Ameur and Ferhat Khendek},
title = {Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL},
booktitle = {27th International Conference on Engineering of Complex Computer Systems,
{ICECCS} 2023, Toulouse, France, June 14-16, 2023},
publisher = {{IEEE}},
year = {2023},
pdf = {https://www.lri.fr/~wolff/papers/conf/2023FosterWolffICECCS.pdf},
url = {https://arxiv.org/pdf/2302.07629.pdf}
}
@article{DBLP:journals/afp/FosterW20,
author = {Simon Foster and
Burkhart Wolff},
title = {A Sound Type System for Physical Quantities, Units, and Measurements},
journal = {Arch. Formal Proofs},
volume = {2020},
year = {2020},
url = {https://www.isa-afp.org/entries/Physical\_Quantities.html},
timestamp = {Thu, 10 Dec 2020 12:37:34 +0100},
biburl = {https://dblp.org/rec/journals/afp/FosterW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/TahaWY20,
author = {Safouan Taha and
Burkhart Wolff and
Lina Ye},
title = {The {HOL-CSP} Refinement Toolkit},
journal = {Arch. Formal Proofs},
volume = {2020},
year = {2020},
url = {https://www.isa-afp.org/entries/CSP\_RefTK.html},
timestamp = {Wed, 17 Feb 2021 16:35:22 +0100},
biburl = {https://dblp.org/rec/journals/afp/TahaWY20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jot/BruckerTW20,
author = {Achim D. Brucker and
Fr{\'{e}}d{\'{e}}ric Tuong and
Burkhart Wolff},
title = {Model Transformation as Conservative Theory-Transformation},
journal = {J. Object Technol.},
volume = {19},
number = {3},
pages = {3:1--16},
year = {2020},
url = {https://doi.org/10.5381/jot.2020.19.3.a3},
doi = {10.5381/jot.2020.19.3.a3},
timestamp = {Tue, 03 Nov 2020 08:17:34 +0100},
biburl = {https://dblp.org/rec/journals/jot/BruckerTW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/simeuro/VanBW20,
author = {Hai Nguyen Van and
Fr{\'{e}}d{\'{e}}ric Boulanger and
Burkhart Wolff},
title = {Timed Discrete-Event Simulation of Aviation Scenarios},
journal = {Simul. Notes Eur.},
volume = {30},
number = {2},
pages = {51--60},
year = {2020},
url = {https://doi.org/10.11128/sne.30.tn.10512},
doi = {10.11128/sne.30.tn.10512},
timestamp = {Thu, 16 Jul 2020 17:14:17 +0200},
biburl = {https://dblp.org/rec/journals/simeuro/VanBW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ifm/TahaWY20,
author = {Safouan Taha and
Burkhart Wolff and
Lina Ye},
editor = {Brijesh Dongol and
Elena Troubitsyna},
title = {Philosophers May Dine - Definitively!},
booktitle = {Integrated Formal Methods - 16th International Conference, {IFM} 2020,
Lugano, Switzerland, November 16-20, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12546},
pages = {419--439},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-63461-2\_23},
doi = {10.1007/978-3-030-63461-2\_23},
timestamp = {Tue, 17 Nov 2020 15:23:51 +0100},
biburl = {https://dblp.org/rec/conf/ifm/TahaWY20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{brucker.ea:ontologies-certification:2019,
abstract = { A common problem in the certification of highly safety or security critical systems is the
consistency of the certification documentation in general and, in particular, the linking between
semi-formal and formal content of the certification documentation.
We address this problem by using an existing framework, Isabelle/DOF, that allows writing
certification documents with consistency guarantees, in both, the semi-formal and formal parts.
Isabelle/DOF supports the \emph{modeling} of document ontologies using a strongly typed ontology
definition language. An ontology is then \emph{enforced} inside documents including formal parts,
e.g., system models, verification proofs, code, tests and validations of corner-cases. The entire set
of documents is checked within Isabelle/HOL, which includes the definition of ontologies and the
editing of integrated documents based on them. This process is supported by an IDE that provides
continuous checking of the document consistency.
In this paper, we present how a specific software-engineering certification standard, namely CENELEC
50128, can be modeled inside Isabelle/DOF. Based on an ontology covering a substantial part of this
standard, we present how Isabelle/DOF can be applied to a certification case-study in the railway
domain.},
keywords = {Certification of Safety-Critical Systems, CENELEC 50128, Formal Document Development, Isabelle/DOF,
Isabelle/HOL},
location = {Bergen},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Integrated Formal Methods (iFM)},
language = {USenglish},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-ontologies-certification-2019},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {11918},
isbn = {3-540-25109-X},
doi = {10.1007/978-3-030-34968-4_4},
editor = {Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa},
pdf = {https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf},
title = {{U}sing {O}ntologies in {F}ormal {D}evelopments {T}argeting {C}ertification},
classification = {conference},
areas = {formal methods, software},
categories = {isadof},
year = {2019},
public = {yes}
}
@incollection{HOL-CSP-iFM2020,
keywords = {Process-Algebra, Concurrency, Computational Models, Parametric System Verification},
author = {Safouan Taha and Lina Ye and Burkhart Wolff},
booktitle = {Integrated Formal Methods (iFM)},
language = {USenglish},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {12546},
doi = {10.1007/978-3-030-63461-2_23},
editor = {Carlo A. Furia},
title = {{P}hilosophers may {D}ine - {D}efinitively!},
pdf = {https://www.lri.fr/~wolff/papers/conf/2020-iFM_CSP.pdf},
classification = {conference},
areas = {formal methods, software},
year = {2020},
public = {yes}
}
@incollection{Tuong-IsabelleC:2019,
abstract = {We present a framework for C code in C11 syntax deeply
integrated into the Isabelle/PIDE devel- opment environment. Our framework
provides an abstract interface for verification back-ends to be plugged-in
independently. Thus, various techniques such as deductive program
verification or white- box testing can be applied to the same source,
which is part of an integrated PIDE document model. Semantic back-ends
are free to choose the supported C fragment and its semantics. In
particular, they can differ on the chosen memory model or the specification
mechanism for framing conditions.
Our framework supports semantic annotations of C sources in the form of
comments. Annota- tions serve to locally control back-end settings, and can
express the term focus to which an annotation refers. Both the logical and
the syntactic context are available when semantic annotations are evaluated.
As a consequence, a formula in an annotation can refer both to HOL or C
variables.
Our approach demonstrates the degree of maturity and expressive power the
Isabelle/PIDE sub-system has achieved in recent years. Our integration
technique employs Lex and Yacc style grammars to ensure efficient
deterministic parsing. We present two case studies for the integration of
(known) semantic back-ends in order to validate the design decisions for
our back-end interface.
},
address = {Heidelberg},
author = {Fr\'ederic Tuong and Burkhart Wolff},
booktitle = {International Workshop on Formal Integrated Development Environments (F-IDE)},
doi = {10.4204/EPTCS.310.3},
keywords = {Isabelle, HOL, C11, Program Verification, Program Testing},
language = {USenglish},
location = {Porto, Protogal},
number = {314},
pdf = {https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf},
publisher = {Open Publishing Association},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
title = {{D}eeply {I}ntegrating {C11} {C}ode {S}upport into {I}sabelle/{PIDE}},
year = {2019}
}
@misc{brucker_achim_d_2019_3370483,
author = {Brucker, Achim D. and
Wolff, Burkhart},
title = {{I}sabelle/{DOF}},
month = aug,
year = 2019,
doi = {10.5281/zenodo.3370483},
url = {https://doi.org/10.5281/zenodo.3370483}
}
@incollection{brucker.wolff:isadof-design-impl:2019,
abstract = {DOF is a novel framework for \emph{defining} ontologies and
\emph{enforcing} them during document development and document
evolution. A major goal of DOF is the integrated development of
formal certification documents (\eg, for Common Criteria or CENELEC
50128) that require consistency across both formal and informal
arguments.
To support a consistent development of formal and informal parts of
a document, we provide Isabelle/DOF, an implementation of DOF on top of
Isabelle/HOL. \isadof is integrated into Isabelle's IDE, which
allows for smooth ontology development as well as immediate
ontological feedback during the editing of a document.
In this paper, we give an in-depth presentation of the design
concepts of DOF's Ontology Definition Language (ODL) and key
aspects of the technology of its implementation. \isadof is the
first ontology language supporting machine-checked
links between the formal and informal parts in an LCF-style
interactive theorem proving environment.
Sufficiently annotated, large documents can easily be developed
collaboratively, while \emph{ensuring their consistency}, and the
impact of changes (in the formal and the semi-formal content) is
tracked automatically.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {International Conference on Software Engineering and Formal Methods (SEFM)},
doi = {10.1007/978-3-319-96812-4_3},
keywords = {Isabelle, HOL, Ontologies, Certification},
language = {USenglish},
location = {Oslo, Norway},
number = {11724},
pdf = {https://www.lri.fr/~wolff/papers/conf/2019-sefm-isa_dof-framework.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {{I}sabelle/{DOF}: {D}esign and {I}mplementation},
year = {2019}
}
@incollection{brucker.ea:isabelle-ontologies:2018,
abstract = {While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation.\\\\Up to now, Isabelle's document preparation system lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.\\\\In this paper, we present Isabelle/DOF, a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for conventional typesetting \emph{as well} as formal development. We show how to model document ontologies inside Isabelle/DOF, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support.},
address = {Heidelberg},
author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli and Burkhart Wolff},
booktitle = {Conference on Intelligent Computer Mathematics (CICM)},
doi = {10.1007/978-3-319-96812-4_3},
keywords = {Isabelle/Isar, HOL, Ontologies},
language = {USenglish},
location = {Hagenberg, Austria},
number = {11006},
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Using The Isabelle Ontology Framework: Linking the Formal with the Informal},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018},
year = {2018}
}
@inproceedings{bockenek:hal-02069705,
title = {{U}sing {I}sabelle/{UTP} for the {V}erification of {Si}orting {A}lgorithms: {A} {C}ase {S}tudy},
booktitle = {{I}sabelle {W}orkshop {part of {FLOC}'18}},
author = {Bockenek, Joshua A and Lammich, Peter and Nemouchi, Yakoub and Wolff, Burkhart},
url = {https://hal.archives-ouvertes.fr/hal-02069705},
note = {Isabelle Workshop 2018, Colocated with Interactive Theorem Proving. As part of FLOC 2018, Oxford, GB.},
year = {2018},
month = jul,
pdf = {https://www.lri.fr/~wolff/papers/conf/Isabelle_2018_paper_6.pdf},
hal_id = {hal-02069705},
hal_version = {v1}
}
@inproceedings{BCPW2018,
title = {Making Agile Development Processes fit for V-style Certification
Procedures},
author = {Bezzecchi, S. and Crisafulli, P. and Pichot, C. and Wolff, B.},
booktitle = {{ERTS'18}},
abstract = {We present a process for the development of safety and security
critical components in transportation systems targeting a high-level
certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408).
The process adheres to the objectives of an ``agile development'' in
terms of evolutionary flexibility and continuous improvement. Yet, it
enforces the overall coherence of the development artifacts (ranging from
proofs over tests to code) by a particular environment (CVCE).
In particular, the validation process is built around a formal development
based on the interactive theorem proving system Isabelle/HOL, by linking the
business logic of the application to the operating system model, down to
code and concrete hardware models thanks to a series of refinement proofs.
We apply both the process and its support in CVCE to a case-study that
comprises a model of an odometric service in a railway-system with its
corresponding implementation integrated in seL4 (a secure kernel for
which a comprehensive Isabelle development exists). Novel techniques
implemented in Isabelle enforce the coherence of semi-formal
and formal definitions within to specific certification processes
in order to improve their cost-effectiveness.
},
pdf = {https://www.lri.fr/~wolff/papers/conf/2018erts-agile-fm.pdf},
year = {2018},
series = {ERTS Conference Proceedings},
location = {Toulouse}
}
@inproceedings{AissatVW2016,
title = {Infeasible Paths Elimination by Symbolic Execution Techniques:
Proof of Correctness and Preservation of Paths},
author = {Aissat, R. and Voisin, F. and Wolff, B.},
booktitle = {{ITP'16}},
abstract = {TRACER is a tool for verifying safety properties of sequential C
programs. TRACER attempts at building a finite symbolic execution
graph which over-approximates the set of all concrete reachable
states and the set of feasible paths.
We present an abstract framework for TRACER and similar CEGAR-like
systems. The framework provides 1) a graph-transformation based
method for reducing the feasible paths in control-flow graphs, 2)
a model for symbolic execution, subsumption, predicate abstraction
and invariant generation.
In this framework we formally prove two key properties: correct
construction of the symbolic states and preservation of feasible
paths. The framework focuses on core operations, leaving to
concrete prototypes to “fit in” heuristics for combining them.},
year = {2016},
series = {Lecture Notes in Computer Science},
volume = {9762},
pdf = {https://www.lri.fr/~wolff/papers/conf/2016-itp-InfPathsNSE.pdf},
location = {Vienna}
}
@inproceedings{DBLP:conf/tap/BruckerW16,
author = {Achim D. Brucker and
Burkhart Wolff},
title = {Monadic Sequence Testing and Explicit Test-Refinements},
booktitle = {Tests and Proofs - 10th International Conference, {TAP} 2016, Held
as Part of {STAF} 2016, Vienna, Austria, July 5-7, 2016, Proceedings},
volume = {LNCS 7942},
series = {Lecture Notes in Computer Science},
pages = {17--36},
year = {2016},
abstract = {Abstract We present an abstract framework for sequence testing
that is implemented in Isabelle/HOL-TestGen. Our framework is
based on the theory of state-exception monads, explicitly modelled
in HOL, and can cope with typed input and output, interleaving
executions including abort, and synchronisation.
The framework is particularly geared towards symbolic execution
and has proven effective in several large case-studies involving
system models based on large (or infinite) state.
On this basis, we rephrase the concept of test-refinements for
inclusion, deadlock and IOCO-like tests, together with a formal
theory of its rela- tion to traditional, IO-automata based notions.},
url = {http://dx.doi.org/10.1007/978-3-319-41135-4_2},
pdf = {https://www.brucker.ch/bibliography/download/2016/brucker.ea-monadic-sequence-testing-2016.pdf},
doi = {10.1007/978-3-319-41135-4_2}
}
@inproceedings{DBLP:conf/models/BruckerCDGHHTWW16,
author = {Achim D. Brucker and
Jordi Cabot and
Gwendal Daniel and
Martin Gogolla and
Adolfo S{\'{a}}nchez{-}Barbudo Herrera and
Frank Hilken and
Fr{\'{e}}d{\'{e}}ric Tuong and
Edward D. Willink and
Burkhart Wolff},
title = {Recent Developments in {OCL} and Textual Modelling},
booktitle = {Proceedings of the 16th International Workshop on {OCL} and Textual
Modelling co-located with 19th International Conference on Model Driven
Engineering Languages and Systems {(MODELS} 2016), Saint-Malo, France,
October 2, 2016.},
pages = {157--165},
year = {2016},
url = {http://ceur-ws.org/Vol-1756/paper12.pdf},
timestamp = {Sun, 11 Dec 2016 13:10:16 +0100},
biburl = {http://dblp.org/rec/bib/conf/models/BruckerCDGHHTWW16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/afp/AissatVW16,
author = {Romain A{\"{\i}}ssat and
Fr{\'{e}}d{\'{e}}ric Voisin and
Burkhart Wolff},
title = {Infeasible Paths Elimination by Symbolic Execution Techniques: Proof
of Correctness and Preservation of Paths},
journal = {Archive of Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/InfPathElimination.shtml},
timestamp = {Thu, 17 Aug 2017 16:21:55 +0200},
biburl = {http://dblp.org/rec/bib/journals/afp/AissatVW16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@techreport{AGVW2016,
author = {Aissat, R. and Gaudel, M.-C. and Voisin, F. and Wolff, B.},
title = {Pruning Infeasible Paths via Graph Transformations and
Symbolic Execution: a Method and a Tool},
number = {1588},
institution = {L.R.I., Univ. Paris-Sud},
url = {https://www.lri.fr/srubrique.php?news=33},
year = {2016}
}
@inproceedings{DBLP:conf/qrs/AissatGVW16,
author = {Romain A{\"{\i}}ssat and
Marie{-}Claude Gaudel and
Fr{\'{e}}d{\'{e}}ric Voisin and
Burkhart Wolff},
title = {A Method for Pruning Infeasible Paths via Graph Transformations and
Symbolic Execution},
booktitle = {2016 {IEEE} International Conference on Software Quality, Reliability
and Security, {QRS} 2016, Vienna, Austria, August 1-3, 2016},
pages = {144--151},
year = {2016},
url = {https://doi.org/10.1109/QRS.2016.26},
doi = {10.1109/QRS.2016.26},
timestamp = {Thu, 17 Aug 2017 16:22:01 +0200},
biburl = {http://dblp.org/rec/bib/conf/qrs/AissatGVW16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@techreport{brucker.ea:hol-testgen:2016,
author = {Achim D. Brucker and Lukas Br{\"u}gger and Abderrahmane
Feliachi and Chantal Keller and Matthias P. Krieger and
Delphine Longuet and Yakoub Nemouchi and Fr{\'e}d{\'e}ric
Tuong and Burkhart Wolff },
institution = {Laboratoire en Recherche en Informatique (LRI),
Universit\'e Paris-Sud 11, France},
language = {USenglish},
month = apr,
title = {{HOL-TestGen} 1.8.0 User Guide},
categories = {testing,holtestgen},
classification = {unrefereed},
areas = {formal methods, software},
keywords = {symbolic test case generations, black box testing, theorem
proving, Isabelle/HOL},
year = {2016},
number = {1586},
num_pages = {111},
pdf = {https://www.brucker.ch/bibliography/download/2016/brucker.ea-hol-testgen-2016.pdf},
public = {yes},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2016}
}
@techreport{brucker.ea:formal-semantics-ocl-2.5:2015,
author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
institution = {LRI, Univ Paris Sud, CNRS, Centrale Sup\'elec,
Universit\'e Paris-Saclay, France},
language = {USenglish},
month = sep,
title = {Featherweight {OCL}: {A} {P}roposal for a {M}achine-{C}hecked {F}ormal
{S}emantics for {OCL} 2.5},
categories = {holocl},
classification = {unrefereed},
areas = {formal methods, software},
year = {2015},
number = {1582},
num_pages = {196},
public = {yes},
abstract = {The Unified Modeling Language (UML) is one of the few
modeling languages that is widely used in industry. While
UML is mostly known as diagrammatic modeling language
(e.g., visualizing class models), it is complemented by a
textual language, called Object Constraint Language (OCL).
OCL is a textual annotation language, originally based on a
three-valued logic, that turns UML into a formal language.
Unfortunately the semantics of this specification language,
captured in the ``Annex A'' of the OCL standard, leads to
different interpretations of corner cases. Many of these
corner cases had been subject to formal analysis since more
than ten years.
The situation complicated with the arrival of version 2.3
of the OCL standard. OCL was aligned with the latest
version of UML: this led to the extension of the
three-valued logic by a second exception element, called
null. While the first exception element invalid has a
strict semantics, null has a non strict interpretation. The
combination of these semantic features lead to remarkable
confusion for implementors of OCL compilers and
interpreters.
In this paper, we provide a formalization of the core of
OCL in HOL. It provides denotational definitions, a logical
calculus and operational rules that allow for the execution
of OCL expressions by a mixture of term rewriting and code
compilation. Moreover, we describe a coding-scheme for UML
class models that were annotated by code-invariants and
code contracts. An implementation of this coding-scheme has
been undertaken: it consists of a kind of compiler that
takes a UML class model and translates it into a family of
definitions and derived theorems over them capturing the
properties of constructors and selectors, tests and casts
resulting from the class model. However, this compiler is
not included in this document.
Our formalization reveals several inconsistencies and
contradictions in the current version of the OCL standard.
They reflect a challenge to define and implement OCL tools
in a uniform manner. Overall, this document is intended to
provide the basis for a machine-checked text ``Annex A'' of
the OCL standard targeting at tool implementors. },
pdf = {https://www.lri.fr/~bibli/Rapports-internes/2015/RR1582.pdf},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-semantics-ocl-2.5-2015}
}
@article{tuong.ea:meta-model:2015,
author = {Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
title = {A {M}eta-{M}odel for the {I}sabelle {API}},
journal = {Archive of Formal Proofs},
year = {2015},
url = {https://www.brucker.ch/bibliography/abstract/tuong.ea-meta-model-2015},
issn = {2150-914x},
categories = {holocl},
public = yes
}
@inbook{used-fm:2015,
author = {Yakoub Nemouchi and Abderrahmane Feliachi and
Burkhart Wolff and Cyril Proch},
year = 2015,
chapter = {Using Isabelle/HOL in Certification Processes:
A System Description and Mandatory Recommendations},
editor = {Sergey Tverdyshev and Oto Havle and Holger Blasum and Bruno Langenstein
and Werner Stephan and Abderrahmane Feliachi and Yakoub Nemouchi and
Burkhart Wolff and Cyril Proch and Freek Verbeek and Julien Schmaltz},
title = {Used Formal Methods},
publisher = {The EURO-MILS Project},
note = {available from the Project site: \url{http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper-October2015.pdf}},
doi = {http://dx.doi.org/10.5281/zenodo.47297}
}
@article{feliachi-wolff:SymbTestgenCirta:2013,
author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff},
title = {Symbolic Test-generation in {HOL}-{T}est{G}en/{C}irTA: A Case Study},
journal = {Int. J. Software Informatics},
volume = {9},
number = {2},
year = {2015},
pages = {177--203},
abstract = {HOL-TestGen/CirTA is a theorem-prover based test generation
environment for specifications written in Circus, a
process-algebraic specification language in the tradition
of CSP. HOL-TestGen/CirTA is based on a formal embedding of
its semantics in Isabelle/HOL, allowing to derive rules over
specification constructs in a logically safe way.
Beyond the derivation of algebraic laws and calculi for
process refinement, the originality of HOL-TestGen/ CirTA
consists in an entire derived theory for the generation of
symbolic test-traces, including optimized rules for test-generation
as well as rules for symbolic execution. The deduction process
is automated by Isabelle tactics, allowing to protract the
state-space explosion resulting from blind enumeration of data.
The implementation of test-generation procedures in CirTA is
completed by an integrated tool chain that transforms the
initial Circus specification of a system into a set of
equivalence classes (or “symbolic tests”), which were compiled
to conventional JUnit test-drivers.
This paper describes the novel tool-chain based on prior
theoretical work on semantics and test-theory and attempts
an evaluation via a medium-sized case study performed on a
component of a real-world safety-critical medical monitoring
system written in Java. We provide experimental measurements
of the kill-capacity of implementation mutants.},
public = yes,
url = {https://www.lri.fr/~wolff/papers/journals/2015-cirta-case-study.pdf}
}
@article{DBLP:journals/afp/BruckerBW17,
author = {Achim D. Brucker and
Lukas Br{\"{u}}gger and
Burkhart Wolff},
title = {Formal Network Models and Their Application to Firewall Policies},
journal = {Archive of Formal Proofs},
volume = {2017},
year = {2017},
url = {https://www.isa-afp.org/entries/UPF_Firewall.shtml},
timestamp = {Wed, 25 Jan 2017 16:31:56 +0100},
biburl = {http://dblp.org/rec/bib/journals/afp/BruckerBW17},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/formats/VanBBKVW17,
author = {Hai Nguyen Van and
Thibaut Balabonski and
Fr{\'{e}}d{\'{e}}ric Boulanger and
Chantal Keller and
Beno{\^{\i}}t Valiron and
Burkhart Wolff},
title = {A Symbolic Operational Semantics for {TESL} - With an Application
to Heterogeneous System Testing},
booktitle = {Formal Modeling and Analysis of Timed Systems - 15th International
Conference, {FORMATS} 2017, Berlin, Germany, September 5-7, 2017,
Proceedings},
pages = {318--334},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-65765-3_18},
doi = {10.1007/978-3-319-65765-3_18},
timestamp = {Fri, 01 Sep 2017 14:18:17 +0200},
biburl = {http://dblp.org/rec/bib/conf/formats/VanBBKVW17},
pdf = {https://www.lri.fr/~wolff/papers/conf/2017-FORMATS-TESL.pdf},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{brucker-wolff:FormalFirewallTest:2013,
author = {Achim D. Brucker and Lukas Br\"ugger and Burkhart Wolff},
title = {Formal Firewall Conformance Testing: An Application of Test and Proof Techniques},
journal = {Softw. Test., Verif. Reliab.},
volume = {25},
number = {1},
year = {2015},
pages = {34--71},
abstract = {Firewalls are an important means to secure critical ICT infrastructures. As configurable off-the-shelf products,
the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well
as the correct configuration. While testing the implementation can be done once by the manufacturer, the
configuration needs to be tested for each application individually. This is particularly challenging as the configuration,
implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and,
thus, difficult to validate.
This paper presents a formal model of both stateless and stateful firewalls (packet filters), including network
address translation (NAT), to which a specification-based conformance test case generation approach is applied. Furthermore,
a verified optimisation technique for this approach is presented: Starting from a formal model for stateless firewalls,
a collection of semantics-preserving policy transformation rules and an algorithm that optimises the specification with respect
of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates
verification and testing, i. e., tests and proofs to support conformance testing of network policies.
The presented approach is supported by a test framework that allows to test actual firewalls using the test cases
generated based on the formal model. Finally, a report on several larger case studies is presented.
},
pdf = {https://www.lri.fr/~wolff/papers/journals/2010-stvr-fw-test.pdf},
doi = {10.1002/stvr.1544}
}
@inproceedings{DBLP:conf/models/VanBBTVWY15,
author = {Hai Nguyen Van and
Thibaut Balabonski and
Fr{\'{e}}d{\'{e}}ric Boulanger and
Safouan Taha and
Beno{\^{\i}}t Valiron and
Burkhart Wolff and
Lina Ye},
title = {Towards a Formal Semantics of the {TESL} Specification Language},
booktitle = {Joint Proceedings of the 3rd International Workshop on the Globalization
Of Modeling Languages and the 9th International Workshop on Multi-Paradigm
Modeling co-located with {ACM/IEEE} 18th International Conference
on Model Driven Engineering Languages and Systems, GEMOC+MPM@MoDELS
2015, Ottawa, Canada, September 28, 2015.},
pages = {14--19},
year = {2015},
url = {http://ceur-ws.org/Vol-1511/paper-03.pdf},
timestamp = {Fri, 20 Nov 2015 15:31:33 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/models/VanBBTVWY15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{brucker.ea:ipc-testing:2015,
abstract = {In this paper, we adapt model-based testing techniques to
concurrent code, namely for test generations of an
(industrial) OS kernel called PikeOS\@. Since our
data-models are complex, the problem is out of reach of
conventional model-checking techniques. Our solution is
based on symbolic execution implemented inside the
interactive theorem proving environment Isabelle/HOL
extended by a plugin with test generation facilities called
HOL-TestGen.
As a foundation for our symbolic computing techniques, we
refine the theory of monads to embed interleaving
executions with abort, synchronization, and shared memory
to a general but still optimized behavioral test framework.
This framework is instantiated by a model of PikeOS
inter-process communication system-calls. Inheriting a
micro-architecture going back to the L4 kernel, the system
calls of the IPC-API are internally structured by atomic
actions; according to a security model, these actions can
fail and must produce error-codes. Thus, our tests reveal
errors in the enforcement of the security model.},
keywords = {test program generation, symbolic test case generations,
black box testing, testing operating systems,
certification, CC, concurrency, interleaving},
location = {San Francisco, California, USA},
author = {Achim D. Brucker and Oto Havle and Yakoub Nemouchi and
Burkhart Wolff},
title = {Testing the IPC Protocol for a Real-Time Operating
System},
booktitle = {Working Conference on Verified Software: Theories, Tools,
and Experiments},
language = {USenglish},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {9593},
isbn = {3-540-14031-X},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
pdf = {http://www.lri.fr/~wolff/papers/conf/2015-vstte-ipc-testing.pdf},
issn = {0302-9743},
categories = {holtestgen},
classification = {conference},
areas = {formal methods},
year = {2015},
public = {yes},
doi = {10.1007/978-3-319-29613-5_3},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-ipc-testing-2015}
}
@inproceedings{DBLP:conf/nfm/VerbeekHSTBL0WN15,
author = {Freek Verbeek and
Oto Havle and
Julien Schmaltz and
Sergey Tverdyshev and
Holger Blasum and
Bruno Langenstein and
Werner Stephan and
Burkhart Wolff and
Yakoub Nemouchi},
title = {Formal {API} Specification of the PikeOS Separation Kernel},
booktitle = {{NASA} Formal Methods - 7th International Symposium, {NFM} 2015, Pasadena,
CA, USA, April 27-29, 2015, Proceedings},
pages = {375--389},
year = {2015},
url = {http://dx.doi.org/10.1007/978-3-319-17524-9_26},
doi = {10.1007/978-3-319-17524-9_26},
timestamp = {Wed, 08 Apr 2015 14:02:16 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/VerbeekHSTBL0WN15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/models/LonguetTW14,
author = {Delphine Longuet and Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff},
title = {Towards a {T}ool for {F}eatherweight {OCL:} {A} {C}ase {S}tudy {O}n {S}emantic
{R}eflection},
booktitle = {Proceedings of the 14th International Workshop on {OCL} and Textual
Modelling co-located with 17th International Conference on Model Driven
Engineering Languages and Systems {(MODELS} 2014), Valencia, Spain,
September 30, 2014.},
pages = {43--52},
year = {2014},
url = {http://ceur-ws.org/Vol-1285/paper05.pdf},
timestamp = {Wed, 05 Nov 2014 15:39:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/models/LonguetTW14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/afp/BruckerBW14,
author = {Achim D. Brucker and
Lukas Br{\"{u}}gger and
Burkhart Wolff},
title = {The Unified Policy Framework {(UPF)}},
journal = {Archive of Formal Proofs},
volume = {2014},
year = {2014},
url = {https://www.isa-afp.org/entries/UPF.shtml},
timestamp = {Mon, 19 Sep 2016 15:58:56 +0200},
biburl = {http://dblp.org/rec/bib/journals/afp/BruckerBW14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/models/BruckerCDGGJTW14,
author = {Achim D. Brucker and
Tony Clark and
Carolina Dania and
Geri Georg and
Martin Gogolla and
Fr{\'{e}}d{\'{e}}ric Jouault and
Ernest Teniente and
Burkhart Wolff},
title = {Panel Discussion: Proposals for Improving {OCL}},
booktitle = {Proceedings of the 14th International Workshop on {OCL} and Textual
Modelling co-located with 17th International Conference on Model Driven
Engineering Languages and Systems {(MODELS} 2014), Valencia, Spain,
September 30, 2014.},
pages = {83--99},
year = {2014},
url = {http://ceur-ws.org/Vol-1285/paper09.pdf},
timestamp = {Wed, 05 Nov 2014 15:39:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/models/BruckerCDGGJTW14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{UPF-AFP,
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
title = {The {U}nified {P}olicy {F}ramework {(UPF)}},
journal = {Archive of Formal Proofs},
month = nov,
year = 2014,
note = {\url{http://afp.sf.net/entries/UPF.shtml},
Formal proof development},
issn = {2150-914x}
}
@article{CISC-Kernel-AFP,
author = {Freek Verbeek and Sergey Tverdyshev and Oto Havle and Holger Blasum and Bruno Langenstein and Werner Stephan and Yakoub Nemouchi and Abderrahmane Feliachi and Burkhart Wolff and Julien Schmaltz},
title = {Formal Specification of a Generic Separation Kernel},
journal = {Archive of Formal Proofs},
month = jul,
year = 2014,
note = {\url{http://afp.sf.net/entries/CISC-Kernel.shtml},
Formal proof development},
issn = {2150-914x}
}
@article{jron_et_al:DR:2013:4006,
author = {Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff},
title = {{Symbolic Methods in Testing (Dagstuhl Seminar 13021)}},
pages = {1--29},
journal = {Dagstuhl Reports},
issn = {2192-5283},
year = {2013},
volume = {3},
number = {1},
editor = {Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
url = {http://drops.dagstuhl.de/opus/volltexte/2013/4006},
urn = {urn:nbn:de:0030-drops-40060},
doi = {10.4230/DagRep.3.1.1},
area = {logical_representations},
annote = {Keywords: Automated Deduction, White-box testing,
Black-box Testing, Fuzz-Testing, Unit-Testing,
Theorem prover-based Testing}
}
@incollection{feliachi.ea:cirta:2013,
abstract = {Formal specifications provide strong bases for testing and
bring powerful techniques and technologies. Expressive formal
specification languages combine large data domain and behavior.
Thus, symbolic methods have raised particular interest for
test generation techniques. Integrating formal testing in
proof environments such as Isabelle/HOL is referred to as
“theorem-prover based testing”. Theorem-prover based testing
can be adapted to a specific specification language via a
representation of its formal semantics, paving the way for
specific support of its constructs. The main challenge of
this approach is to reduce the gap between pen-and-paper
semantics and formal mechanized theories.
In this paper we
consider testing based on the Circus specification language.
This language integrates the notions of states and of
complex data in a Z-like fashion with communicating
processes inspired from CSP. We present a machine-checked
formalization in Isabelle/HOL of this lan- guage and its
testing theory. Based on this formal representation of the
semantics we revisit the original associated testing theory.
We discovered unforeseen simplifications in both definitions
and symbolic computations. The approach lends itself to the
construction of a tool, that directly uses semantic definitions
of the language as well as derived rules of its testing theory,
and thus provides some powerful sym- bolic computation
machinery to seamlessly implement them both in a technical
environment. },
keywords = {symbolic test case generations, black box testing, theorem
proving, network security, firewall testing, conformance
testing},
location = {Wellington},
author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Makarius Wenzel and Burkhart Wolff},
booktitle = {Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods(ICFEM)},
language = {USenglish},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {8144},
title = {The Circus Testing Theory Revisited in Isabelle/HOL},
categories = {holtestgen},
classification = {conference},
areas = {formal testing, semantics, formal methods},
year = {2013},
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-Circus-testing.pdf}
}
@incollection{brucker.ea:hol-testgen-fw:2013,
abstract = { The HOL-TestGen environment is conceived as a system for
modeling and semi-automated test generation with an
emphasis on expressive power and generality. However, its
underlying technical framework Isabelle/HOL supports the
customization as well as the development of highly
automated add-ons working in specific application domains.
In this paper, we present HOL-TestGen/fw, an add-on for the
test framework HOL-TestGen, that allows for testing the
conformance of firewall implementations to high-level
security policies. Based on generic theories specifying a
security-policy language, we developed specific theories
for network data and firewall policies. On top of these
firewall specific theories, we provide mechanisms for
policy transformations based on derived rules and adapted
code-generators producing test drivers. Our empirical
evaluations shows that HOL-TestGen/fw is a competitive
environment for testing firewalls or high-level policies of
local networks. },
keywords = {symbolic test case generations, black box testing, theorem
proving, network security, firewall testing, conformance
testing},
location = {Shanghai},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
booktitle = {International Colloquium on Theoretical Aspects of Computing (ICTAC)},
language = {USenglish},
publisher = {Springer-Verlag},
address = {Heidelberg},
series = {Lecture Notes in Computer Science},
number = {8049},
title = {HOL-TestGen/FW: An Environment for Specification-based
Firewall Conformance Testing},
categories = {holtestgen},
classification = {conference},
areas = {security, formal methods},
year = {2013},
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-ictac-hol-testgen-fw.pdf}
}
@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13,
author = {Bruno Barras and
Lourdes Del Carmen Gonz{\'a}lez-Huesca and
Hugo Herbelin and
Yann R{\'e}gis-Gianas and
Enrico Tassi and
Makarius Wenzel and
Burkhart Wolff},
title = {Pervasive Parallelism in Highly-Trustable Interactive Theorem
Proving Systems},
booktitle = {MKM/Calculemus/DML},
year = {2013},
pages = {359-363},
doi = {10.1007/978-3-642-39320-4_29},
pdf = {http://www.lri.fr/~wolff/papers/conf/CICM13-PervasiveParallsm.pdf},
area = {logical_representations},
bibsource = {DBLP, http://dblp.uni-trier.de},
classification = {conference},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7961},
abstract = {Interactive theorem proving is a technology of fundamental
importance for mathematics and computer-science. It is based on expressive
logical foundations and implemented in a highly trustable way. Applications
include huge mathematical proofs and semi-automated verifications of complex
software systems. Interactive development of larger and larger proofs
increases the demand for computing power, which means explicit parallelism
on current multicore hardware.
The architecture of contemporary interactive
provers such as Coq, Isabelle or the HOL family goes back to the influential
LCF system from 1979, which has pioneered key principles like correctness
by construction for primitive inferences and definitions, free programmability
in userspace via ML, and toplevel command interaction. Both Coq and Isabelle
have elaborated the prover architecture over the years, driven by the demands
of sophisticated proof procedures, derived specification principles, large
libraries of formalized mathematics etc. Despite this success, the operational
model of interactive proof checking was limited by sequential ML evaluation
and the sequential read-eval-print loop, as inherited from LCF.}
}
@article{DBLP:journals/corr/BarrasGHRTWW13,
author = {Bruno Barras and
Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and
Hugo Herbelin and
Yann R{\'{e}}gis{-}Gianas and
Enrico Tassi and
Makarius Wenzel and
Burkhart Wolff},
title = {Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving
Systems},
journal = {CoRR},
volume = {abs/1305.7360},
year = {2013},
url = {http://arxiv.org/abs/1305.7360},
archiveprefix = {arXiv},
eprint = {1305.7360},
timestamp = {Wed, 07 Jun 2017 14:43:08 +0200},
biburl = {http://dblp.org/rec/bib/journals/corr/BarrasGHRTWW13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{Brucker:2013:TAP,
author = {Brucker, Achim D. and Feliachi, Abderrahmane and Nemouchi,
Yakoub and Wolff, Burkhart},
title = {Test Program Generation for a Microprocessor -- A Case-Study},
booktitle = {Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13)},
series = {Lecture Notes in Computer Science},
volume = {LNCS 7942},
year = {2013},
location = {Budapest, Hungaria},
pages = {76--95},
numpages = {20},
classification = {conference},
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-tap-tproc-testgen.pdf},
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-TapPresentation.pdf},
publisher = {Springer LNCS},
doi = {10.1007/978-3-642-38916-0_5},
area = {logical_representations},
domain = {os_test},
abstract = {Certifications of critical security or safety system properties are
becoming increasingly important for a wide range of products.
Certifying large systems like operating systems up to Common
Criteria EAL 4 is common practice today, and higher certification
levels are at the brink of becoming reality.
To reach EAL 7 one has
to formally verify properties on the specification as well as test
the implementation thoroughly. This includes tests of the used
hardware platform underlying a proof architecture to be certified.
In this paper, we address the latter problem: we present a case
study that uses a formal model of a microprocessor and generate
test programs from it. These test programs validate that a
microprocessor implements the specified instruction set correctly.
We built our case study on an existing model that was, together
with an operating system, developed in Isabelle/HOL. We use
HOL-TestGen, a model-based testing environment which is an
extension of Isabelle/HOL. We develop several conformance test
scenarios, where processor models were used to synthesize test
programs that were run against real hard- ware in the loop.
Our test case generation approach directly benefits from the
existing models and formal proofs in Isabelle/HOL.},
keywords = {test program generation, symbolic test case generations,
black box testing, white box testing, theorem proving,
interactive testing}
}
@inproceedings{Brucker:2012:FOS:2428516.2428520,
author = {Brucker, Achim D. and Wolff, Burkhart},
title = {Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL},
booktitle = {Proceedings of the 12th Workshop on OCL and Textual Modelling},
series = {OCL '12},
year = {2012},
isbn = {978-1-4503-1799-3},
location = {Innsbruck, Austria},
pages = {19--24},
numpages = {6},
url = {10.1145/2428516.2428520},
doi = {10.1145/2428516.2428520},
acmid = {2428520},
pdf = {http://www.lri.fr/~wolff/papers/workshop/featherweight-ocl.pdf},
publisher = {ACM},
address = {New York, NY, USA},
area = {logical_representations},
domain = {os_test},
classification = {conference},
keywords = {HOL-OCL, OCL, formal semantics}
}
@article{Feliachi-Wolff-Gaudel-AFP12,
author = {Abderrahmane Feliachi and Burkhart Wolff and Marie-Claude Gaudel},
title = {Isabelle/Circus},
journal = {Archive of Formal Proofs},
month = jun,
year = 2012,
note = {\url{http://afp.sourceforge.net/entries/Circus.shtml},
Formal proof development},
area = {logical_representations},
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). Isabelle/Circus is a formalization of
the UTP and the Circus language in Isabelle/HOL. It contains proof rules and
tactic support that allows for proofs of refinement for Circus processes
(involving both data and behavioral aspects).
The Isabelle/Circus environment supports a syntax for the semantic
definitions which is close to textbook presentations of Circus. This
article contains an extended version of corresponding VSTTE Paper together
with the complete formal development of its underlying commented theories.},
issn = {2150-914x}
}
@proceedings{DBLP:conf/utp/2008,
editor = {Burkhart Wolff and Marie-Claude Gaudel and Abderrahmane Feliachi},
title = {Unifying Theories of Programming, 4th International Symposium,
UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers},
booktitle = {UTP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {LNCS 7681},
year = 2013,
isbn = {978-3-642-35704-6}
}
@techreport{brucker.ea:hol-testgen:2012,
author = {Achim D. Brucker and Lukas Br{\"u}gger and Matthias P.
Krieger and Burkhart Wolff},
institution = {Laboratoire en Recherche en Infromatique (LRI),
Universit\'e Paris-Sud 11, France},
language = {USenglish},
month = apr,
title = {{HOL-TestGen} 1.7.0 User Guide},
categories = {testing,holtestgen},
classification = {unrefereed},
areas = {formal methods, software},
keywords = {symbolic test case generations, black box testing, theorem
proving, Isabelle/HOL},
year = {2012},
number = {1551},
area = {logical_representations},
num_pages = {120},
pdf = {http://www.brucker.ch/bibliography/download/2012/brucker.ea-hol-testgen-2012.pdf},
public = {yes},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2012}
}
@inproceedings{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 = {LNCS 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},
area = {logical_representations},
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},
area = {logical_representations},
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},
area = {logical_representations},
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},
area = {logical_representations},
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},
area = {logical_representations},
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.}
}
@inproceedings{DBLP:conf/models/BruckerLTW13,
author = {Achim D. Brucker and
Delphine Longuet and
Fr{\'e}d{\'e}ric Tuong and
Burkhart Wolff},
title = {On the {S}emantics of {O}bject-{O}riented {D}ata {S}tructures and
{P}ath {E}xpressions},
booktitle = {OCL@MoDELS},
year = {2013},
pages = {23-32},
ee = {http://ceur-ws.org/Vol-1092/brucker.pdf},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
volume = {1092}
}
@inproceedings{DBLP:conf/models/BruckerCCDGPRWW13,
author = {Achim D. Brucker and
Dan Chiorean and
Tony Clark and
Birgit Demuth and
Martin Gogolla and
Dimitri Plotnikov and
Bernhard Rumpe and
Edward D. Willink and
Burkhart Wolff},
title = {Report on the Aachen OCL Meeting},
booktitle = {OCL@MoDELS},
year = {2013},
pages = {103-111},
ee = {http://ceur-ws.org/Vol-1092/aachen.pdf},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
volume = {1092},
year = {2013}
}
@article{brucker.ea:2012,
author = {Achim D. Brucker and Burkhart Wolff},
title = {On {T}heorem {P}rover-based {T}esting},
journal = {Formal Asp. Comput. (FAOC)},
year = {2013},
month = sept,
volume = {25},
number = {5},
pages = {683--721},
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},
area = {logical_representations},
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},
area = {logical_representations},
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},
area = {logical_representations},
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}
}
@article{DBLP:journals/fac/BruckerW13,
author = {Achim D. Brucker and
Burkhart Wolff},
title = {On theorem prover-based testing},
journal = {Formal Asp. Comput.},
volume = {25},
number = {5},
pages = {683--721},
year = {2013},
url = {https://doi.org/10.1007/s00165-012-0222-y},
doi = {10.1007/s00165-012-0222-y},
timestamp = {Tue, 06 Jun 2017 22:21:37 +0200},
biburl = {http://dblp.org/rec/bib/journals/fac/BruckerW13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@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 provers such 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 = {https://www.lri.fr/~wolff/papers/journals/brucker.ea-extensible-2008-b},
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://www.lri.fr/~wolff/papers/conf/2007-tphols-isar-tool-framework.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
}
@techreport{brucker.ea:path-expressions:2013-b,
author = {Achim D. Brucker and Delphine Longuet and Fr{\'e}d{\'e}ric
Tuong and Burkhart Wolff},
title = {On the Semantics of Object-oriented Data Structures and
Path Expressions (Extended Version)},
booktitle = {Workshop on OCL and Textual Modelling (OCL 2013)},
year = {2013},
abstract = { \UML/\OCL is perceived as the de-facto standard for
specifying object-oriented models in general and data
models in particular. Since recently, all data types of
\UML/\OCL comprise two different exception elements:
\inlineocl{invalid} (``bottom'' in semantics terminology)
and \inlineocl{null} (for ``non-existing element''). This
has far-reaching consequences on both the logical and
algebraic properties of \OCL expressions as well as the
path expressions over object-oriented data structures, \ie,
class models.
In this paper, we present a formal semantics for
object-oriented data models in which all data types and,
thus, all class attributes and path expressions, support
\inlineocl{invalid} and \inlineocl{null}. Based on this
formal semantics, we present a set of \OCL test cases that
can be used for evaluating the support of \inlineocl{null}
and \inlineocl{invalid} in \OCL tools.},
classification = {unrefereed},
categories = {holocl},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-path-expressions-2013-b},
number = {1565},
institution = {Laboratoire en Recherche en Informatique (LRI),
Universit\'e Paris-Sud 11, France},
areas = {formal methods, software},
keywords = { Object-oriented Data Structures, Path Expressions,
Featherweight OCL, Null, Invalid, Formal Semantics},
public = {yes},
pdf = {http://www.brucker.ch/bibliography/download/2013/brucker.ea-path-expressions-2013-b.pdf}
}
@article{brucker.ea:featherweight:2014,
author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart
Wolff},
title = {Featherweight OCL: A Proposal for a Machine-Checked Formal
Semantics for OCL 2.5},
journal = {Archive of Formal Proofs},
month = jan,
year = {2014},
note = {\url{http://afp.sf.net/entries/Featherweight_OCL.shtml},
Formal proof development},
issn = {2150-914x},
abstract = {The Unified Modeling Language (UML) is one of the few
modeling languages that is widely used in industry. While
UML is mostly known as diagrammatic modeling language
(e.g., visualizing class models), it is complemented by a
textual language, called Object Constraint Language (OCL).
OCL is based on a three-valued logic that turns UML into a
formal language. Unfortunately the semantics of this
specification language, captured in the "Annex A" of the
OCL standard, leads to different interpretations of corner
cases. We formalize the core of OCL: denotational
definitions, a logical calculus and operational rules that
allow for the execution of OCL expressions by a mixture of
term rewriting and code compilation. Our formalization
reveals several inconsistencies and contradictions in the
current version of the OCL standard. Overall, this document
is intended to provide the basis for a machine-checked text
"Annex A" of the OCL standard targeting at tool
implementors.},
public = {yes},
classification = {formal},
categories = {holocl},
pdf = {http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},
filelabel = {Outline},
file = {http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},
areas = {formal methods, software},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014}
}
@inproceedings{nguyenvan_et_al:LIPIcs:2020:12983,
author = {Hai Nguyen Van and Fr{\'e}d{\'e}ric Boulanger and Burkhart Wolff},
title = {{TESL: A Model with Metric Time for Modeling and Simulation}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
isbn = {978-3-95977-167-2},
issn = {1868-8969},
year = {2020},
volume = {178},
editor = {Emilio Mu{\~n}oz-Velasco and Ana Ozaki and Martin Theobald},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12983},
urn = {urn:nbn:de:0030-drops-129837},
doi = {10.4230/LIPIcs.TIME.2020.15},
annote = {Keywords: Timed Systems, Semantics, Models, Simulation}
}
@inproceedings{DBLP:conf/formats/VanBBKVW20,
author = {Hai Nguyen Van and
Thibaut Balabonski and
Fr{\'{e}}d{\'{e}}ric Boulanger and
Chantal Keller and
Beno{\^{\i}}t Valiron and
Burkhart Wolff},
title = {On the Semantics of Polychronous Polytimed Specifications},
booktitle = {Formal Modeling and Analysis of Timed Systems - 18th International
Conference, {FORMATS} 2020, Vienna, Austria, September 1-3, 2020,
Proceedings},
pages = {23--40},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-57628-8\_2},
doi = {10.1007/978-3-030-57628-8\_2},
pdf = {https://www.lri.fr/~wolff/papers/conf/2020-Formats-SPPS.pdf},
timestamp = {Tue, 25 Aug 2020 15:34:38 +0200},
biburl = {https://dblp.org/rec/conf/formats/VanBBKVW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
This file was generated by bibtex2html 1.96.