[1] 
Achim D. Brucker, Idir AitSadoune, Paolo Crisafulli, and Burkhart Wolff.
Using the isabelle ontology framework: Linking the formal with the
informal.
In Conference on Intelligent Computer Mathematics (CICM),
number 11006 in Lecture Notes in Computer Science. SpringerVerlag,
Heidelberg, 2018.
[ bib 
DOI 
http 
.pdf ]
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. Keywords: Isabelle/Isar, HOL, Ontologies 
[2] 
S. Bezzecchi, P. Crisafulli, C. Pichot, and B. Wolff.
Making agile development processes fit for vstyle certification
procedures.
In ERTS'18, ERTS Conference Proceedings, 2018.
[ bib 
.pdf ]
We present a process for the development of safety and security critical components in transportation systems targeting a highlevel 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 casestudy that comprises a model of an odometric service in a railwaysystem 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 semiformal and formal definitions within to specific certification processes in order to improve their costeffectiveness.

[3]  Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Formal network models and their application to firewall policies. Archive of Formal Proofs, 2017, 2017. [ bib  http ] 
[4]  Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, and Burkhart Wolff. A symbolic operational semantics for TESL  with an application to heterogeneous system testing. In Formal Modeling and Analysis of Timed Systems  15th International Conference, FORMATS 2017, Berlin, Germany, September 57, 2017, Proceedings, pages 318334, 2017. [ bib  DOI  http  .pdf ] 
[5] 
Achim D. Brucker, Lukas Brügger, Abderrahmane Feliachi, Chantal Keller,
Matthias P. Krieger, Delphine Longuet, Yakoub Nemouchi, Frédéric
Tuong, and Burkhart Wolff.
HOLTestGen 1.8.0 user guide.
Technical Report 1586, Laboratoire en Recherche en Informatique
(LRI), Université ParisSud 11, France, April 2016.
[ bib 
http 
.pdf ]
Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL 
[6] 
R. Aissat, F. Voisin, and B. Wolff.
Infeasible paths elimination by symbolic execution techniques: Proof
of correctness and preservation of paths.
In ITP'16, volume 9762 of Lecture Notes in Computer
Science, 2016.
[ bib 
.pdf ]
TRACER is a tool for verifying safety properties of sequential C programs. TRACER attempts at building a finite symbolic execution graph which overapproximates the set of all concrete reachable states and the set of feasible paths. We present an abstract framework for TRACER and similar CEGARlike systems. The framework provides 1) a graphtransformation based method for reducing the feasible paths in controlflow 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.

[7] 
Achim D. Brucker and Burkhart Wolff.
Monadic sequence testing and explicit testrefinements.
In Tests and Proofs  10th International Conference, TAP 2016,
Held as Part of STAF 2016, Vienna, Austria, July 57, 2016, Proceedings,
volume LNCS 7942 of Lecture Notes in Computer Science, pages 1736,
2016.
[ bib 
DOI 
http 
.pdf ]
Abstract We present an abstract framework for sequence testing that is implemented in Isabelle/HOLTestGen. Our framework is based on the theory of stateexception 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 casestudies involving system models based on large (or infinite) state. On this basis, we rephrase the concept of testrefinements for inclusion, deadlock and IOCOlike tests, together with a formal theory of its rela tion to traditional, IOautomata based notions.

[8]  Achim D. Brucker, Jordi Cabot, Gwendal Daniel, Martin Gogolla, Adolfo SánchezBarbudo Herrera, Frank Hilken, Frédéric Tuong, Edward D. Willink, and Burkhart Wolff. Recent developments in OCL and textual modelling. In Proceedings of the 16th International Workshop on OCL and Textual Modelling colocated with 19th International Conference on Model Driven Engineering Languages and Systems (MODELS 2016), SaintMalo, France, October 2, 2016., pages 157165, 2016. [ bib  .pdf ] 
[9]  Romain Aïssat, Frédéric Voisin, and Burkhart Wolff. Infeasible paths elimination by symbolic execution techniques: Proof of correctness and preservation of paths. Archive of Formal Proofs, 2016, 2016. [ bib  http ] 
[10]  R. Aissat, M.C. Gaudel, F. Voisin, and B. Wolff. Pruning infeasible paths via graph transformations and symbolic execution: a method and a tool. Technical Report 1588, L.R.I., Univ. ParisSud, 2016. [ bib  http ] 
[11]  Romain Aïssat, MarieClaude Gaudel, Frédéric Voisin, and Burkhart Wolff. A method for pruning infeasible paths via graph transformations and symbolic execution. In 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016, Vienna, Austria, August 13, 2016, pages 144151, 2016. [ bib  DOI  http ] 
[12] 
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff.
Featherweight OCL: A Proposal for a MachineChecked
Formal Semantics for OCL 2.5.
Technical Report 1582, LRI, Univ Paris Sud, CNRS, Centrale Supélec,
Université ParisSaclay, France, September 2015.
[ bib 
http 
.pdf ]
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 threevalued 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 threevalued 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 codingscheme for UML class models that were annotated by codeinvariants and code contracts. An implementation of this codingscheme 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 machinechecked text “Annex A” of the OCL standard targeting at tool implementors.

[13]  Frédéric Tuong and Burkhart Wolff. A MetaModel for the Isabelle API. Archive of Formal Proofs, 2015. [ bib  http ] 
[14]  Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, and Cyril Proch. Used Formal Methods, chapter Using Isabelle/HOL in Certification Processes: A System Description and Mandatory Recommendations. The EUROMILS Project, 2015. available from the Project site: http://www.euromils.eu/downloads/Deliverables/Y2/2015EMUsedFormalMethodsWhitePaperOctober2015.pdf. [ bib  DOI ] 
[15] 
Abderrahmane Feliachi, MarieClaude Gaudel, and Burkhart Wolff.
Symbolic testgeneration in HOLTestGen/Cirta: A case study.
Int. J. Software Informatics, 9(2):177203, 2015.
[ bib 
.pdf ]
HOLTestGen/CirTA is a theoremprover based test generation environment for specifications written in Circus, a processalgebraic specification language in the tradition of CSP. HOLTestGen/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 HOLTestGen/ CirTA consists in an entire derived theory for the generation of symbolic testtraces, including optimized rules for testgeneration as well as rules for symbolic execution. The deduction process is automated by Isabelle tactics, allowing to protract the statespace explosion resulting from blind enumeration of data. The implementation of testgeneration 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 testdrivers. This paper describes the novel toolchain based on prior theoretical work on semantics and testtheory and attempts an evaluation via a mediumsized case study performed on a component of a realworld safetycritical medical monitoring system written in Java. We provide experimental measurements of the killcapacity of implementation mutants.

