[1] Achim D. Brucker, Lukas Brügger, Abderrahmane Feliachi, Chantal Keller, Matthias P. Krieger, Delphine Longuet, Yakoub Nemouchi, Frédéric Tuong, and Burkhart Wolff. HOL-TestGen 1.8.0 user guide. Technical Report 1586, Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, April 2016. [ bib | http | .pdf ]
Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL
[2] 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 over-approximates the set of all concrete reachable states and the set of feasible paths. We present an abstract framework for TRACER and similar CEGAR-like systems. The framework provides 1) a graph-transformation based method for reducing the feasible paths in control-flow graphs, 2) a model for symbolic execution, subsumption, predicate abstraction and invariant generation. In this framework we formally prove two key properties: correct construction of the symbolic states and preservation of feasible paths. The framework focuses on core operations, leaving to concrete prototypes to “fit in” heuristics for combining them.

[3] Achim D. Brucker and Burkhart Wolff. Monadic sequence testing and explicit test-refinements. In Tests and Proofs - 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings, volume LNCS 7942 of Lecture Notes in Computer Science, pages 17-36, 2016. [ bib | DOI | http | .pdf ]
Abstract We present an abstract framework for sequence testing that is implemented in Isabelle/HOL-TestGen. Our framework is based on the theory of state-exception monads, explicitly modelled in HOL, and can cope with typed input and output, interleaving executions including abort, and synchronisation. The framework is particularly geared towards symbolic execution and has proven effective in several large case-studies involving system models based on large (or infinite) state. On this basis, we rephrase the concept of test-refinements for inclusion, deadlock and IOCO-like tests, together with a formal theory of its rela- tion to traditional, IO-automata based notions.

[4] 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. Paris-Sud, 2016. [ bib | http ]
[5] Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. Technical Report 1582, LRI, Univ Paris Sud, CNRS, Centrale Supélec, Université Paris-Saclay, 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 three-valued logic, that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the “Annex A” of the OCL standard, leads to different interpretations of corner cases. Many of these corner cases had been subject to formal analysis since more than ten years. The situation complicated with the arrival of version 2.3 of the OCL standard. OCL was aligned with the latest version of UML: this led to the extension of the three-valued logic by a second exception element, called null. While the first exception element invalid has a strict semantics, null has a non strict interpretation. The combination of these semantic features lead to remarkable confusion for implementors of OCL compilers and interpreters. In this paper, we provide a formalization of the core of OCL in HOL. It provides denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Moreover, we describe a coding-scheme for UML class models that were annotated by code-invariants and code contracts. An implementation of this coding-scheme has been undertaken: it consists of a kind of compiler that takes a UML class model and translates it into a family of definitions and derived theorems over them capturing the properties of constructors and selectors, tests and casts resulting from the class model. However, this compiler is not included in this document. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. They reflect a challenge to define and implement OCL tools in a uniform manner. Overall, this document is intended to provide the basis for a machine-checked text “Annex A” of the OCL standard targeting at tool implementors.

[6] Frédéric Tuong and Burkhart Wolff. A Meta-Model for the Isabelle API. Archive of Formal Proofs, 2015. [ bib | http ]
[7] 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 EURO-MILS Project, 2015. available from the Project site: http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper-October2015.pdf. [ bib | DOI ]
[8] Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Symbolic test-generation in HOL-TestGen/Cirta: A case study. Int. J. Software Informatics, 9(2):177-203, 2015. [ bib | .pdf ]
HOL-TestGen/CirTA is a theorem-prover based test generation environment for specifications written in Circus, a process-algebraic specification language in the tradition of CSP. HOL-TestGen/CirTA is based on a formal embedding of its semantics in Isabelle/HOL, allowing to derive rules over specification constructs in a logically safe way. Beyond the derivation of algebraic laws and calculi for process refinement, the originality of HOL-TestGen/ CirTA consists in an entire derived theory for the generation of symbolic test-traces, including optimized rules for test-generation as well as rules for symbolic execution. The deduction process is automated by Isabelle tactics, allowing to protract the state-space explosion resulting from blind enumeration of data. The implementation of test-generation procedures in CirTA is completed by an integrated tool chain that transforms the initial Circus specification of a system into a set of equivalence classes (or “symbolic tests”), which were compiled to conventional JUnit test-drivers. This paper describes the novel tool-chain based on prior theoretical work on semantics and test-theory and attempts an evaluation via a medium-sized case study performed on a component of a real-world safety-critical medical monitoring system written in Java. We provide experimental measurements of the kill-capacity of implementation mutants.

[9] 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):34-71, 2015. [ bib | DOI | .pdf ]
Firewalls are an important means to secure critical ICT infrastructures. As configurable off-the-shelf products, the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well as the correct configuration. While testing the implementation can be done once by the manufacturer, the configuration needs to be tested for each application individually. This is particularly challenging as the configuration, implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and, thus, difficult to validate. This paper presents a formal model of both stateless and stateful firewalls (packet filters), including network address translation (NAT), to which a specification-based conformance test case generation approach is applied. Furthermore, a verified optimisation technique for this approach is presented: Starting from a formal model for stateless firewalls, a collection of semantics-preserving policy transformation rules and an algorithm that optimises the specification with respect of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates verification and testing, i. e., tests and proofs to support conformance testing of network policies. The presented approach is supported by a test framework that allows to test actual firewalls using the test cases generated based on the formal model. Finally, a report on several larger case studies is presented.

[10] 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 Multi-Paradigm Modeling co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, GEMOC+MPM@MoDELS 2015, Ottawa, Canada, September 28, 2015., pages 14-19, 2015. [ bib | .pdf ]
[11] Achim D. Brucker, Oto Havle, Yakoub Nemouchi, and Burkhart Wolff. Testing the ipc protocol for a real-time 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. Springer-Verlag, Heidelberg, 2015. [ bib | DOI | http | .pdf ]
In this paper, we adapt model-based testing techniques to concurrent code, namely for test generations of an (industrial) OS kernel called PikeOS. Since our data-models are complex, the problem is out of reach of conventional model-checking techniques. Our solution is based on symbolic execution implemented inside the interactive theorem proving environment Isabelle/HOL extended by a plugin with test generation facilities called HOL-TestGen. As a foundation for our symbolic computing techniques, we refine the theory of monads to embed interleaving executions with abort, synchronization, and shared memory to a general but still optimized behavioral test framework. This framework is instantiated by a model of PikeOS inter-process communication system-calls. Inheriting a micro-architecture going back to the L4 kernel, the system calls of the IPC-API are internally structured by atomic actions; according to a security model, these actions can fail and must produce error-codes. Thus, our tests reveal errors in the enforcement of the security model.

