Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
- 2006 (7) (remove)
Document Type
- Report (5)
- Doctoral Thesis (1)
- Preprint (1)
Language
- English (7) (remove)
Has Fulltext
- yes (7)
Keywords
- Certifying Compilers (1)
- Extraction (1)
- Formal Semantics (1)
- Formalisierung (1)
- OCL 2.0 (1)
- Profiles (1)
- SDL (1)
- SDL-2000 (1)
- Sprachprofile (1)
- Translation Validation (1)
Faculty / Organisational entity
A translation contract is a binary predicate corrTransl(S,T) for source programs S and target programs T. It precisely specifies when T is considered to be a correct translation of S. A certifying compiler generates --in addittion to the target T-- a proof for corrTransl(S,T). Certifying compilers are important for the development of safety critical systems to establish the behavioral equivalence of high-level programs with their compiled assembler code. In this paper, we report on a certifying compiler, its proof techniques, and the underlying formal framework developed within the proof assistent Isabelle/HOL. The compiler uses a tiny C-like language as input, has an optimization phase, and generates MIPS code. The underlying translation contract is based on a trace semantics. We investigate design alternatives and discuss our experiences.
The validity of formulas w.r.t. a specification over first-order logic with a semantics based on all models is semi-decidable. Therefore, we may implement a proof procedure which finds a proof for every valid formula fully automatically. But this semantics often lacks intuition: Some pathological models such as the trivial model may produce unexpected results w.r.t. validity. Instead, we may consider just a class of special models, for instance, the class of all data models. Proofs are then performed using induction. But, inductive validity is not semi-decidable -- even for first-order logic. This theoretical drawback manifests itself in practical limitations: There are theorems that cannot be proved by induction directly but only generalizations can be proved. For their definition, we may have to extend the specification. Therefore, we cannot expect to prove interesting theorems fully automatically. Instead, we have to support user-interaction in a suitable way. In this thesis, we aim at developing techniques that enhance automatic proof control of (inductive) theorem provers and that enable user-interaction in a suitable way. We integrate our new proof techniques into the inductive theorem prover QuodLibet and validate them with various case studies. Essentially, we introduce the following three proof techniques: -We integrate a decision procedure for linear arithmetic into QuodLibet in a close way by defining new inference rules that perform the elementary steps of the decision procedure. This allows us to implement well-known heuristics for automatic proof control. Furthermore, we are able to provide special purpose tactics that support the manual speculation of lemmas if a proof attempt gets stuck. The integration improves the ability of the theorem prover to prove theorems automatically as well as its efficiency. Our approach is competitive with other approaches regarding efficiency; it provides advantages regarding the speculation of lemmas. -The automatic proof control searches for a proof by applying inference rules. The search space is not only infinite, but grows dramatically with the depth of the search. In contrast to this, checking and analyzing performed proofs is very efficient. As the search space also has a high redundancy, it is reasonable to reuse subproofs found during proof search. We define new notions for the contribution of proof steps to a proof. These notions enable the derivation of pruned proofs and the identification of superfluous subformulas in theorems. A proof may be reused in two ways: upward propagation prunes a proof by eliminating superfluous proof steps; sideward reuse closes an open proof obligation by replaying an already found proof. -For interactive theorem provers, it is essential not only to prove automatically as many lemmas as possible but also to restrict proof search in such a way that the proof process stops within a reasonable amount of time. We introduce different markings in the goals to be proved and the lemmas to be applied to restrict proof search in a flexible way: With a forbidden marking, we can simulate well-known approaches for applying conditional lemmas. A mandatory marking provides a new heuristics which is inspired by local contribution of proof steps. With obligatory and generous markings, we can fine-tune the degree of efficiency and extent of proof search manually. With an elaborate case study, we show the benefits of the different techniques, in particular the synergetic effect of their combination.
With the UML 2.0 standard, the Unified Modeling Language took a big step towards SDL, incorporating many features of the language. SDL is a mature and complete language with formal semantics. The Z.109 standard defines a UML Profile for SDL, mapping UML constructs to corresponding counterparts in SDL, giving them a precise semantics. In this report, we present a case study for the formalisation of the Z.109 standard. The formal definition makes the mapping precise and can be used to derive tool support.
Web-based authentication is a popular mechanism implemented by Wireless Internet Service Providers (WISPs) because it allows a simple registration and authentication of customers, while avoiding the high resource requirements of the new IEEE 802.11i security standard and the backward compatibility issues of legacy devices. In this work we demonstrate two different and novel attacks against web-based authentication. One attack exploits operational anomalies of low- and middle-priced devices in order to hijack wireless clients, while the other exploits an already known vulnerability within wired-networks, which in dynamic wireless environments turns out to be even harder to detect and protect against.
Katja is a tool generating order-sorted recursive data types as well as position types for Java, from specifications using an enhanced ML like notation. Katja’s main features are its conciseness of specifications, the rich interface provided by the generated code and the Java atypical immutability of types. After several stages of extending and maintaining the Katja project, it became apparent many changes had to be done. The original design of Katja wasn’t prepared for the introduction of several backends, the introduction of position sorts and constant feature enhancements and bug fixes. By supplying this report Katja reaches release status for the first time.
Over a period of 30 years, ITU-T’s Specification and Description Language (SDL) has matured to a sophisticated formal modelling language for distributed systems and communication protocols. The language definition of SDL-2000, the latest version of SDL, is complex and difficult to maintain. Full tool support for SDL is costly to implement. Therefore, only subsets of SDL are currently supported by tools. These SDL subsets - called SDL profiles - already cover a wide range of systems, and are often suffcient in practice. In this report, we present our approach for extracting the formal semantics for SDL profiles from the complete SDL semantics. We then formalise the approach, present our SDL-profile tool, and report on our experiences.
Ownership Domains generalize ownership types. They support programming patterns like iterators that are not possible with ordinary ownership types. However, they are still too restrictive for cases in which an object X wants to access the public domains of an arbitrary number of other objects, which often happens in observer scenarios. To overcome this restriction, we developed so-called loose domains which abstract over several precise domains. That is, similar to the relation between supertypes and subtypes we have a relation between loose and precise domains. In addition, we simplified ownership domains by reducing the number of domains per object to two and hard-wiring the access permissions between domains. We formalized the resulting type system for an OO core language and proved type soundness and a fundamental accessibility property.