[16] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.
Formal firewall conformance testing: An application of test and proof
techniques.
Softw. Test., Verif. Reliab., 25(1):3471, 2015.
[ bib 
DOI 
.pdf ]
Firewalls are an important means to secure critical ICT infrastructures. As configurable offtheshelf 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 specificationbased 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 semanticspreserving 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.

[17]  Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Safouan Taha, Benoît Valiron, Burkhart Wolff, and Lina Ye. Towards a formal semantics of the TESL specification language. In Joint Proceedings of the 3rd International Workshop on the Globalization Of Modeling Languages and the 9th International Workshop on MultiParadigm Modeling colocated with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, GEMOC+MPM@MoDELS 2015, Ottawa, Canada, September 28, 2015., pages 1419, 2015. [ bib  .pdf ] 
[18] 
Achim D. Brucker, Oto Havle, Yakoub Nemouchi, and Burkhart Wolff.
Testing the ipc protocol for a realtime operating system.
In Arie Gurfinkel and Sanjit A. Seshia, editors, Working
Conference on Verified Software: Theories, Tools, and Experiments, number
9593 in Lecture Notes in Computer Science. SpringerVerlag, Heidelberg, 2015.
[ bib 
DOI 
http 
.pdf ]
In this paper, we adapt modelbased testing techniques to concurrent code, namely for test generations of an (industrial) OS kernel called PikeOS. Since our datamodels are complex, the problem is out of reach of conventional modelchecking 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 HOLTestGen. 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 interprocess communication systemcalls. Inheriting a microarchitecture going back to the L4 kernel, the system calls of the IPCAPI are internally structured by atomic actions; according to a security model, these actions can fail and must produce errorcodes. 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 
[19]  Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan, Burkhart Wolff, and Yakoub Nemouchi. Formal API specification of the pikeos separation kernel. In NASA Formal Methods  7th International Symposium, NFM 2015, Pasadena, CA, USA, April 2729, 2015, Proceedings, pages 375389, 2015. [ bib  DOI  http ] 
[20]  Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. The Unified Policy Framework (UPF). Archive of Formal Proofs, November 2014. http://afp.sf.net/entries/UPF.shtml, Formal proof development. [ bib ] 
[21]  Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, and Julien Schmaltz. Formal specification of a generic separation kernel. Archive of Formal Proofs, July 2014. http://afp.sf.net/entries/CISCKernel.shtml, Formal proof development. [ bib ] 
[22]  Delphine Longuet, Frédéric Tuong, and Burkhart Wolff. Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection. In Proceedings of the 14th International Workshop on OCL and Textual Modelling colocated with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., pages 4352, 2014. [ bib  .pdf ] 
[23]  Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. The unified policy framework (UPF). Archive of Formal Proofs, 2014, 2014. [ bib  http ] 
[24]  Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, and Burkhart Wolff. Panel discussion: Proposals for improving OCL. In Proceedings of the 14th International Workshop on OCL and Textual Modelling colocated with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., pages 8399, 2014. [ bib  .pdf ] 
[25] 
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff.
Featherweight ocl: A proposal for a machinechecked formal semantics
for ocl 2.5.
Archive of Formal Proofs, January 2014.
http://afp.sf.net/entries/Featherweight_OCL.shtml, Formal proof
development.
[ bib 
http 
.pdf ]
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 threevalued 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 machinechecked text "Annex A" of the OCL standard targeting at tool implementors.

[26]  Thierry Jéron, Margus Veanes, and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). Dagstuhl Reports, 3(1):129, 2013. [ bib  DOI  http ] 
[27] 
Abderrahmane Feliachi, MarieClaude Gaudel, Makarius Wenzel, and Burkhart
Wolff.
The circus testing theory revisited in isabelle/hol.
In Formal Methods and Software Engineering  15th International
Conference on Formal Engineering Methods(ICFEM), number 8144 in Lecture
Notes in Computer Science. SpringerVerlag, Heidelberg, 2013.
[ bib 
.pdf ]
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 “theoremprover based testing”. Theoremprover 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 penandpaper 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 Zlike fashion with communicating processes inspired from CSP. We present a machinechecked 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 
[28] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.
Holtestgen/fw: An environment for specificationbased firewall
conformance testing.
In International Colloquium on Theoretical Aspects of Computing
(ICTAC), number 8049 in Lecture Notes in Computer Science. SpringerVerlag,
Heidelberg, 2013.
[ bib 
.pdf ]
The HOLTestGen environment is conceived as a system for modeling and semiautomated 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 addons working in specific application domains. In this paper, we present HOLTestGen/fw, an addon for the test framework HOLTestGen, that allows for testing the conformance of firewall implementations to highlevel security policies. Based on generic theories specifying a securitypolicy 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 codegenerators producing test drivers. Our empirical evaluations shows that HOLTestGen/fw is a competitive environment for testing firewalls or highlevel policies of local networks. Keywords: symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing 
[29] 
Bruno Barras, Lourdes Del Carmen GonzálezHuesca, Hugo Herbelin, Yann
RégisGianas, Enrico Tassi, Makarius Wenzel, and Burkhart Wolff.
Pervasive parallelism in highlytrustable interactive theorem proving
systems.
In MKM/Calculemus/DML, volume 7961 of Lecture Notes in
Computer Science, pages 359363. Springer, 2013.
[ bib 
DOI 
.pdf ]
Interactive theorem proving is a technology of fundamental importance for mathematics and computerscience. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semiautomated 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 readevalprint loop, as inherited from LCF.

