Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2006 | Book

Verifying a Hotel Key Card System Read chapter Read first chapter

Theoretical Aspects of Computing - ICTAC 2006

Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings

Editors: Kamel Barkaoui, Ana Cavalcanti, Antonio Cerone

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

The International Colloquium on Theoretical Aspects of Computing (ICTAC) held in 2006 in Tunis, Tunisia, was the third of a series of events created by the InternationalInstituteforSoftwareTechnologyoftheUnitedNationsUniversity. The aim of the colloquium is to bring together researchers from academia, - dustry, and governmentto present their results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. The previous events were held in Guiyang, China (2004), and Hanoi, Vi- nam (2005). Beyond its scholarly goals, another main purpose of ICTAC is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries, as in the mandate of the United Nations University. These proceedings record the contributions from the invited speakers and from the technical sessions. We present four invited papers, 21 technical papers, selected out of 78 submissions from 24 countries, and two extended abstracts of tutorials. The Programme Committee includes researchers from 27 countries. Each of the 78 papers was evaluated by at least three reviewers. After the evaluation, reports were returned to the Programme Committee for discussion and reso- tion of con?icts. Based on their recommendations, we concluded the consensus process, and selected the 21 papers that we present here. For the evaluation of the submitted tutorials, this year we had the help of a separate Programme Committee especially invited for that purpose.

Table of Contents

Frontmatter

Invited Papers

Verifying a Hotel Key Card System
Abstract
Two models of an electronic hotel key card system are contrasted: a state based and a trace based one. Both are defined, verified, and proved equivalent in the theorem prover Isabelle/HOL. It is shown that if a guest follows a certain safety policy regarding her key cards, she can be sure that nobody but her can enter her room.
Tobias Nipkow
Z/Eves and the Mondex Electronic Purse
Abstract
We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original \({\sc L^{A}T_{E}X}\) sources, without changing their technical content, except to correct errors: we found problems in the original texts and missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the research objectives of building the Repository for the Verified Software Grand Challenge.
Jim Woodcock, Leo Freitas
Verification Constraint Problems with Strengthening
Abstract
The deductive method reduces verification of safety properties of programs to, first, proposing inductive assertions and, second, proving the validity of the resulting set of first-order verification conditions. We discuss the transition from verification conditions to verification constraints that occurs when the deductive method is applied to parameterized assertions instead of fixed expressions (e.g., p 0 + p 1 j + p 2 k ≥0, for parameters p 0, p 1, and p 2, instead of 3 + j – k ≥0) in order to discover inductive assertions. We then introduce two new verification constraint forms that enable the incremental and property-directed construction of inductive assertions. We describe an iterative method for solving the resulting constraint problems. The main advantage of this approach is that it uses off-the-shelf constraint solvers and thus directly benefits from progress in constraint solving.
Aaron R. Bradley, Zohar Manna

Semantics

Quantitative μ-Calculus Analysis of Power Management in Wireless Networks
Abstract
An important concern in wireless network technology is battery conservation. A promising approach to saving energy is to allow nodes periodically to enter a “low power mode”, however this strategy contributes to message delay, and careful management is required so that the system-wide performance is not severely compromised.
In this paper we show how to manage power schedules using the quantitative modal μ-calculus which allows the specification of a quantitative performance property as a game in which a maximising player’s optimal strategy corresponds to optimising overall performance relative to the specified property.
We extend the standard results on discounted games to a class of infinite state systems, and illustrate our results on a small case study.
A. K. McIver
Termination and Divergence Are Undecidable Under a Maximum Progress Multi-step Semantics for LinCa
Abstract
We introduce a multi-step semantics MTS-mp for LinCa which demands maximum progress in each step, i.e. which will only allow transitions that are labeled with maximal (in terms of set inclusion) subsets of the set of enabled actions. We compare MTS-mp with the original ITS-semantics for LinCa specified in [CJY94] and with a slight modification of the original MTS-semantics specified in [CJY94]. Given a LinCa-process and a Tuple Space configuration, the possible transitions under our MTS-mp-semantics are always a subset of the possible transitions under the presented MTS-semantics for LinCa.
We compare the original ITS-semantics and the presented MTS-semantics with our MTS-mp-semantics, and as a major result, we will show that under MTS-mp neither termination nor divergence of LinCa processes is decidable. In contrast to this [BGLZ04], in the original semantics for LLinCa [CJY94] termination is decidable.
Mila Majster-Cederbaum, Christoph Minnameier
A Topological Approach of the Web Classification
Abstract
In this paper we study some topological aspects related to the important operations of searching and classification over the Web. Classification is dictated by some criteria, and these criteria can be defined as a classification operator. An interesting problem is to prove the existence of a stable classification with respect to a certain operator. In this context we provide a topological approach to describe the structure of the web based on the trips given by the links of the web documents, and present various topologies defined over the Web. Some results regarding the topological properties as connectivity, density and separation are presented. The Alexandrov topology plays a particular role, and we have a certain equivalence between this topology and the classification process.
Gabriel Ciobanu, Dănuţ Rusu

