Fundamenta Informaticae

Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct.

We introduce Nuovo DRM, a digital rights management scheme aimed to provide formal and practical security. The scheme is based on a recent DRM scheme, which we formally specify in the ?CRL process algebraic language. The original scheme stated the following security requirements: effectiveness, secrecy and resistance of content masquerading. We formalise these security requirements as well as strong fairness and formally check the original scheme against these requirements. This verification step uncovered several security weaknesses, which are addressed by Nuovo DRM. In addition to that, Nuovo DRM introduces several procedural practices to enhance the practical security of the scheme. A finite model of Nuovo DRM is subsequently model-checked and shown to satisfy its design requirements, including secrecy, fairness and resistance to content masquerading.

This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if ε-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.

In the context of Service Oriented Computing, contracts are descriptions of the observable message-passing behavior of services. Contracts have been already successfully exploited to solve the problem of client/service composition. Inspired by current orchestration languages, we consider services where the choice to perform an output may not depend on the environment. Under this assumption, we propose a new theory of contracts which also addresses the problem of composition of multiple services (not only one client with one service). Moreover, we relate our theory of contracts with the theory of must testing pre-order (interpreted as a subcontract relation) and we show that a compliant group of contracts is still compliant if every contract is replaced by one of its subcontracts.

Web services are emerging as a promising technology for the development of next generation distributed heterogeneous software systems.We define a new behavioural equivalence forWeb services, based on bisimilarity and inspired by recent advances in the theory of reactive systems. The equivalence is compositional and decidable, and it provides a firm ground for enhanced behaviouraware discovery and for a sound incremental development of services and service compositions.

Policies are used to describe rules that are employed to modify (often distributed) system behaviour at runtime. Typically policies are created by many different people and there are many policies leading naturally to inconsistency between the policies, a problem that has been recognised and termed policy conflict. We present a novel formal semantics for distributed policies expressed in the APPEL language (so far APPEL only had an informal semantics and a recently defined formal semantics without distribution of policies). The semantics is expressed in ΔDSTL(x), an extension of temporal logic to deal with global applications: it includes modalities to localize properties to system components, an operator to deal with events, and temporal modalities à la Unity. A further contribution of the paper is the development of semantics based techniques to detect policy conflict and a consideration of conflict resolution.

Reusing available software components in developing new systems is always a priority, as it usually saves a considerable amount of time, money, and human effort. Since it might not always be possible to find a single component that provides the sought functionality, an ideal scenario for software reuse would be to build a new software system by composing existing components based on their behavioral properties. In this paper we take advantage of logical reasoning to find a solution for automatic composition of stateless components. Stateless components are components with a simple two step behavior: they receive all their inputs at the same time, and then return the corresponding outputs also at the same time. We provide concrete algorithms to find possible component compositions for a requested behavior. We then validate the returned compositions using composition algebraic rules. Composition algebra is a minimal process algebra that is specifically designed for this validation. In order to understand the functionality of the proposed approach in realistic situations, we also study some of the experimental results obtained by implementing the algorithm and running it on some test cases.