[30]  Bruno Barras, Lourdes Del Carmen GonzálezHuesca, Hugo Herbelin, Yann RégisGianas, Enrico Tassi, Makarius Wenzel, and Burkhart Wolff. Pervasive parallelism in highlytrustable interactive theorem proving systems. CoRR, abs/1305.7360, 2013. [ bib  arXiv  http ] 
[31] 
Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff.
Test program generation for a microprocessor  a casestudy.
In Proceedings of the 6th Intl. Conf. on Test and Proof (TAP
'13), volume LNCS 7942 of Lecture Notes in Computer Science, pages
7695. Springer LNCS, 2013.
[ bib 
DOI 
.pdf ]
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 HOLTestGen, a modelbased 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 
[32]  Burkhart Wolff, MarieClaude Gaudel, and Abderrahmane Feliachi, editors. Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 2728, 2012, Revised Selected Papers, volume LNCS 7681 of Lecture Notes in Computer Science. Springer, 2013. [ bib ] 
[33]  Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff. On the Semantics of ObjectOriented Data Structures and Path Expressions. In OCL@MoDELS, volume 1092 of CEUR Workshop Proceedings, pages 2332. CEURWS.org, 2013. [ bib ] 
[34]  Achim D. Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D. Willink, and Burkhart Wolff. Report on the aachen ocl meeting. In OCL@MoDELS, volume 1092 of CEUR Workshop Proceedings, pages 103111. CEURWS.org, 2013. [ bib ] 
[35] 
Achim D. Brucker and Burkhart Wolff.
On Theorem Proverbased Testing.
Formal Asp. Comput. (FAOC), 25(5):683721, 2013.
[ bib 
DOI 
.pdf ]
HOLTestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOLTestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOLTestGen method is twostaged: 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 testhypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for blackbox unit, sequence, reactive sequence and whitebox test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial casestudies. Keywords: Isabelle/HOL, Theorem proving, Modelbased Testing, Programbased Testing, Testcase Generation 
[36]  Achim D. Brucker and Burkhart Wolff. On theorem proverbased testing. Formal Asp. Comput., 25(5):683721, 2013. [ bib  DOI  http ] 
[37] 
Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff.
On the semantics of objectoriented data structures and path
expressions (extended version).
Technical Report 1565, Laboratoire en Recherche en Informatique
(LRI), Université ParisSud 11, France, 2013.
[ bib 
http 
.pdf ]
/is perceived as the defacto standard for specifying objectoriented models in general and data models in particular. Since recently, all data types of /comprise two different exception elements: invalid (“bottom” in semantics terminology) and null (for “nonexisting element”). This has farreaching consequences on both the logical and algebraic properties of expressions as well as the path expressions over objectoriented data structures, , class models. In this paper, we present a formal semantics for objectoriented data models in which all data types and, thus, all class attributes and path expressions, support invalid and null. Based on this formal semantics, we present a set of test cases that can be used for evaluating the support of null and invalid in tools. Keywords: Objectoriented Data Structures, Path Expressions, Featherweight OCL, Null, Invalid, Formal Semantics 
[38] 
Abderrahmane Feliachi, Burkhart Wolff, and MarieClaude Gaudel.
Isabelle/circus.
Archive of Formal Proofs, June 2012.
http://afp.sourceforge.net/entries/Circus.shtml, Formal proof
development.
[ bib ]
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.

[39] 
Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff.
HOLTestGen 1.7.0 user guide.
Technical Report 1551, Laboratoire en Recherche en Infromatique
(LRI), Université ParisSud 11, France, April 2012.
[ bib 
http 
.pdf ]
Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL 
[40] 
Achim D. Brucker and Burkhart Wolff.
Featherweight ocl: a study for the consistent semantics of ocl 2.3 in
hol.
In Proceedings of the 12th Workshop on OCL and Textual
Modelling, OCL '12, pages 1924, New York, NY, USA, 2012. ACM.
[ bib 
DOI 
www: 
.pdf ]
Keywords: HOLOCL, OCL, formal semantics 
[41] 
Abderrahmane Feliachi, MarieClaude Gaudel, and Burkhart Wolff.
Isabelle/Circus: A process specification and verification
environment.
In VSTTE, volume LNCS 7152 of Lecture Notes in Computer
Science, pages 243260, 2012.
[ bib 
DOI 
.pdf ]
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 machinechecked, 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.

[42]  Abderrahmane Feliachi. Representing Circus Operational Semantics in Isabelle/HOL. Technical Report 1544, LRI, http://www.lri.fr/Rapportsinternes, Université ParisSud XI, August 2011. [ bib  .pdf ] 
[43]  Jordi Cabot, Robert Clarisó, Martin Gogolla, and Burkhart Wolff. Preface (ocl 2011 proceedings). ECEASST, 44, 2011. [ bib ] 
[44]  Burkhart Wolff and Fatiha Zaïdi, editors. Testing Software and Systems  23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 710, 2011. Proceedings, volume 7019 of Lecture Notes in Computer Science. Springer, 2011. [ bib  DOI ] 
[45]  Martin Gogolla and Burkhart Wolff, editors. Tests and Proofs  5th International Conference, TAP 2011, Zurich, Switzerland, June 30  July 1, 2011. Proceedings, volume 6706 of Lecture Notes in Computer Science. Springer, 2011. [ bib  DOI  .pdf ] 
[46] 
Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff.
An approach to modular and testable security models of realworld
healthcare applications.
Proceedings of the ACM Symposium on Access control models and
technologies, pages 133142. ACM, 2011.
SACMAT 2011.
[ bib 
DOI 
.pdf ]
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 largescale 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 modelbased testing techniques of a large system exhibiting critical security features. We model the four information governance principles, comprising a rolebased 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 Higherorder Logic (HOL) and processed together with suitable test specifications in the HOLTestGen 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 modelbased testing.

[47]  Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff. HOLTestGen 1.5.0 user guide. Technical Report 670, ETH Zurich, April 2010. [ bib  .pdf ] 
[48] 
Abderrahmane Feliachi, MarieClaude Gaudel, and Burkhart Wolff.
Unifying Theories in Isabelle/HOL.
In Unifying Theories of Programming (UTP2010), number 6445 in
Lecture Notes in Computer Science. SpringerVerlag, Heidelberg, 2010.
[ bib 
DOI 
.pdf ]
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. Keywords: UTP, Theorem Proving, Symbolic test case generations, Isabelle/HOL 
[49] 
Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and Burkhart Wolff.
A Specificationbased Test Case Generation Method for
UML/OCL.
In Proceedings of the Workshop on OCL and Textual Modelling (OCL
2010), 2010.
LNCS 6627.
[ bib 
DOI 
.pdf ]
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 DNFbased 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 objectid's; thus, our approach avoids the generation of isomorphic object graphs by using a concise and still humanreadable symbolic representation.

[50] 
Matthias P. Krieger, Alexander Knapp, and Burkhart Wolff.
Automatic and Efficient Simulation of Operation Contracts.
In Eelco Visser, Jaakko Jarvi, and Giorgios Economopoulos, editors,
Ninth International Conference on Generative Programming and Component
Engineering (GPCE'10). IEEE Computer Society, 2010.
[ bib 
DOI 
.pdf ]
Operation contracts consisting of pre and postconditions are a wellknown 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.

[51] 
Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff.
Verified Firewall Policy Transformations for Test Case
Generation.
Software Testing, Verification, and Validation, 2010
International Conference on, 0:345354, 2010.
[ bib 
DOI 
.pdf ]
We present an optimization technique for modelbased generation of test cases for firewalls. Based on a formal model for firewall policies in higherorder logic, we derive a collection of semanticspreserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/hol. Finally, we use the normalized policies to generate test cases with the domainspecific firewall testing tool . 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 statespace explosions in test case generation for security policies.

[52]  Burkhart Wolff. Topdown vs. Bottomup: Formale Methoden im wissenschaftlichen Wettbewerb. Ein essayistischer Survey über den Stand der Kunst. Technical report, DFKI Technischer Bericht, 2009. Erschienen in der Festschrift zum 60. Geburtstag von Bernd KriegBrückner. [ bib  .pdf ] 
[53] 
Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff.
HOLBoogie  An Interactive ProverBackend for the
Verified C Compiler.
Journal of Automated Resoning (JAR), 44(12):111144, 2009.
[ bib 
DOI 
.pdf ]
Boogie is a verification condition generator for an imperative core language. It has frontends for the programming languages C# and C enriched by annotations in firstorder logic, ie pre and postconditions, assertions, and loop invariants. Moreover, concepts like ghost fields, ghost variables, ghost code and specification functions have been introduced to support a specific modeling methodology. Boogie's verification conditions  constructed via a wp calculus from annotated programs  are usually transferred to automated theorem provers such as Simplify or Z3. This also comprises the expansion of languagespecific modeling constructs in terms of a theory describing memory and elementary operations on it; this theory is called machine/memory model. In this paper, we present a proof environment, HOLBoogie, that combines Boogie with the interactive theorem prover Isabelle/, for a specific C frontend 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. Keywords: Isabelle/HOL, Theorem proving, Program verification, Memory models, Annotation languages 
[54] 
Achim D. Brucker and Burkhart Wolff.
Semantics, Calculi, and Analysis for ObjectOriented
Specifications.
Acta Informatica, 46(4):255284, 2009.
[ bib 
DOI 
.pdf ]
We present a formal semantics for an objectoriented 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 refinementbased objectoriented development. Keywords: UML , OCL , objectoriented specification , refinement , formal methods 
[55] 
Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff.
Proving Fairness and Implementation Correctness of a
Microkernel Scheduler.
Journal of Automated Reasoning (JAR), 42(24):349388, 2009.
G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System
Verification (2008).
[ bib 
DOI 
.pdf ]
We report on the formal proof of a microkernel's key property, namely the fairness property of its multipriority process scheduler. The proof architecture links a layer of behavioral reasoning over systemtrace sets with a concrete, fairly realistic implementation written in C. Our microkernel provides an infrastructure 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 interprocess communication (IPC) via synchronous message passing. The kernel establishes process switches according to IPCs and timerevents; 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, machinedependent 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. Keywords: Microkernel, Formal verification, Interactive theorem proving, Isabelle/HOL 
[56] 
Achim D. Brucker and Burkhart Wolff.
HOLTestGen: An Interactive Testcase Generation
Framework.
In Marsha Chechik and Martin Wirsing, editors, Fundamental
Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes
in Computer Science, pages 417420. SpringerVerlag, Heidelberg, 2009.
[ bib 
DOI 
http 
.ps.gz 
.pdf ]
We present HOLTestGen, an extensible test environment for specificationbased testing build upon the proof assistant Isabelle. HOLTestGen leverages the semiautomated 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. HOLTestGen 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 
[57] 
Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff.
Extending OCL with nullreferences.
In S. Ghosh, editor, MODELS 2009 Workshops, LNCS 6002, pages
261275. Springer Verlag, Heidelberg, 2009.
BestPaper Award at the OCL 2009 Workshop.
[ bib 
DOI 
http 
.ps.gz 
.pdf ]
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 threevalued propositional logic. Recent versions of the OCL standard added a second exception element, which, similar to the null references in objectoriented programming languages, is given a nonstrict semantics. Unfortunately, this extension has been done in an ad hoc manner, which results in several inconsistencies and contradictions. Keywords: , UML, OCL, null reference, formal semantics 
[58] 
Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, and Burkhart Wolff.
A verification approach for systemlevel concurrent programs.
In Verified Software: Theories, Tools, Experiments, LNCS 5295,
pages 161176. Springer Berlin / Heidelberg, September 2008.
[ bib 
DOI 
.pdf ]
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 HoareLogic. 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.

[59] 
Achim D. Brucker and Burkhart Wolff.
Extensible universes for objectoriented data models.
In Jan Vitek, editor, Proceedings of the European Conference of
ObjectOriented Programming (ECOOP 2008), LNCS 5142, pages 438462.
SpringerVerlag, Paphos, Cyprus, July 2008.
[ bib 
DOI 
http 
.pdf ]
We present a datatype package that enables the shallow embedding technique to objectoriented specification and programming languages. This datatype package incrementally compiles an objectoriented data model to a theory containing objectuniverses, 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 objectoriented corelanguage called imp++, for which correctness of a HoareLogic with respect to an operational semantics is proven.

[60] 
Sascha Böhme, Rustan Leino, and Burkhart Wolff.
HOLBoogie  An Interactive Prover for the Boogie
Program Verifier.
In Sofiene Tahar, Otmane Ait Mohamed, and César Muñoz,
editors, 21th International Conference on Theorem proving in
HigherOrder Logics (TPHOLs 2008), LNCS 5170. SpringerVerlag, Montreal,
Canada, 2008.
[ bib 
DOI 
.pdf ]
Boogie is a program verification condition generator for animperative core language. It has frontends for the programming languagesC# and C enriched by annotations in firstorder 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 proofenvironment,HOLBoogie, that combines Boogie with the interactivetheorem prover Isabelle/HOL. In particular, we present specific techniquescombining automated and interactive proof methods for codeverification.We will exploit our proofenvironment in two ways: First, we present scenariosto debugännotations (in particular: invariants) by interactiveproofs. Second, we use our environment also to verify background theories,i.e. theories for datatypes used in annotations as well as memoryand machine models underlying the verification method for C.

[61] 
Achim D. Brucker and Burkhart Wolff.
An Extensible Encoding of Objectoriented Data Models in
HOL with an Application to IMP++.
Journal of Automated Reasoning (JAR), Selected Papers of the
AVOCSVERIFY Workshop 2006(34):219249, 2008.
Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds).
[ bib 
DOI 
http ]
We present an extensible encoding of objectoriented data models into higherorder logic (HOL). Our encoding is supported by a datatype package that leverages the use of the shallow embedding technique to objectoriented specification and programming languages. The package incrementally compiles an objectoriented data model, i.e., a class model, to a theory containing objectuniverses, constructors, accessor functions, coercions (casts) between dynamic and static types, characteristic sets, and coinductive 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 objectoriented corelanguage called IMP++, for which we formally prove the correctness of a Hoare logic with respect to a denotational semantics.

[62] 
Achim D. Brucker and Burkhart Wolff.
A Formal Proof Environment for UML/OCL.
In Proceedings of Formal Aspects of Software Engineering (FASE
2008), volume 4961 of Lecture Notes in Computer Science, pages
97101. Springer Berlin / Heidelberg, 2008.
[ bib 
DOI 
.pdf ]
We present the theorem proving environment HOLOCL that is integrated in a MDE framework. HOLOCL allows to reason over UML class models annotated with OCL specifications. Thus, HOLOCL strengthens a crucial part of the UML to an objectoriented formal method. 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 sideconditions from modeltransformations.

[63] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.
Modelbased firewall conformance testing.
In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES
2008, LNCS 5047, pages 103118. SpringerVerlag, Tokyo, Japan, 2008.
[ bib 
DOI 
http 
.pdf ]
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 modelbased testing tool HOLTestGen. 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 domainspecific firewall testing tool HOLTestGen/FW.

[64] 
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.
Verifying testhypotheses  an experiment in test and proof.
In Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko,
editors, Modelbased Testing (MBT) 2008, volume 202 of Electronic
Notes in Theoretical Computer Science, pages 1528, Budapest, Hungary,
2008. Elsevier Science Publishers.
[ bib 
DOI 
.pdf ]
HOLTestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. The HOLTestGen method is twostaged: 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 HOLTestGen 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.

[65] 
David Basin, Hironobu Kuruma, Shin Nakajima, and Burkhart Wolff.
The Z Specification Language and the Proof Environment
Isabelle/HOLZ.
Computer Software  Journal of the Japanese Society for
Software Science and Technology, 24(2):2126, April 2007.
In Japanese.
[ bib 
http ]
Z is a standardized and wellestablished 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 higherorder logic (HOL). On this basis, a theoremproving environment such as Isabelle/HOLZ can be built. In this paper, we show how properties over specifications can be formally proven in HOLZ. Particular emphasis is put on proving relationships between specification such as refinement.

[66] 
David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, and Burkhart
Wolff.
Verifying a signature architecture: a comparative case study.
Formal Aspects of Computing, 19(1):6391, March 2007.
http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0.
[ bib 
DOI 
.pdf ]
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 formalmethods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both dataoriented and processoriented 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 finitestate 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 timeconsuming nor more complex than model checking.

[67] 
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
An MDA framework supporting OCL.
Electronic Communications of the EASST, 5, 2007.
[ bib 
http 
.pdf ]
We present a modeldriven 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 runtimetest environments) and formal analysis using the theorem proving environment HOLOCL. 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.