Concurrency

Bisimulation Congruences in the Calculus of Looping Sequences
Abstract
The Calculus of Looping Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and composing them by means of operators of concatenation, looping, containment and parallel composition. CLS terms can be transformed by applying rewrite rules. We give a labeled transition semantics for CLS by using, as labels, contexts in which rules can be applied. We define bisimulation relations that are congruences with respect to the operators on terms, and we show an application of CLS to the modeling of a biological system and we use bisimulations to reason about properties of the described system.
Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, Angelo Troina
Stronger Reduction Criteria for Local First Search
Abstract
Local First Search (LFS) is a partial order technique for reducing the number of states to be explored when trying to decide reachability of a local (component) property in a parallel system; it is based on an analysis of the structure of the partial orders of executions in such systems. Intuitively, LFS is based on a criterion that allows to guide the search for such local properties by limiting the “concurrent progress” of components.
In this paper, we elaborate the analysis of the partial orders in question and obtain related but significantly stronger criteria for reductions, show their relation to the previously established criterion, and discuss the algorithmics of the proposed improvement. Our contribution is both fundamental in providing better insights into LFS and practical in providing an improvement of high potential, as is illustrated by experimental results.
Marcos E. Kurbán, Peter Niebert, Hongyang Qu, Walter Vogler
A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes
Abstract
We present a new lattice-theoretic model for communicating sequential processes. The model underpins a process algebra that is very close to CSP. It differs from CSP “at the edges” for the purposes of creating an elegant algebra of communicating processes. The one significant difference is that we postulate additional distributive properties for external choice. The shape of the algebra that emerges suggests a lattice-theoretic model, in contrast to traditional trace-theoretic models. We show how to build the new model in a mathematically clean step-by-step process. The essence of our approach is to model simple processes (i.e. those without choice, parallelism, or recursion) as a poset S of sequences, and then order-embed S into a complete (and completely distributive) lattice called the free completely distributive lattice over S. We explain the technique in detail and show that the resulting model does indeed capture our algebra of communicating sequential processes. The focus of the paper is not on the algebra per se, but on the model and the soundness of the algebra.
Malcolm Tyrrell, Joseph M. Morris, Andrew Butterfield, Arthur Hughes
A Petri Net Translation of π-Calculus Terms
Abstract
In this paper, we propose a finite structural translation of possibly recursive π-calculus terms into Petri nets. This is achieved by using high level nets together with an equivalence on markings in order to model entering into recursive calls, which do not need to be guarded.
Raymond Devillers, Hanna Klaudel, Maciej Koutny

Model Checking

Handling Algebraic Properties in Automatic Analysis of Security Protocols
Abstract
In this paper we extend the approximation based theoretical framework in which the security problem – secrecy preservation against an intruder – may be semi-decided through a reachability verification.
We explain how to cope with algebraic properties for an automatic approximation-based analysis of security protocols. We prove that if the initial knowledge of the intruder is a regular tree language, then the security problem may by semi-decided for protocols using cryptographic primitives with algebraic properties. More precisely, an automatically generated approximation function enables us 1) an automatic normalization of transitions, and 2) an automatic completion procedure. The main advantage of our approach is that the approximation function makes it possible to verify security protocols with an arbitrary number of sessions.
The concepts are illustrated on an example of the view-only protocol using a cryptographic primitive with the exclusive or algebraic property.
Y. Boichut, P. -C. Héam, O. Kouchnarenko
A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems
Abstract
The reachability problem as well as the computation of the phase portrait for the class of planar hybrid systems defined by constant differential inclusions (SPDI), has been shown to be decidable. The existing reachability algorithm is based on the exploitation of topological properties of the plane which are used to accelerate certain kind of cycles. The complexity of the algorithm makes the analysis of large systems generally unfeasible. In this paper we present a compositional parallel algorithm for reachability analysis of SPDIs. The parallelization is based on the qualitative information obtained from the phase portrait of an SPDI, in particular the controllability kernel.
Gordon Pace, Gerardo Schneider
Thread-Modular Verification Is Cartesian Abstract Interpretation
Abstract
Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of over-approximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, our result provides a characterization of a minimal increase in the precision of the Flanagan and Qadeer algorithm that leads to the loss of its polynomial complexity.
Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Formal Languages