Keywords: test program generation, symbolic test case generations, black box testing, testing operating systems, certification, CC, concurrency, interleaving
[12] 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 27-29, 2015, Proceedings, pages 375-389, 2015. [ bib | DOI | http ]
[13] 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 ]
[14] 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/CISC-Kernel.shtml, Formal proof development. [ bib ]
[15] 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 co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., pages 43-52, 2014. [ bib | .pdf ]
[16] 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 co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., pages 83-99, 2014. [ bib | .pdf ]
[17] Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight ocl: A proposal for a machine-checked 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 three-valued logic that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the "Annex A" of the OCL standard, leads to different interpretations of corner cases. We formalize the core of OCL: denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. Overall, this document is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.

[18] Thierry Jéron, Margus Veanes, and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). Dagstuhl Reports, 3(1):1-29, 2013. [ bib | DOI | http ]
[19] Abderrahmane Feliachi, Marie-Claude 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. Springer-Verlag, 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 “theorem-prover based testing”. Theorem-prover based testing can be adapted to a specific specification language via a representation of its formal semantics, paving the way for specific support of its constructs. The main challenge of this approach is to reduce the gap between pen-and-paper semantics and formal mechanized theories. In this paper we consider testing based on the Circus specification language. This language integrates the notions of states and of complex data in a Z-like fashion with communicating processes inspired from CSP. We present a machine-checked formalization in Isabelle/HOL of this lan- guage and its testing theory. Based on this formal representation of the semantics we revisit the original associated testing theory. We discovered unforeseen simplifications in both definitions and symbolic computations. The approach lends itself to the construction of a tool, that directly uses semantic definitions of the language as well as derived rules of its testing theory, and thus provides some powerful sym- bolic computation machinery to seamlessly implement them both in a technical environment.

Keywords: symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing
[20] Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Hol-testgen/fw: An environment for specification-based firewall conformance testing. In International Colloquium on Theoretical Aspects of Computing (ICTAC), number 8049 in Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2013. [ bib | .pdf ]
The HOL-TestGen environment is conceived as a system for modeling and semi-automated test generation with an emphasis on expressive power and generality. However, its underlying technical framework Isabelle/HOL supports the customization as well as the development of highly automated add-ons working in specific application domains. In this paper, we present HOL-TestGen/fw, an add-on for the test framework HOL-TestGen, that allows for testing the conformance of firewall implementations to high-level security policies. Based on generic theories specifying a security-policy language, we developed specific theories for network data and firewall policies. On top of these firewall specific theories, we provide mechanisms for policy transformations based on derived rules and adapted code-generators producing test drivers. Our empirical evaluations shows that HOL-TestGen/fw is a competitive environment for testing firewalls or high-level policies of local networks.

Keywords: symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing
[21] Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, and Burkhart Wolff. Pervasive parallelism in highly-trustable interactive theorem proving systems. In MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 359-363. Springer, 2013. [ bib | DOI | .pdf ]
Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware. The architecture of contemporary interactive provers such as Coq, Isabelle or the HOL family goes back to the influential LCF system from 1979, which has pioneered key principles like correctness by construction for primitive inferences and definitions, free programmability in userspace via ML, and toplevel command interaction. Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large libraries of formalized mathematics etc. Despite this success, the operational model of interactive proof checking was limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF.

[22] Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff. Test program generation for a microprocessor - a case-study. In Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13), volume LNCS 7942 of Lecture Notes in Computer Science, pages 76-95. 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 HOL-TestGen, a model-based testing environment which is an extension of Isabelle/HOL. We develop several conformance test scenarios, where processor models were used to synthesize test programs that were run against real hard- ware in the loop. Our test case generation approach directly benefits from the existing models and formal proofs in Isabelle/HOL.

Keywords: test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
[23] Burkhart Wolff, Marie-Claude Gaudel, and Abderrahmane Feliachi, editors. Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers, volume LNCS 7681 of Lecture Notes in Computer Science. Springer, 2013. [ bib ]
[24] Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff. On the Semantics of Object-Oriented Data Structures and Path Expressions. In OCL@MoDELS, volume 1092 of CEUR Workshop Proceedings, pages 23-32. CEUR-WS.org, 2013. [ bib ]
[25] 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 103-111. CEUR-WS.org, 2013. [ bib ]
[26] Achim D. Brucker and Burkhart Wolff. On Theorem Prover-based Testing. Formal Asp. Comput. (FAOC), 25(5):683-721, 2013. [ bib | DOI | .pdf ]
HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.

Keywords: Isabelle/HOL, Theorem proving, Model-based Testing, Program-based Testing, Testcase Generation
[27] Achim D. Brucker, Delphine Longuet, Frédéric Tuong, and Burkhart Wolff. On the semantics of object-oriented data structures and path expressions (extended version). Technical Report 1565, Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, 2013. [ bib | http | .pdf ]
/is perceived as the de-facto standard for specifying object-oriented models in general and data models in particular. Since recently, all data types of /comprise two different exception elements: invalid (“bottom” in semantics terminology) and null (for “non-existing element”). This has far-reaching consequences on both the logical and algebraic properties of expressions as well as the path expressions over object-oriented data structures, , class models. In this paper, we present a formal semantics for object-oriented data models in which all data types and, thus, all class attributes and path expressions, support 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: Object-oriented Data Structures, Path Expressions, Featherweight OCL, Null, Invalid, Formal Semantics
[28] Abderrahmane Feliachi, Burkhart Wolff, and Marie-Claude 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.

