Catálogo de publicaciones - libros

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.

We describe our experiences in mechanising the specification, refinement, and proof of the using the Z/Eves theorem prover. We took a conservative approach and mechanised the original 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.

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 to that occurs when the deductive method is applied to parameterized assertions instead of fixed expressions (, + + ≥0, for parameters , , and , instead of 3 + – ≥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.

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.

We introduce a multi-step semantics for which demands 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 with the original -semantics for LinCa specified in [CJY94] and with a slight modification of the original -semantics specified in [CJY94]. Given a -process and a configuration, the possible transitions under our -semantics are always a subset of the possible transitions under the presented -semantics for .

We compare the original -semantics and the presented -semantics with our --semantics, and as a major result, we will show that under - neither termination nor divergence of processes is decidable. In contrast to this [BGLZ04], in the original semantics for LinCa [CJY94] termination is decidable.

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.

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.

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.

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 of sequences, and then order-embed into a complete (and completely distributive) lattice called the over . 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.

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.