Capture-Avoiding Substitution as a Nominal Algebra
Abstract
Substitution is fundamental to computer science, underlying for example quantifiers in predicate logic and beta-reduction in the lambda-calculus. So is substitution something we define on syntax on a case-by-case basis, or can we turn the idea of ‘substitution’ into a mathematical object?
We exploit the new framework of Nominal Algebra to axiomatise substitution. We prove our axioms sound and complete with respect to a canonical model; this turns out to be quite hard, involving subtle use of results of rewriting and algebra.
Murdoch J. Gabbay, Aad Mathijssen
Prime Decomposition Problem for Several Kinds of Regular Codes
Abstract
Given a class C of codes. A regular code in C is called prime if it cannot be decomposed as a catenation of at least two non-trivial regular codes in C. The prime decomposition problem for the class C of codes consists in decomposing regular codes in C into prime factors in C. In this paper, a general approach to this problem is proposed, by means of which solutions for the prime decomposition problem are obtained, in a unified way, for several classes of codes. These classes are all subclasses of prefix codes and can be defined by binary relations.
Kieu Van Hung, Do Long Van
A New Approach to Determinisation Using Bit-Parallelism
Abstract
We present a new approach to the determinisation process of specified types of automata using bit-parallel algorithms. We present the determinisation of nondeterministic pattern matching automata (PMA) for approximate pattern matching and we introduce the determinisation of suffix automata. This new approach speeds the determinisation up to m times, where m is the length of the pattern searched by PMA, or accepted by the suffix automaton, respectively.
Jan Šupol, Bořivoj Melichar

Logic and Type Theory

Proving ATL* Properties of Infinite-State Systems
Abstract
Alternating temporal logic (atl*) was introduced to prove properties of multi-agent systems in which the agents have different objectives and may collaborate to achieve them. Examples include (distributed) controlled systems, security protocols, and contract-signing protocols. Proving atl* properties over finite-state systems was shown decidable by Alur et al., and a model checker for the sublanguage atl implemented in mocha.
In this paper we present a sound and complete proof system for proving alt* properties over infinite-state systems. The proof system reduces proofs of alt* properties over systems to first-order verification conditions in the underlying assertion language. The verification conditions make use of predicate transformers that depend on the system structure, so that proofs over systems with a simpler structure, e.g., turn-based systems, directly result in simpler verification conditions. We illustrate the use of the proof system on a small example.
Matteo Slanina, Henny B. Sipma, Zohar Manna
Type Safety for FJ and FGJ
Abstract
Mainly concerned with type safety, Featherweight Java, or FJ, is a well known minimal core for Java and Generic Java. However, in the type system of FJ, the treatment of downcast is omitted. In this paper we propose a stronger type system for FJ and FGJ. In order to deal with the cast problems, we introduce some special techniques for types, and also strengthen the types for expressions and methods in terms of the type declaration notations. Supported by the type system and our techniques, we can ensure properties stronger than the ones proved in Igarashi et al’s original FJ paper. Examples making the above mentioned contributions clear are illustrated throughout this paper. Furthermore a case study on design patterns showing the advantages of our results is given.
Shuling Wang, Quan Long, Zongyan Qiu
Partizan Games in Isabelle/HOLZF
Abstract
Partizan Games (PGs) were invented by John H. Conway and are described in his book On Numbers and Games. We formalize PGs in Higher Order Logic extended with ZF axioms (HOLZF) using Isabelle, a mechanical proof assistant. We show that PGs can be defined as the unique fixpoint of a function that arises naturally from Conway’s original definition. While the construction of PGs in HOLZF relies heavily on the ZF axioms, operations on PGs are defined on a game type that hides its set theoretic origins. A polymorphic type of sets that are not bigger than ZF sets facilitates this. We formalize the induction principle that Conway uses throughout his proofs about games, and prove its correctness. For these purposes we examine how the notions of well-foundedness in HOL and ZF are related in HOLZF. Finally, games (modulo equality) are added to Isabelle’s numeric types by showing that they are an instance of the axiomatic type class of partially ordered abelian groups.
Steven Obua
Proof-Producing Program Analysis
Abstract
Proof-producing program analysis augments the invariants inferred by an abstract interpreter with their correctness proofs. If these invariants are precise enough to guarantee safety, this method is an automatic verification tool. We present proof-synthesis algorithms for a simple flow chart language and domains \({\mathcal{V}}\to{\mathbb{V}}\) mapping variables to abstract values and discuss some benefits for proof carrying code systems. Our work has been carried out in Isabelle/HOL and incorporated within a verified proof carrying code system.
Amine Chaieb