[29] Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff. HOL-TestGen 1.7.0 user guide. Technical Report 1551, Laboratoire en Recherche en Infromatique (LRI), Université Paris-Sud 11, France, April 2012. [ bib | http | .pdf ]
Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL
[30] 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 19-24, New York, NY, USA, 2012. ACM. [ bib | DOI | www: | .pdf ]
Keywords: HOL-OCL, OCL, formal semantics
[31] Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Isabelle/Circus: A process specification and verification environment. In VSTTE, volume LNCS 7152 of Lecture Notes in Computer Science, pages 243-260, 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 machine-checked, formal semantics based on a "shallow embedding" of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and imple- ment tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.

[32] Abderrahmane Feliachi. Representing Circus Operational Semantics in Isabelle/HOL. Technical Report 1544, LRI, http://www.lri.fr/Rapports-internes, Université Paris-Sud XI, August 2011. [ bib | .pdf ]
[33] Jordi Cabot, Robert Clarisó, Martin Gogolla, and Burkhart Wolff. Preface (ocl 2011 proceedings). ECEASST, 44, 2011. [ bib ]
[34] Burkhart Wolff and Fatiha Zaïdi, editors. Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 7-10, 2011. Proceedings, volume 7019 of Lecture Notes in Computer Science. Springer, 2011. [ bib | DOI ]
[35] 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 ]
[36] Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. An approach to modular and testable security models of real-world health-care applications. Proceedings of the ACM Symposium on Access control models and technologies, pages 133-142. 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 large-scale development project aiming to modernise the IT infrastructure of the National Health Service (NHS) in England. Consisting of heteroge- neous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features. We model the four information governance principles, comprising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed en- velopes and legitimate relationships. The model is given in Higher-order Logic (HOL) and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular em- phasis is put on the modular description of security poli- cies and their generic combination and its consequences for model-based testing.

[37] Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff. HOL-TestGen 1.5.0 user guide. Technical Report 670, ETH Zurich, April 2010. [ bib | .pdf ]
[38] Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Unifying Theories in Isabelle/HOL. In Unifying Theories of Programming (UTP2010), number 6445 in Lecture Notes in Computer Science. Springer-Verlag, 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.

Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and xsCircus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation. UTP, Theorem Proving, Isabelle/HOL, CSP, Circus

Keywords: UTP, Theorem Proving, Symbolic test case generations, Isabelle/HOL
[39] Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and Burkhart Wolff. A Specification-based 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 DNF-based test case generation methods to class models and recursive query operations on them. A key feature of our approach is an implicit representation of object graphs avoiding a repre- sentation based on object-id's; thus, our approach avoids the generation of isomorphic object graphs by using a concise and still human-readable symbolic representation.

[40] 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 well-known means of specifying operations. In this paper we deal with the problem of operation contract simulation, i.e., determining operation results satisfying the postconditions based on input data supplied by the user; simulating operation contracts is an important technique for requirements validation and prototyping. Current approaches to operation contract simulation exhibit poor performance for large sets of input data or require additional guidance from the user. We show how these problems can be alleviated and describe an efficient as well as fully automatic approach. It is implemented in our tool OCLexec that generates from UML/OCL operation contracts corresponding Java implementations which call a constraint solver at runtime. The generated code can serve as a prototype. A case study demonstrates that our approach can handle problem instances of considerable size.

[41] 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:345-354, 2010. [ bib | DOI | .pdf ]
We present an optimization technique for model-based generation of test cases for firewalls. Based on a formal model for firewall policies in higher-order logic, we derive a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/hol. Finally, we use the normalized policies to generate test cases with the domain-specific firewall testing tool . The resulting procedure is characterized by a gain in efficiency of two orders of magnitude and can handle configurations with hundreds of rules as occur in practice. Our approach can be seen as an instance of a methodology to tame inherent state-space explosions in test case generation for security policies.

[42] Burkhart Wolff. Top-down vs. Bottom-up: 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 Krieg-Brückner. [ bib | .pdf ]
[43] Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(1-2):111-144, 2009. [ bib | DOI | .pdf ]
Boogie is a verification condition generator for an imperative core language. It has front-ends for the programming languages C# and C enriched by annotations in first-order logic, ie pre- and postconditions, assertions, and loop invariants. Moreover, concepts like ghost fields, ghost variables, ghost code and 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 language-specific 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, HOL-Boogie, that combines Boogie with the interactive theorem prover Isabelle/, for a specific C front-end and machine/memory model. In particular, we present specific techniques combining automated and interactive proof methods for code verification. The main goal of our environment is to help program verification engineers in their task to “debug” annotations and to find combined proofs where purely automatic proof attempts fail.

Keywords: Isabelle/HOL, Theorem proving, Program verification, Memory models, Annotation languages
[44] Achim D. Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica, 46(4):255-284, 2009. [ bib | DOI | .pdf ]
We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/HOL and the language is oriented towards OCL formulae in the context of UML class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.

Keywords: UML , OCL , object-oriented specification , refinement , formal methods
[45] Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler. Journal of Automated Reasoning (JAR), 42(2-4):349-388, 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 multi-priority process scheduler. The proof architecture links a layer of behavioral reasoning over system-trace sets with a concrete, fairly realistic implementation written in C. Our microkernel provides an infra-structure for memory virtualization, for communication with hardware devices, for processes (represented as a sequence of assembler instructions, which are executed concurrently over an underlying, formally defined processor), and for inter-process communication (IPC) via synchronous message passing. The kernel establishes process switches according to IPCs and timer-events; however, the scheduling of process switches follows a hierarchy of priorities, favoring, e. g., system processes over application processes over maintenance processes. Besides the quite substantial models developed in Isabelle/HOL and the formal clarification of their relationship, we provide a detailed analysis what formal requirements a microkernel imposes on the key ingredients (hardware, timers, machine-dependent code) in order to establish the correct operation of the overall system. On the methodological side, we show how early modeling with hindsight to the later verification has substantially helped our project.