[68] 
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
Semantic issues of OCL: Past, present, and future.
Electronic Communications of the EASST, 5, 2007.
[ bib 
http 
.pdf ]
We report on the results of a longterm project to formalize the semantics of OCL 2.0 in Higherorder Logic (HOL). The ultimate goal of the project is to provide a formalized, machinechecked semantic basis for a theorem proving environment for OCL (as an example for an objectoriented 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.

[69] 
Achim D. Brucker and Burkhart Wolff.
Testsequence generation with holtestgen  with an application to
firewall testing.
In Bertrand Meyer and Yuri Gurevich, editors, TAP 2007: Tests
And Proofs, number 4454 in Lecture Notes in Computer Science, pages
149168. SpringerVerlag, Zurich, 2007.
[ bib 
DOI 
http 
.ps.gz 
.pdf ]
HOLTestGen is a specification and testcase generation environment extending the interactive theorem prover Isabelle/HOL. Its method is twostaged: 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 blackbox unittests, HOLTestGen's underlying logic and deduction engine is powerful enough to be used in testsequence generation, too. We develop the theory for testsequence generation with HOLTestGen and describe its use in a substantial casestudy in the field of computer security, namely the blackbox test of configured firewalls. Keywords: security, modelbased testing, specificationbased testing, firewall testing 
[70] 
Makarius Wenzel and Burkhart Wolff.
Building formal method tools in the isabelle/isar framework.
In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, LNCS
4732, pages 351366. SpringerVerlag, 2007.
[ bib 
DOI 
.pdf ]
We present the generic system framework of Isabelle/Isarunderlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plugins, 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 HOLZ 3.0 environment, which is geared towards the analysis of Z specifications and formal proof of forwardrefinements.

[71] 
Achim D. Brucker and Burkhart Wolff.
A package for extensible objectoriented data models with an
application to imp++.
In Abhik Roychoudhury and Zijiang Yang, editors, International
Workshop on Software Verification and Validation (SVV 2006), Computing
Research Repository (CoRR). Seattle, USA, August 2006.
[ bib 
.ps.gz 
.pdf ]
We present a datatype package that enables the use of shallow embedding technique to objectoriented specification and programming languages. The package incrementally compiles an objectoriented data model to a theory containing objectuniverses, 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 objectoriented corelanguage called , for which correctness of a Hoare logic with respect to an operational semantics is proven. Keywords: datatype package, extensible objectoriented data model, objectoriented specification,shallow embedding 
[72] 
Achim D. Brucker and Burkhart Wolff.
The HOLOCL Book.
Technical Report 525, ETH Zürich, 2006.
[ bib 
.pdf ]
HOLOCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higherorder Logic (HOL) instance of the interactive theorem prover Isabelle. HOLOCL defines a machinechecked 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 lambdacalculus with parametric polymorphism. As a consequence of conservativity with respect to higherorder logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOLOCL 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 Keywords: security, SecureUML, UML, OCL, HOLOCL, modeltransformation 
[73] 
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
An MDA framework supporting OCL.
In 6th OCL Workshop at the UML/MoDELS Conference, 2006.
[ bib 
.pdf ]
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 toolchain provides support for software modeling using UML/OCL and guides the user from typechecking 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.

[74] 
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
A model transformation semantics and analysis methodology for
SecureUML.
In Oscar Nierstrasz, Jon Whittle, David Harel, and Gianna Reggio,
editors, MoDELS 2006: Model Driven Engineering Languages and Systems,
LNCS 4199, pages 306320. SpringerVerlag, Genova, 2006.
An extended version of this paper is available as ETH Technical
Report, no. 524.
[ bib 
DOI 
.pdf ]
SecureUML is a security modeling language for formalizing access control requirements in a declarative way. It is equipped with a notation in terms of a profile, and can be combined with arbitrary design modeling languages. We present a semantics for SecureUML in terms of a model transformation to standard uml/ocl. The transformation scheme is used as part of an implementation of a tool chain ranging from frontend visual modeling tools over codegenerators to the interactive theorem proving environment . The methodological consequences for an analysis of the generated formulae are discussed.

[75] 
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.
Semantic issues of OCL: Past, present, and future.
In 6th OCL Workshop at the UML/MoDELS Conference, 2006.
[ bib 
http 
.pdf ]
We report on the results of a longterm project to formalize the semantics of OCL 2.0 in Higherorder Logic (HOL). The ultimate goal of the project is to provide a formalized, machinechecked semantic basis for a theorem proving environment for OCL (as an example for an objectoriented 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 programminglike verifications and specification refinement, which are, in our view, necessary to make OCL more fit for future extensions.

[76] 
Manuel Núñez García, Klaus Havelund, Grigore Rosu, and Burkhart
Wolff, editors.
Proceedings of the International Workshop on Formal Aspects of
Testing and Runtime Verification (FATES/RV), Seattle, USA, 2006. Springer
Verlag.
LNCS 4262.
[ bib 
DOI ]
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.

[77] 
David Aspinall, Christoph Lüth, and Burkhart Wolff.
Assisted Proof Document Authoring.
In Fourth International Conference on Mathematical Knowledge
Management (MKM 05), LNCS 3863. Springer Verlag, 2005.
[ bib 
DOI 
.pdf ]
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 humanreadable 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 humanreadable 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.

[78] 
David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff.
Specifying and Verifying Hysteresis Signature System with
HOLZ.
Technical Report 471, Computer Security Group, ETH Zürich, 1 2005.
[ bib 
.pdf ]
We report on a casestudy in using the dataoriented modeling language Z to formalize a security architecture for administering digital signatures and its architectural security requirements. Within an embedding of Z in the higherorder logic Isabelle/HOL, we provide formal machinechecked 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 processoriented 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).

[79] 
David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff.
Verification of a Signature Architecture with HOLZ.
In Formal Methods 2005, LNCS 3582, pages 269285. Springer
Verlag, 2005.
[ bib 
DOI 
.pdf ]
We report on a case study in using HOLZ, an embedding of Z in higherorder logic, to specify and verify a security architecture for administering digital signatures. We have used HOLZ to formalize and combine both dataoriented and processoriented architectural views. Afterwards, we formalized temporal requirements in Z and carried out verification in higherorder 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 timeconsuming nor more complex than model checking.

[80]  Achim D. Brucker and Burkhart Wolff. HOLTestGen 1.0.0 user guide. Technical Report 482, Computer Security Group, ETH Zürich, apr 2005. [ bib ] 
[81] 
Achim D. Brucker and Burkhart Wolff.
Interactive Testing using HOLTestGen.
In Wolfgang Grieskamp and Carsten Weise, editors, Formal
Approaches to Testing of Software (FATES 05), LNCS 3997, pages 87102.
SpringerVerlag, Edinburgh, 2005.
[ bib 
DOI ]
HOLTestGen is a test environment for specificationbased 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 nontrivial 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. HOLTestGen 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.

[82] 
Achim D. Brucker and Burkhart Wolff.
Symbolic test case generation for primitive recursive functions.
In Jens Grabowski and Brian Nielsen, editors, Formal Approaches
to Testing of Software (FATES 04), LNCS 3395, pages 1632. SpringerVerlag,
Linz 04, 2005.
[ bib 
DOI 
http ]
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 blackbox testing of external programs. Our method is twostaged: first, the original formula is partitioned into test cases by transformation into a Hornclause 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 AVLtrees and the redblack tree implementation in the standard library from SML/NJ.

[83] 
Achim D. Brucker and Burkhart Wolff.
A verification approach for applied system security.
International Journal on Software Tools for Technology Transfer
(STTT), 7(3):233247, 2005.
[ bib 
DOI 
.pdf ]
We present a method for the security analysis of realistic models over offtheshelf systems and their configuration by formal, machinechecked proofs. The presentation follows a large case study based on a formal security analysis of a CVSServer architecture.

[84] 
Thomas Meyer and Burkhart Wolff.
Tacticbased optimized compilation of functional programs.
In JeanChristophe Filliatre, Christine Paulin, and Benjamin Werner,
editors, Types for Proofs and Programs (TYPES 2004), LNCS 3839, pages
202215. Springer Verlag, 8 2005.
[ bib 
DOI 
.pdf ]
Within a framework of correct codegeneration 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 crosscheck 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 sidecalculi inferring e.g. strictness of functions. The derived rules were grouped and setup as an instance of our generic, tacticbased translator for specifications to code.

[85] 
Burkhart Wolff.
Correct tools for formal methods in software engineering, 2005.
Habilitationsschrift.
[ bib 
.pdf ]
The development of 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 socalled logical framework by their semantics using a particular representation technique  called shallow embedding  motivated by more efficient deduction. Based on this representation, symbolic computations in tool implementations can be based on formally proven correct derived rules. As such, this correctnessoriented approach has been known for a while and has been criticized for a number of shortcomings:

[86] 
Achim D. Brucker and Burkhart Wolff.
Symbolic test case generation for primitive recursive functions.
Technical Report 449, Computer Security Group, ETH Zürich, jun
2004.
[ bib ]
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 blackboxtesting of external programs.

[87] 
Nicole Rauch and Burkhart Wolff.
Formalizing java's two'scomplement integral type in isabelle/hol.
Technical Report 458, ETH Zürich, 11 2004.
[ bib 
www: ]
We present a formal model of Java two’scomplement 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, machinechecked proofs for the ring properties and divisor/remainder theorems etc. are provided. This work is suited to build the framework for machinesupported reasoning over arithmetic formulae in the context of Java sourcecode verification.

[88] 
Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.
HOLZ 2.0: A Proof Environment for ZSpecifications.
Journal of Universal Computer Science, 9(2):152172, February
2003.
[ bib 
DOI 
.ps.gz 
.pdf ]
We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structurepreserving, 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 wellknown and trusted theorem prover with advanced deduction technology such as higherorder rewriting, tableauxbased provers and arithmetic decision procedures. A further achievement of this work is the integration of our embedding into a new toolchain providing a Zoriented type checker, documentation facilities and macro support for refinement proofs; as a result, the gap has been closed between a logical embedding proven correct and a tool suited for applications of nontrivial size.

[89] 
David Basin and Burkhart Wolff, editors.
Theorem Proving in Higher Order Logics, 16th
International Conference (TPHOLs 2003), Rome, Italy, Sep 2003.
SpringerVerlag.
LNCS 2758.
[ bib 
DOI ]
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ür:Researchers and professionalsSchlagworte: automated deduction formal methods formal verification hardware verification higherorder logic logic design mathematical logic model checking program verification proof theory theorem provers theorem proving unification

[90] 
Achim D. Brucker and Burkhart Wolff.
Using theory morphisms for implementing formal methods tools.
In Herman Geuvers and Freek Wiedijk, editors, Types 2002,
Proceedings of the workshop Types for Proof and Programs, LNCS 2646.
SpringerVerlag, Nijmegen, 2003.
[ bib 
DOI ]
Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed metalogic, 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.

[91] 
Achim D. Brucker and Burkhart Wolff.
A case study of a formalized security architecture.
In Thomas Arts and Wan Fokkink, editors, Eighth International
Workshop onFormal Methods for Industrial Critical Systems (FMICS'03),
volume 80. Elsevier Science Publishers, 2003.
[ bib 
.ps.gz 
.pdf ]
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 CVSServer architecture performed in [93]. The analysis is based on an abstract architecture (enforcing a rolebased access control on the repository), which is refined to an implementation architecture (based on the usual discretionary access control provided by the 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, machinechecked 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 offtheshelf system by formal machinechecked proofs.

[92] 
Nicole Rauch and Burkhart Wolff.
Formalizing java's two'scomplement integral type in isabelle/hol.
In Electronic Notes in Theoretical Computer Science, volume 80.
Elsevier Science Publishers, 2003.
[ bib 
.pdf ]
We present a formal model of the Java two'scomplement 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, machinechecked proofs for the ring properties and divisor/remainder theorems etc. are provided. This work is suited to build the framework for machinesupported reasoning over arithmetic formulae in the context of Java sourcecode verification.

[93] 
Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.
The CVSserver case study: A formalized security architecture.
In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors,
FMTOOLS 2002, number 200211 in Technical Report, pages 4752.
Augsburg, July 2002.
[ bib 
http 
.pdf ]
CVS is a widely known version management system. Configured in server mode, it can be used for the distributed development of software as well as its distribution from a central database called the repository. In this setting, a number of security mechanisms have to be integrated into the CVSserver architecture. We present an abstract formal model of the access control aspects of a CVSserver architecture enforcing a rolebased access control on the data in the repository. This abstract architecture is refined to an implementation architecture, which represents (an abstraction of) a concrete CVSserver 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 HOLZ, such that refinement proofs for this case study can be done in Isabelle/HOL.

[94] 
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff.
HOLZ 2.0: A proof environment for zspecifications.
In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors,
FMTOOLS 2002, number 200211 in Technical Report, pages 3338.
Augsburg, July 2002.
[ bib 
http 
.pdf ]
We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a L^{A}T_{E}Xbased front end (including the integrated typechecker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOLZ, namely for the schemacalculus and structural Z proofs.

[95] 
Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.
A CVSServer security architecture  concepts and formal
analysis.
Technical Report 182, AlbertLudwigsUniversität Freiburg, 2002.
[ bib 
http 
.ps.gz 
.pdf ]
We present a secure architecture of a CVSserver, its implementation (i.e. mainly its configuration) and its formal analysis. Our CVSserver is uses cvsauth, that provides protection of passwords and protection of some internal data of the CVS repository. In contrast to other (security oriented) CVSarchitectures, our approach allows the CVSserver run on an open filesystem, i.e. a filesystem where users can have direct access both by CVScommands and by standard UNIX/POSIX commands such as mv. For our secure architecture of the CVSserver, we provide a formal specification and security analysys. The latter is based on a refinement mapping highlevel security requirements on the architecture on lowlevel security mechanisms on the UNIX/POSIX filesystem level. The purpose of the formal analysis of the secure CVSserver architecture is twofold: First, it is the bases for the specification of mutual security properties such as nonrepudiation, 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 
[96] 
Achim D. Brucker and Burkhart Wolff.
HOLOCL: Experiences, consequences and design choices.
In JeanMarc Jézéquel, Heinrich Hussmann, and Stephen Cook,
editors, UML 2002: Model Engineering, Concepts and Tools, number 2460
in Lecture Notes in Computer Science. SpringerVerlag, Dresden, 2002.
[ bib 
DOI 
http 
.pdf ]
Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higherorder logic [97], 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 sublanguage 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, higherorder logic 
[97] 
Achim D. Brucker and Burkhart Wolff.
A proposal for a formal OCL semantics in Isabelle/HOL.
In César Muñoz, Sophiène Tahar, and Víctor
Carreño, editors, Theorem Proving in Higher Order Logics, number
2410 in Lecture Notes in Computer Science, pages 99114. SpringerVerlag,
Hampton, VA, USA, 2002.
[ bib 
DOI 
http 
.pdf ]
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 
[98]  Burkhart Wolff, Oliver Berthold, Sebastian Clauß, Hannes Federrath, Stefan Köpsell, and Andreas Pfitzmann. Towards a formal analysis of a mix network. Technical Report 171, AlbertLudwigsUniversität Freiburg, 2002. [ bib  .pdf ] 
[99] 
Achim D. Brucker and Burkhart Wolff.
Testing distributed component based systems using UML/OCL.
In K. Bauknecht, W. Brauer, and Th. Mück, editors,
Informatik 2001, volume 1 of Tagungsband der GI/ÖCG Jahrestagung,
pages 608614, Wien, November 2001. Österreichische Computer
Gesellschaft.
[ bib 
http 
.ps.gz 
.pdf ]
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 UMLmodel for a component can be used in a blackbox 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.

[100] 
Achim D. Brucker and Burkhart Wolff.
Checking OCL Constraints in Distributed Systems Using J2EE/EJB.
Technical Report 157, AlbertLudwigsUniversität Freiburg, July
2001.
[ bib 
http 
.ps.gz 
.pdf ]
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 UMLmodel for a component can be used in a blackbox 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 
[101] 
Christoph Lüth and Burkhart Wolff.
sml_tk: Functional programming for guis  reference manual.
Technical Report 158, AlbertLudwigsUniversität Freiburg, July
2001.
[ bib 
.pdf ]
In this reference manual, we describe the SMLbased programming environment sml_tk for graphical user interfaces, version 3.0. sml_tk is based on the highly portable XWindow 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 infoboxes, treelistwidgets, tabs and tables. sml_tk is the basic library for a collection of GUIs for formal method tools such as TAS and IsaWin.

[102] 
Burkhart Wolff.
Verifying explicit substitution calculi in binding structures with
effect binding.
In Pierre Lescanne, editor, Workshop on Explicit Substitution
Theory and Applications (WESTAPP'01), volume 210 of Logic Group
Preprint Series, pages 58  71. Department of Philosophy  Utrecht
University, May 2001.
[ bib 
.ps.gz ]
Binding structures enrich traditional abstract syntax by providing support for representing binding mechanisms (based on deBruijn indices), termschemata 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 effectbinding that enables the explicit representations of both contexts and terms inside one term metalanguage,2) The foundation of a formal (machineassisted) substitution theory of effectbinding that is wellsuited 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.

[103] 
T. Meyer and Burkhart Wolff.
Correct codegeneration in a generic framework.
In M. Aargaard, J. Harrison, and T. Schubert, editors, TPHOLs
2000: Supplemental Proceedings, OGI Technical Report CSE 00009, pages
213230. Oregon Graduate Institute, Portland, USA, July 2000.
[ bib 
.ps.gz 
.pdf ]
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 wellfounded recursion) and develop their theory in Isabelle/HOL. These theories serve as a semantic interface for a generic codegenerator which is set up for each program notion with an individual codescheme for SML.

[104]  David Basin, Luca Viganò, and Burkhart Wolff. Berichte aus den instituten: Lehrstuhl für softwaretechnik und softwareproduktionsumgebung, freiburg. PIK (Praxis der Informationsverarbeitung und Kommunikation), 23(4):248249, 2000. [ bib  .ps.gz  .pdf ] 
[105] 
Christoph Lüth and Burkhart Wolff.
More about TAS and IsaWin: Tools for formal program development.
In T. Maibaum, editor, Fundamental Approaches to Software
Engineering FASE 2000. Joint European Conferences on Theory and Practice of
Software ETAPS 2000, number 1783 in Lecture Notes in Computer Science,
pages 367 370. Springer Verlag, 2000.
[ bib 
.ps.gz 
.pdf.gz ]
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.

[106] 
Christoph Lüth and Burkhart Wolff.
TAS  a generic window inference system.
In J. Harrison and M. Aagaard, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, number 1869
in Lecture Notes in Computer Science, pages 405422. Springer Verlag, 2000.
[ bib 
.pdf ]
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 commandlanguagefree user interaction by gestures like drag&drop and proofbypointing, and a development management for transformational proofs. It is <em>generic</eM> 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.

[107] 
Christoph Lüth and Burkhart Wolff.
Functional design and implementation of graphical user interfaces for
theorem provers.
Journal of Functional Programming, 9(2):167 189, 1999.
[ bib 
DOI 
.ps.gz 
.pdf ]
This paper attempts to develop a metaphor suited to visualize the LCFstyle 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 <em>generic</em> and <em>open</em> 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.

[108] 
Chritoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, and Burkhart
Wolff.
HOLZ in the UniForMWorkbench  a case study in tool
integration for z.
In J. Bowen, editor, 11. International Conference of Z Users
ZUM'98, LNCS 1493, pages 116134. Springer Verlag, 1998.
[ bib 
DOI 
.ps.gz ]
The UniForMWorkbench is an open toolintegration environment providing typesafe communication, a toolkit for graphical userinterfaces, 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 HOLZ 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 selfdeveloped 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.

[109] 
C. Lüth, E. W. Karlsen, Kolyang, S. Westmeier, and B. Wolff.
Tool integration in the uniform workbench.
In Berghammer and Hoffmann, editors, Workshop on Tool Support
for System Specification, Development, and Verification, 1998.
[ bib 
.ps.gz ]
The UniForMWorkbench is an open toolintegration environment providing typesafe communication, a toolkit for graphical userinterfaces, 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 HOLZ 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 selfdeveloped 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.

[110]  Haykal Tej, Christoph Lüth, and Burkhart Wolff. Generic transformational program development. Unpublished Paper., 1998. [ bib  .pdf ] 
[111]  Kolyang, C. Lüth, T. Meier, and B. Wolff. Tas and isawin: Generic interfaces for transformational program development and theorem proving. In M. Dauchet M. Bidoit, editor, TAPSOFT 97: Theory and Practice of Software Development, LNCS 1214, pages 855858. Springer Verlag, 1997. [ bib  DOI  .ps.gz ] 
[112]  Kolyang, C. L}uth, T. Meier, and B. Wolff. Generic interfaces for transformation systems and interactive theorem provers. In B. Buth K.Berghammer, J.Peleska, editor, Proceedings of the “International Workshop for Tool Support in Verification and Validation'', BISS Monographs. Shaker Verlag, 1997. [ bib  .ps.gz ] 
[113] 
H. Tej and B. Wolff.
A corrected failuredivergence model for csp in isabelle/hol.
In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Proceedings
of the FME 97  Industrial Applications and Strengthened Foundations of
Formal Methods, LNCS 1313, pages 318337. Springer Verlag, 1997.
[ bib 
DOI 
.ps.gz 
.pdf ]
We present a failuredivergence 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.

[114] 
B. Wolff.
A Generic Calculus of Transformations.
PhD thesis, Universität Bremen, Aachen, 1997.
[ bib 
http ]
Binding structures enrich traditional abstract syntax by providing support for representing binding mechanisms (based on deBruijn indices), termschemata and a very clean algebraic theory of substitution. We provide the following main results:

[115]  Kolyang, C. Lüth, T. Meier, and B. Wolff. Generating graphical userinterfaces in a functional setting. In N. Merriam, editor, Proceedings of the User Interfaces for Theorem Provers (UITP 96), Technical Report. University of York, 1996. [ bib  .ps.gz ] 
[116] 
Kolyang, T. Santen, and B. Wolff.
Correct and userfriendly implementation of transformation systems.
In M.C. Gaudel and J. Woodcock, editors, FME 96  Industrial
Benefits and Advances in Formal Methods, LNCS 1051, pages 629648. Springer
Verlag, 1996.
[ bib 
DOI 
.ps.gz 
.pdf ]
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 userfriendly way. We illustrate the approach by proving and implementing the transformation Global Search on the basis of the tactical theorem prover Isabelle. A graphical userinterface based on the XWindow toolkit Tk provides user friendly access to the underlying machinery.

[117] 
Kolyang, T. Santen, and B. Wolff.
A structure preserving encoding of z in isabelle/hol.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics  9th International Conference, LNCS 1125,
pages 283298. Springer Verlag, 1996.
[ bib 
.ps.gz 
.pdf ]
We present a semantic representation of the core concepts of the specification language Z in higherorder 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.

[118]  C. Lüth, S. Westmeier, and B. Wolff. sml_tk: Functional programming for graphical user interfaces. Technical Report 8/96, Universität Bremen, 1996. [ bib  .ps.gz ] 
[119]  B. KriegBrückner, J. Liu, H. Shi, and B. Wolff. Towards correct, efficient and reusable transformational developments. In M. Broy and S. Jähnichen, editors, KORSO  Methods, Languages, and Tools for the Construction of Correct Software, LNCS 1009, pages 270284. Springer Verlag, 1995. [ bib  .ps.gz ] 
[120]  Kolyang and B. Wolff. Development by refinement revisited: Lessons learnt from an example. In G. Snelting, editor, Beiträge der GIFachtagung “Softwaretechnik 95'', Braunschweig, Mitteilungen der Fachgruppen `Software Engineering' und `RequirementsEngineering',Band 15, Heft 3, ISSN 07208928, pages 5766. GI, 1995. [ bib  .ps.gz ] 
This file was generated by bibtex2html 1.96.