Real-Time and Mobility

Reachability Analysis of Mobile Ambients in Fragments of AC Term Rewriting
Abstract
In this paper we investigate the connection between fragments of associative-commutative Term Rewriting and fragments of Mobile Ambients, a powerful model for mobile and distributed computations. The connection can be used to transfer decidability and undecidability results for important computational properties like reachability from one formalism to the other. Furthermore, it can be viewed as a vehicle to apply tools based on rewriting for the simulation and validation of specifications given in Mobile Ambients.
Giorgio Delzanno, Roberto Montagna
Interesting Properties of the Real-Time Conformance Relation tioco
Abstract
We are interested in black-box conformance testing of real-time systems. Our framework is based on the model of timed automata with inputs and outputs (TAIO). We use a timed conformance relation called tioco which is the extension of the untimed relation ioco. We show that considering only lazy-input TAIO is enough for describing all possible non-blocking specifications. We compare between tioco and the trace-inclusion relation. We prove that tioco is undecidable and that it does not distinguish specifications with the same set of observable traces. We prove tioco to be transitive and stable w.r.t both compositionality and action hiding for input-complete specifications. We compare between tioco and two other timed conformance relations, rtioco and \( \sqsubseteq_{\mathsf{\it tioco}}\).
Moez Krichen, Stavros Tripakis
Model Checking Duration Calculus: A Practical Approach
Abstract
Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS).
Roland Meyer, Johannes Faber, Andrey Rybalchenko
Spatio-temporal Model Checking for Mobile Real-Time Systems
Abstract
This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. We provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study “generalised railroad crossing” (GRC) enriched by requirements inexpressible in non-spatial formalisms.
Jan-David Quesel, Andreas Schäfer

Tutorials: Extended Abstracts

Tutorial on Formal Methods for Distributed and Cooperative Systems
Abstract
This tutorial is proposed by representatives of the MeFoSyLoMa group. MeFoSyLoMa is an informal group gathering several teams from various universities in the Paris area:
– Université Paris-Dauphine (LAMSADE laboratory),
– Université P. & M. Curie (LIP6 laboratory),
– Université Paris 13 (LIPN laboratory),
– ENST (LTCI laboratory),
– Conservatoire National des Arts et Métiers (CEDRIC laboratory).
These teams have extensive knowledge and experience in the design, analysis and implementation of distributed systems. The cooperation within the group aims at joining forces, sharing experiences and building joint projects to solve issues in the design of reliable distributed systems.
Christine Choppy, Serge Haddad, Hanna Klaudel, Fabrice Kordon, Laure Petrucci, Yann Thierry-Mieg
Decision Procedures for the Formal Analysis of Software
Abstract
Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.
David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
Backmatter
Metadata
Title
Theoretical Aspects of Computing - ICTAC 2006
Editors
Kamel Barkaoui
Ana Cavalcanti
Antonio Cerone
Copyright Year
2006
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-48816-3
Print ISBN
978-3-540-48815-6
DOI
https://doi.org/10.1007/11921240

Premium Partner

    Image Credits