Keywords: Microkernel, Formal verification, Interactive theorem proving, Isabelle/HOL
[46] Achim D. Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pages 417-420. Springer-Verlag, Heidelberg, 2009. [ bib | DOI | http | .ps.gz | .pdf ]
We present HOL-TestGen, an extensible test environment for specification-based testing build upon the proof assistant Isabelle. HOL-TestGen leverages the semi-automated generation of test theorems (a form of a partition), and their refinement to concrete test data, as well as the automatic generation of a test driver for the execution and test result verification. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit and sequence test techniques in a logically consistent way.

Keywords: symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
[47] Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff. Extending OCL with null-references. In S. Ghosh, editor, MODELS 2009 Workshops, LNCS 6002, pages 261-275. Springer Verlag, Heidelberg, 2009. Best-Paper 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 three-valued propositional logic. Recent versions of the OCL standard added a second exception element, which, similar to the null references in object-oriented programming languages, is given a non-strict semantics. Unfortunately, this extension has been done in an ad hoc manner, which results in several inconsistencies and contradictions.

In this paper, we present a consistent formal semantics (based on our approach) that includes such a non-strict exception element. We discuss the possible consequences concerning class diagram semantics as well as deduction rules. The benefits of our approach for the specification-pragmatics of design level operation contracts are demonstrated with a small case-study.

Keywords: , UML, OCL, null reference, formal semantics
[48] Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, and Burkhart Wolff. A verification approach for system-level concurrent programs. In Verified Software: Theories, Tools, Experiments, LNCS 5295, pages 161-176. 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 Hoare-Logic. C0 is compiled by a verified compiler into assembly code representing a cooperative concurrent transition system. For the latter, it is shown that it can actually be executed in a true concurrent way reflecting the C0 semantics.

[49] Achim D. Brucker and Burkhart Wolff. Extensible universes for object-oriented data models. In Jan Vitek, editor, Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008), LNCS 5142, pages 438-462. Springer-Verlag, Paphos, Cyprus, July 2008. [ bib | DOI | http | .pdf ]
We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. This datatype package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, accessors functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for an object-oriented core-language called imp++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven.

[50] Sascha Böhme, Rustan Leino, and Burkhart Wolff. HOL-Boogie - 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 Higher-Order Logics (TPHOLs 2008), LNCS 5170. Springer-Verlag, Montreal, Canada, 2008. [ bib | DOI | .pdf ]
Boogie is a program verification condition generator for animperative core language. It has front-ends for the programming languagesC# and C enriched by annotations in first-order logic.Its verification conditions - constructed via a wp calculus from these annotations - are usually transferred to automated theorem provers such as Simplify or Z3. In this paper, however, we present a proof-environment,HOL-Boogie, that combines Boogie with the interactivetheorem prover Isabelle/HOL. In particular, we present specific techniquescombining automated and interactive proof methods for code-verification.We will exploit our proof-environment in two ways: First, we present scenariosto debugännotations (in particular: invariants) by interactiveproofs. Second, we use our environment also to verify background theories,i.e. theories for data-types used in annotations as well as memoryand machine models underlying the verification method for C.

[51] Achim D. Brucker and Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning (JAR), Selected Papers of the AVOCS-VERIFY Workshop 2006(3-4):219-249, 2008. Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds). [ bib | DOI | http ]
We present an extensible encoding of object-oriented data models into higher-order logic (HOL). Our encoding is supported by a datatype package that leverages the use of the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model, i.e., a class model, to a theory containing object-universes, constructors, accessor functions, coercions (casts) between dynamic and static types, characteristic sets, and co-inductive class invariants. The package is conservative, i. e., all properties are derived entirely from constant definitions, including the constraints over object structures. As an application, we use the package for an object-oriented core-language called IMP++, for which we formally prove the correctness of a Hoare logic with respect to a denotational semantics.

[52] 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 97-101. Springer Berlin / Heidelberg, 2008. [ bib | DOI | .pdf ]
We present the theorem proving environment HOL-OCL that is integrated in a MDE framework. HOL-OCL allows to reason over UML class models annotated with OCL specifications. Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. provides several derived proof calculi that allow for formal derivations establishing the validity of UML/OCL formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.

[53] Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Model-based firewall conformance testing. In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES 2008, LNCS 5047, pages 103-118. Springer-Verlag, 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 model-based testing tool HOL-TestGen. Based on a formal model of firewalls and their policies in HOL, we first present a derived theory for simplifying policies. We discuss different test plans for test specifications. Finally, we show how to integrate these issues to a domain-specific firewall testing tool HOL-TestGen/FW.

[54] Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Verifying test-hypotheses - an experiment in test and proof. In Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko, editors, Model-based Testing (MBT) 2008, volume 202 of Electronic Notes in Theoretical Computer Science, pages 15-28, Budapest, Hungary, 2008. Elsevier Science Publishers. [ bib | DOI | .pdf ]
HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. The HOL-TestGen method is two-staged: first, the original formula, called test specification, is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs. As such, explicit test hypotheses establish a logical link between validation by test and by proof. Since HOL-TestGen generates explicit test hypotheses and makes them amenable to formal proof, the system is in a unique position to explore the relations between them at an example.

[55] David Basin, Hironobu Kuruma, Shin Nakajima, and Burkhart Wolff. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. Computer Software - Journal of the Japanese Society for Software Science and Technology, 24(2):21-26, April 2007. In Japanese. [ bib | http ]
Z is a standardized and well-established formal specification language originally developed in the 80ies by researchers at oxford University. Although the original emphasis of Z is on specification, the semantics for Z can be expressed within higher-order logic (HOL). On this basis, a theorem-proving environment such as Isabelle/HOL-Z can be built. In this paper, we show how properties over specifications can be formally proven in HOL-Z. Particular emphasis is put on proving relationships between specification such as refinement.

[56] 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):63-91, 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 formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both data-oriented and process-oriented formal methods.We have built and verified two models of the signature architecture using two representative formal methods. In the first, we specify a data model of the architecture in Z that we extend to a trace model and interactively verify by theorem proving. In the second, we model the architecture as a system of communicating processes that we verify by finite-state model checking. We provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with complex operations on data. Moreover, our comparison highlights the advantages of proving theorems about such models and provides evidence that, in the hands of an experienced user, theorem proving may be neither substantially more time-consuming nor more complex than model checking.

