Modelling and Analysing Cyber-Physical Systems (CPS) is a challenge for Formal Methods and therefore a field of active research. It is characteristic of CPSs that models comprise aspects of Newtonian Physics appearing in system environments, the difficulties of their discretization, the problems of communication and interaction between actors in this environment as well as calculations respecting time-bounds. We present a novel framework to address these problems developed with industrial partners involved in the Autonomous Car domain. Based on HOL-CSP, we model time, physical evolution, "scenes” (global states) and "scenarios" (traces) as well as the interaction of "actors" (vehicles, pedestrians, traffic lights) inside this framework. In particular, discrete samplings are modelled by infinite internal choices. For several instances of the modelling framework, we give formal proofs of a particular safety property for Autonomous Cars: if each car follows the same driving strategy defined by the so-called Responsibility-Sensitive Safety (RSS), no collision will occur. The proofs give rise to a number of variants of RSS and optimizations as well as a test-case partitioning of abstract test cases and a test-strategy for integration tests.

Keywords: Cyber–Physical Systems, Autonomous cars, Safety-critical systems, Process-algebra, Concurrency, Proof-based verification

Keywords: Process-Algebra, Concurrency, Computational Models, Parametric System Verification

A common problem in the certification of highly safety or security critical systems is the consistency of the certification documentation in general and, in particular, the linking between semi-formal and formal content of the certification documentation. We address this problem by using an existing framework, Isabelle/DOF, that allows writing certification documents with consistency guarantees, in both, the semi-formal and formal parts. Isabelle/DOF supports the modeling of document ontologies using a strongly typed ontology definition language. An ontology is then enforced inside documents including formal parts, e.g., system models, verification proofs, code, tests and validations of corner-cases. The entire set of documents is checked within Isabelle/HOL, which includes the definition of ontologies and the editing of integrated documents based on them. This process is supported by an IDE that provides continuous checking of the document consistency. In this paper, we present how a specific software-engineering certification standard, namely CENELEC 50128, can be modeled inside Isabelle/DOF. Based on an ontology covering a substantial part of this standard, we present how Isabelle/DOF can be applied to a certification case-study in the railway domain.

Keywords: Certification of Safety-Critical Systems, CENELEC 50128, Formal Document Development, Isabelle/DOF, Isabelle/HOL

We present a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE devel- opment environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or white- box testing can be applied to the same source, which is part of an integrated PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for framing conditions.

Our framework supports semantic annotations of C sources in the form of comments. Annota- tions serve to locally control back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables. Our approach demonstrates the degree of maturity and expressive power the Isabelle/PIDE sub-system has achieved in recent years. Our integration technique employs Lex and Yacc style grammars to ensure efficient deterministic parsing. We present two case studies for the integration of (known) semantic back-ends in order to validate the design decisions for our back-end interface.

Keywords: Isabelle, HOL, C11, Program Verification, Program Testing

DOF is a novel framework for defining ontologies and enforcing them during document development and document evolution. A major goal of DOF is the integrated development of formal certification documents (, for Common Criteria or CENELEC 50128) that require consistency across both formal and informal arguments.

To support a consistent development of formal and informal parts of a document, we provide Isabelle/DOF, an implementation of DOF on top of Isabelle/HOL. is integrated into Isabelle's IDE, which allows for smooth ontology development as well as immediate ontological feedback during the editing of a document.

In this paper, we give an in-depth presentation of the design concepts of DOF's Ontology Definition Language (ODL) and key aspects of the technology of its implementation. is the first ontology language supporting machine-checked links between the formal and informal parts in an LCF-style interactive theorem proving environment.

Sufficiently annotated, large documents can easily be developed collaboratively, while ensuring their consistency, and the impact of changes (in the formal and the semi-formal content) is tracked automatically.

Keywords: Isabelle, HOL, Ontologies, Certification

While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation.

Up to now, Isabelle's document preparation system lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.

In this paper, we present Isabelle/DOF, a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for conventional typesetting as well as formal development. We show how to model document ontologies inside Isabelle/DOF, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support.

Keywords: Isabelle/Isar, HOL, Ontologies

We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an “agile development” in terms of evolutionary flexibility and continuous improvement. Yet, it enforces the overall coherence of the development artifacts (ranging from proofs over tests to code) by a particular environment (CVCE). In particular, the validation process is built around a formal development based on the interactive theorem proving system Isabelle/HOL, by linking the business logic of the application to the operating system model, down to code and concrete hardware models thanks to a series of refinement proofs. We apply both the process and its support in CVCE to a case-study that comprises a model of an odometric service in a railway-system with its corresponding implementation integrated in seL4 (a secure kernel for which a comprehensive Isabelle development exists). Novel techniques implemented in Isabelle enforce the coherence of semi-formal and formal definitions within to specific certification processes in order to improve their cost-effectiveness.

Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL

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.

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.

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.

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.

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.

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

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.

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

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

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.

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

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

/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

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.

Keywords: symbolic test case generations, black box testing, theorem proving, Isabelle/HOL

Keywords: HOL-OCL, OCL, formal semantics

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.

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.

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

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.

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.

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.

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

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

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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

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

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.

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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

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.

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.

We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a L^AT_EX-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.

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

Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic [120], 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

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

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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).

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.

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.