[57] 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 model-driven architecture (MDA) framework that integrates formal analysis techniques into an industrial software development process model. This comprises modeling using UML/OCL, processing models by model transformations, code generation (including runtime-test environments) and formal analysis using the theorem proving environment HOL-OCL. Moreover, our frameworks supports the verification of proof obligations that are generated during model transformations.We show the extensibility of our approach by providing a SecureUML extension of the framework, which allows for an integrated specification of security properties, their analysis and their conversion to code.

[58] 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 long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized, machine-checked semantic basis for a theorem proving environment for OCL (as an example for an object-oriented specification formalism) which is as faithful as possible to the original informal semantics. We report on various (minor) inconsistencies of the OCL semantics, discuss the more recent attempt to align the OCL semantics with UML 2.0 and suggest several extensions which make, in our view, OCL semantics more fit for future extensions towards program verifications and specification refinement.

[59] Achim D. Brucker and Burkhart Wolff. Test-sequence generation with hol-testgen - 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 149-168. Springer-Verlag, Zurich, 2007. [ bib | DOI | http | .ps.gz | .pdf ]
HOL-TestGen is a specification and test-case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs. Although originally designed for black-box unit-tests, HOL-TestGen's underlying logic and deduction engine is powerful enough to be used in test-sequence generation, too. We develop the theory for test-sequence generation with HOL-TestGen and describe its use in a substantial case-study in the field of computer security, namely the black-box test of configured firewalls.

Keywords: security, model-based testing, specification-based testing, firewall testing
[60] 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 351-366. Springer-Verlag, 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 plug-ins, comprising extensible state components and extensible syntax that can be bound to tactical ML programs. Thus the Isabelle/Isar architecture may be understood as an extension and refinement of the traditional "LCF approach", with explicit infrastructure for building derivative systems. To demonstrate the technical potential of the framework, we apply it to a concrete formalmethods tool: the HOL-Z 3.0 environment, which is geared towards the analysis of Z specifications and formal proof of forward-refinements.

[61] Achim D. Brucker and Burkhart Wolff. A package for extensible object-oriented 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 object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, and accessor functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for an object-oriented core-language called , for which correctness of a Hoare logic with respect to an operational semantics is proven.

Keywords: datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding
[62] Achim D. Brucker and Burkhart Wolff. The HOL-OCL Book. Technical Report 525, ETH Zürich, 2006. [ bib | .pdf ]
HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle. HOL-OCL defines a machine-checked formalization of the semantics as described in the standard for OCL 2.0. This conservative, shallow embedding of UML/OCL into Isabelle/HOL includes support for typed, extensible UML data models supporting inheritance and subtyping inside the typed lambda-calculus with parametric polymorphism. As a consequence of conservativity with respect to higher-order logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOL-OCL provides several derived calculi for UML/OCL that allow for formal derivations establishing the validity of UML/OCL formulae. Elementary automated support for such proofs is also provided top

Keywords: security, SecureUML, UML, OCL, HOL-OCL, model-transformation
[63] 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 tool-chain provides support for software modeling using UML/OCL and guides the user from type-checking and model transformations to code generation and formal analysis of the UML/OCL model. We conclude with a report on our experiences in using a functional language for implementing MDA tools.

[64] 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 306-320. Springer-Verlag, 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 front-end visual modeling tools over code-generators to the interactive theorem proving environment . The methodological consequences for an analysis of the generated formulae are discussed.

[65] 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 long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized, machine-checked semantic basis for a theorem proving environment for OCL (as an example for an object-oriented specification formalism) which is as faithful as possible to the original informal semantics. We report on various (minor) inconsistencies of the OCL semantics, discuss the more recent attempt to align the OCL semantics with UML 2.0 and suggest several extensions which make, in our view, OCL semantics more fit for future extensions towards programming-like verifications and specification refinement, which are, in our view, necessary to make OCL more fit for future extensions.

[66] 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.

[67] 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 human-readable mathematical texts. We present an authoring system for formal proof which addresses these concerns. It is based on a central document format which, in the tradition of literate programming, allows one to extract either a formal proof script or a human-readable document; the two may have differing structure and detail levels, but are developed together in a synchronised way. Additionally, we introduce ways to assist production of the central document, by allowing tools to contribute backflow to update and extend it. Our authoring system builds on the new PG Kit architecture for Proof General, bringing the extra advantage that it works in a uniform interface, generically across various interactive theorem provers.

[68] David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff. Specifying and Verifying Hysteresis Signature System with HOL-Z. Technical Report 471, Computer Security Group, ETH Zürich, 1 2005. [ bib | .pdf ]
We report on a case-study in using the data-oriented modeling language Z to formalize a security architecture for administering digital signatures and its architectural security requirements. Within an embedding of Z in the higher-order logic Isabelle/HOL, we provide formal machine-checked proofs of the correctness of the architecture with respect to its requirements. A formalization and verification of the same architecture has been previously carried out using the process-oriented modeling language PROMELA and the SPIN model checker. We use this as a basis for comparing these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking).

[69] David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff. Verification of a Signature Architecture with HOL-Z. In Formal Methods 2005, LNCS 3582, pages 269-285. Springer Verlag, 2005. [ bib | DOI | .pdf ]
We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to specify and verify a security architecture for administering digital signatures. We have used HOL-Z to formalize and combine both data-oriented and process-oriented architectural views. Afterwards, we formalized temporal requirements in Z and carried out verification in higher-order logic. The same architecture has been previously verified using the SPIN model checker. Based on this, we provide a detailed comparison of these two di erent approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with rich data. Moreover, our comparison highlights the advantages of this approach and provides evidence that, in the hands of experienced users, theorem proving is neither substantially more time-consuming nor more complex than model checking.

[70] Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 user guide. Technical Report 482, Computer Security Group, ETH Zürich, apr 2005. [ bib ]
[71] Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Wolfgang Grieskamp and Carsten Weise, editors, Formal Approaches to Testing of Software (FATES 05), LNCS 3997, pages 87-102. Springer-Verlag, Edinburgh, 2005. [ bib | DOI ]
HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant Isabelle/HOL. While there is considerable skepticism with regard to interactive theorem provers in testing communities, we argue that they are a natural choice for (automated) symbolic computations underlying systematic tests. This holds in particular for the development on non-trivial formal test plans of complex software, where some parts of the overall activity require inherently guidance by a test engineer. In this paper, we present the underlying methods for both black box and white box testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit test techniques in a logically consistent way.

[72] 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 16-32. Springer-Verlag, 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 black-box testing of external programs. Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (HCNF). Second, the test cases are analyzed for instances with constant terms satisfying the premises of the clauses. Particular emphasis is put on the control of test hypotheses and test hierarchies to avoid intractability. We applied our method to several examples, including AVL-trees and the red-black tree implementation in the standard library from SML/NJ.

[73] Achim D. Brucker and Burkhart Wolff. A verification approach for applied system security. International Journal on Software Tools for Technology Transfer (STTT), 7(3):233-247, 2005. [ bib | DOI | .pdf ]
We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.

The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.

Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.

[74] Thomas Meyer and Burkhart Wolff. Tactic-based optimized compilation of functional programs. In Jean-Christophe Filliatre, Christine Paulin, and Benjamin Werner, editors, Types for Proofs and Programs (TYPES 2004), LNCS 3839, pages 202-215. Springer Verlag, 8 2005. [ bib | DOI | .pdf ]
Within a framework of correct code-generation from HOLspecifications, we present a particular instance concerned with the optimized compilation of a lazy language (called MiniHaskell) to a strict language (called MiniML). Both languages are defined as shallow embeddings into denotational semantics based on Scott s cpo s, leading to a derivation of the corresponding operational semantics in order to cross-check the basic definitions. On this basis, translation rules from one language to the other were formally derived in Isabelle/HOL. Particular emphasis is put on the optimized compilation of function applications leading to the side-calculi inferring e.g. strictness of functions. The derived rules were grouped and set-up as an instance of our generic, tactic-based translator for specifications to code.

[75] 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 so-called 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 correctness-oriented approach has been known for a while and has been criticized for a number of shortcomings:

    the application range of embeddings in logical frameworks is limited to very small and artificially designed languages, their application is impossible when the formal specification method is still under development,
  1. embedding the semantics conservatively and deriving some rules on this basis does not imply that there is a comprehensive support of a method that is technically powerful enough for applications, the integration in a more global software engineering process and its pragmatics is too difficult, and the usability of embeddings is doubtful even if one is targeting at the (fairly small market of) proof environments.
In contrast to this criticism, we claim that our approach is feasible. We substantiate this by developing:

    suitable embeddings for widely used formal methods, including process-oriented, data-oriented and object-oriented specification methods (CSP, Z, UML/OCL), abstractions and aspect-oriented structuring techniques allowing for the quick development of semantic variants enabling the study consequences of changes in formal methods under development (like UML/OCL), particular techniques for generating library theories, for supporting particular deduction styles in proofs, for specialized deduction support for concrete development methodologies, different scenarios of the integration of the developed tools in conventional tool chains in software engineering, and front-ends for light-weight integration into tool chains (like HOL-Z 2.0) or prototypic encapsulation of logical embeddings into generic graphical user-interfaces for a more comprehensive encapsulation.
Finally, we validate one of these tool chains (HOL-Z 2.0) by a substantial case-study in the field of computer security.

[76] 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 black-box-testing of external programs.

Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (CNF). Second, the test cases are analyzed for ground instances satisfying the premises of the clauses. Particular emphasis is put on the control of test hypothesis' and test hierarchies to avoid intractability.

We applied our method to several examples, including AVL-trees and the red-black implementation in the standard library from SML/NJ.

[77] Nicole Rauch and Burkhart Wolff. Formalizing java's two's-complement integral type in isabelle/hol. Technical Report 458, ETH Zürich, 11 2004. [ bib | www: ]
We present a formal model of Java two’s-complement integral arithmetics. The model directly formalizes the artihmetic operations as given in the Java Language Specification (JLS). The algebraic properties of these definitions are derived. Underspecifications and ambiguities in the JLS are pointed out and clarified. The theory is formally analyzed in Isabelle/HOL that is, machine-checked proofs for the ring properties and divisor/remainder theorems etc. are provided. This work is suited to build the framework for machine-supported reasoning over arithmetic formulae in the context of Java source-code verification.

[78] Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. Journal of Universal Computer Science, 9(2):152-172, 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 structure-preserving, shallow embedding in Isabelle/HOL. On top of the embedding, new proof support for the Z schema calculus and for proof structuring are developed. Thus, we integrate Z into a well-known and trusted theorem prover with advanced deduction technology such as higher-order rewriting, tableaux-based provers and arithmetic decision procedures. A further achievement of this work is the integration of our embedding into a new tool-chain providing a Z-oriented type checker, documentation facilities and macro support for refinement proofs; as a result, the gap has been closed between a logical embedding proven correct and a tool suited for applications of non-trivial size.

[79] David Basin and Burkhart Wolff, editors. Theorem Proving in Higher Order Logics, 16th International Conference (TPHOLs 2003), Rome, Italy, Sep 2003. Springer-Verlag. 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 higher-order logic logic design mathematical logic model checking program verification proof theory theorem provers theorem proving unification

[80] 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. Springer-Verlag, 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 meta-logic, which allows their safe and logically consistent implementation and the reuse of existing theorem prover engines. For being useful, the conservative extension approach must provide derivations for several thousand “folklore” theorems.

In this paper, we present an approach for deriving the mass of these theorems mechanically from an existing library of the meta-logic. The approach presupposes a structured theory morphism mapping library datatypes and library functions to new functions of the specification language while uniformly modifying some semantic properties; for example, new functions may have a different treatment of undefinedness compared to old ones.

[81] 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 CVS-Server architecture performed in [83]. The analysis is based on an abstract architecture (enforcing a role-based access control on the repository), which is refined to an implementation architecture (based on the usual discretionary access control provided by the environment). Both architectures serve as framework to formulate access control and confidentiality properties. Both the abstract as well as the concrete architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for some security properties. Thus, we present a case study for the security analysis of realistic models over an off-the-shelf system by formal machine-checked proofs.

[82] Nicole Rauch and Burkhart Wolff. Formalizing java's two's-complement 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's-complement integral arithmetics. The model directly formalizes the arithmetic operations as given in the Java Language Specification (JLS). The algebraic properties of these definitions are derived. Underspecifications and ambiguities in the JLS are pointed out and clarified. The theory is formally analyzed in Isabelle/HOL, that is, machine-checked proofs for the ring properties and divisor/remainder theorems etc. are provided. This work is suited to build the framework for machine-supported reasoning over arithmetic formulae in the context of Java source-code verification.

[83] Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. The CVS-server case study: A formalized security architecture. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, FM-TOOLS 2002, number 2002-11 in Technical Report, pages 47-52. 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 CVS-server architecture. We present an abstract formal model of the access control aspects of a CVS-server architecture enforcing a role-based access control on the data in the repository. This abstract architecture is refined to an implementation architecture, which represents (an abstraction of) a concrete CVS-server configuration running in a POSIX/UNIX environment. Both the abstract as well as the concrete architecture are specified in the language Z. The specification is compiled to HOL-Z, such that refinement proofs for this case study can be done in Isabelle/HOL.

[84] Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff. HOL-Z 2.0: A proof environment for z-specifications. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, FMTOOLS 2002, number 2002-11 in Technical Report, pages 33-38. Augsburg, July 2002. [ bib | http | .pdf ]
We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a LATEX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus and structural Z proofs.

[85] Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. A CVS-Server security architecture - concepts and formal analysis. Technical Report 182, Albert-Ludwigs-Universität Freiburg, 2002. [ bib | http | .ps.gz | .pdf ]
We present a secure architecture of a CVS-server, its implementation (i.e. mainly its configuration) and its formal analysis. Our CVS-server is uses cvsauth, that provides protection of passwords and protection of some internal data of the CVS repository. In contrast to other (security oriented) CVS-architectures, our approach allows the CVS-server run on an open filesystem, i.e. a filesystem where users can have direct access both by CVS-commands and by standard UNIX/POSIX commands such as mv. For our secure architecture of the CVS-server, we provide a formal specification and security analysys. The latter is based on a refinement mapping high-level security requirements on the architecture on low-level security mechanisms on the UNIX/POSIX filesystem level. The purpose of the formal analysis of the secure CVS-server architecture is twofold: First, it is the bases for the specification of mutual security properties such as non-repudiation, authentication and access control for this architecture. Second, the mapping of the architecture on standard security implementation technology is described. Thus, our approach can be seen as a method to give a formal underpinning for the usually tricky business of system administrators.

Keywords: security architecture, Concurrent Versions System (CVS), Z, formal methods, refinement
[86] Achim D. Brucker and Burkhart Wolff. HOL-OCL: Experiences, consequences and design choices. In Jean-Marc Jézéquel, Heinrich Hussmann, and Stephen Cook, editors, UML 2002: Model Engineering, Concepts and Tools, number 2460 in Lecture Notes in Computer Science. Springer-Verlag, Dresden, 2002. [ bib | DOI | http | .pdf ]
Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [87], we explore several key issues of the design of a formal semantics of the OCL. These issues comprise the question of the interpretation of invariants, pre- and postconditions, their transformation, an executable sub-language and the possibilities of refinement notions. A particular emphasize is put on the issue of mechanized deduction in UML/OCL specification.

Keywords: OCL, Formal semantics, Constraint languages, Refinement, higher-order logic
[87] 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 99-114. Springer-Verlag, 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
[88] 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, Albert-Ludwigs-Universität Freiburg, 2002. [ bib | .pdf ]
[89] 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 608-614, 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 UML-model for a component can be used in a black-box test for the component. Further we introduce different design patterns for EJBs, which are motivated by different levels of abstraction, and show that these patterns work smoothly together with our OCL constraint checking. A prototypic implementation of the code generator, supporting our patterns with OCL support, has been integrated into a commercial software development tool.

[90] Achim D. Brucker and Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Technical Report 157, Albert-Ludwigs-Universitä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 UML-model for a component can be used in a black-box test for the component. Further we introduce different design patterns for EJBs, which are motivated by different levels of abstraction, and show that these patterns work smoothly together with our OCL constraint checking. A prototypic implementation of the code generator, supporting our design patterns with OCL support, has been integrated into a commercial software development tool.

Keywords: OCL, Constraint checking, EJB, J2EE, Design by Contract, Design Pattern, Distributed Systems
[91] Christoph Lüth and Burkhart Wolff. sml_tk: Functional programming for guis - reference manual. Technical Report 158, Albert-Ludwigs-Universität Freiburg, July 2001. [ bib | .pdf ]
In this reference manual, we describe the SML-based programming environment sml_tk for graphical user interfaces, version 3.0. sml_tk is based on the highly portable X-Window Toolkit Tk (and uses internally the Tcl/Tk interpreter wish), but offers functional abstraction over Tk and an own component library for graphical standard widgets such as info-boxes, treelist-widgets, tabs and tables. sml_tk is the basic library for a collection of GUIs for formal method tools such as TAS and IsaWin.

[92] 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 provi-ding support for representing binding mechanisms (based on deBruijn indices), term-schemata and a very clean algebraic theory of substitution. Weprovide a novel binding structure with the following main results: 1) The formalisation of a generic binding structure with the novel conceptof effect-binding that enables the explicit representations of both contexts and terms inside one term meta-language,2) The foundation of a formal (machine-assisted) substitution theory of effect-binding that is well-suited for mechanisation. This can be used for thesystematic and correct development of new calculi with explicit substitutions.The substitution theory is formally proven in Isabelle/HOL; the implementation may serve as (untyped) framework for deep embeddings.

[93] T. Meyer and Burkhart Wolff. Correct code-generation in a generic framework. In M. Aargaard, J. Harrison, and T. Schubert, editors, TPHOLs 2000: Supplemental Proceedings, OGI Technical Report CSE 00-009, pages 213-230. 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 well-founded recursion) and develop their theory in Isabelle/HOL. These theories serve as a semantic interface for a generic code-generator which is set up for each program notion with an individual code-scheme for SML.

[94] 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):248-249, 2000. [ bib | .ps.gz | .pdf ]
[95] 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.

[96] 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 405-422. 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 command-language-free user interaction by gestures like drag&drop and proof-by-pointing, 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.

[97] 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 LCF-style prover design, and a methodology for the implementation of graphical user interfaces for these provers and encapsulations of formal methods. In this problem domain, particular attention has to be paid to the need to construct a variety of objects, keep track of their interdependencies and provide support for their reconstruction as a consequence of changes. We present a prototypical implementation of a <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.

[98] Chritoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, and Burkhart Wolff. HOL-Z in the UniForM-Workbench - a case study in tool integration for z. In J. Bowen, editor, 11. International Conference of Z Users ZUM'98, LNCS 1493, pages 116-134. Springer Verlag, 1998. [ bib | DOI | .ps.gz ]
The UniForM-Workbench is an open tool-integration environment providing type-safe communication, a toolkit for graphical user-interfaces, version management and configuration management. We demonstrate how to integrate several tools for the Z specification language into the workbench, obtaining an instantiation of the workbench suited as a software development environment for Z. In the core of the setting, we use the encoding HOL-Z of Z into Isabelle as semantic foundation and for formal reasoning with Z specifications. In addition to this, external tools like editors and small utilities are integrated, showing the integration of both self-developed and externally developed tools. The resulting prototype demonstrates the viability of our approach to combine public domain tools into a generic software development environment using a strongly typed functional language.

[99] 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 UniForM-Workbench is an open tool-integration environment providing type-safe communication, a toolkit for graphical user-interfaces, version management and configuration management. We demonstrate how to integrate several tools for the Z specification language into the workbench, obtaining an instantiation of the workbench suited as a software development environment for Z. In the core of the setting, we use the encoding HOL-Z of Z into Isabelle as semantic foundation and for formal reasoning with Z specifications. In addition to this, external tools like editors and small utilities are integrated, showing the integration of both self-developed and externally developed tools. The resulting prototype demonstrates the viability of our approach to combine public domain tools into a generic software development environment using a strongly typed functional language.

[100] Haykal Tej, Christoph Lüth, and Burkhart Wolff. Generic transformational program development. Unpublished Paper., 1998. [ bib | .pdf ]
[101] 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 855-858. Springer Verlag, 1997. [ bib | DOI | .ps.gz ]
[102] 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 ]
[103] H. Tej and B. Wolff. A corrected failure-divergence 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 318-337. Springer Verlag, 1997. [ bib | DOI | .ps.gz | .pdf ]
We present a failure-divergence model for CSP following the concepts of [BR 85]. Its formal representation within higher order logic in the theorem prover Isabelle/HOL [Pau 94] revealed an error in the basic definition of CSP concerning the treatment of the termination symbol tick. A corrected model has been formally proven consistent with Isabelle HOL. Moreover, the changed version maintains the essential algebraic properties of CSP. As a result, there is a proven correct implementation of a “CSP workbench'' within Isabelle.

[104] 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), term-schemata and a very clean algebraic theory of substitution. We provide the following main results:

    The establishment of a generic binding structure with the novel concept of effect-binding that enables the representations of both signatures and formulas (i.e. specifications) inside one term meta- language, The foundation of a formal (machine-assisted) substitution theory of effect-binding that is well-suited for mechanisation. This may contribute to the construction of tools such as theorem provers, program transformers, static analysers, evaluators and optimising compilers, The foundation of a rigorous meta-theory for rewriting on effect- binding-structures. The resulting rewrite notion transformation extends combinatory rewrite systems to rewrites on specifications.
The corner stone of this theory is a confluence proof for orthogonal transformations (partly implemented in the proof assistant Isabelle).

[105] Kolyang, C. Lüth, T. Meier, and B. Wolff. Generating graphical user-interfaces 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 ]
[106] Kolyang, T. Santen, and B. Wolff. Correct and user-friendly implementation of transformation systems. In M.-C. Gaudel and J. Woodcock, editors, FME 96 - Industrial Benefits and Advances in Formal Methods, LNCS 1051, pages 629-648. 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 user-friendly way. We illustrate the approach by proving and implementing the transformation Global Search on the basis of the tactical theorem prover Isabelle. A graphical user-interface based on the X-Window toolkit Tk provides user friendly access to the underlying machinery.

[107] 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 283-298. Springer Verlag, 1996. [ bib | .ps.gz | .pdf ]
We present a semantic representation of the core concepts of the specification language Z in higher-order logic. Although it is a “shallow embedding'' like the one presented by Bowen and Gordon, our representation preserves the structure of a Z specification and avoids expanding Z schemas. The representation is implemented in the higher- order logic instance of the generic theorem prover Isabelle. Its parser can convert the concrete syntax of Z schemas into their semantic representation and thus spare users from having to deal with the representation explicitly. Our representation essentially conforms with the latest draft of the Z standard and may give both a clearer understanding of Z schemas and inspire the development of proof calculi for Z.

[108] 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 ]
[109] B. Krieg-Brückner, J. Liu, H. Shi, and B. Wolff. Towards correct, efficient and re-usable transformational developments. In M. Broy and S. Jähnichen, editors, KORSO - Methods, Languages, and Tools for the Construction of Correct Software, LNCS 1009, pages 270-284. Springer Verlag, 1995. [ bib | .ps.gz ]
[110] Kolyang and B. Wolff. Development by refinement revisited: Lessons learnt from an example. In G. Snelting, editor, Beiträge der GI-Fachtagung “Softwaretechnik 95'', Braunschweig, Mitteilungen der Fachgruppen `Software Engineering' und `Requirements-Engineering',Band 15, Heft 3, ISSN 0720-8928, pages 57-66. GI, 1995. [ bib | .ps.gz ]

This file was generated by bibtex2html 1.96.