Catálogo de publicaciones - libros

Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method – the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.

Traditionally, developers of concurrent systems have adopted two distinct approaches: those with semantics and those with semantics. In the coarser interleaving interpretation parallelism can be captured in terms of non-determinism whereas in the finer, truly concurrent interpretation it cannot. Thus processes  ∥  and . + . are identified within the interleaving approach but distinguished within the truly concurrent approach.

In [5] we explored the truly concurrent notions of , whereby transitions can occur individually but not together from a given state, and , whereby the conflict set of a given transition is altered by the occurrence of another transition with which it does not interfere. We presented a translation from the truly concurrent formalism of Petri nets to the interleaving process algebra CSP and demonstrated how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets. This work is of interest firstly because, to the author’s knowledge, no existing tool for Petri nets can perform these checks, and secondly (and perhaps more significantly) because we bridged the gap between truly concurrent and interleaving formalisms, demonstrating that true concurrency can be captured in what is typically considered to be an interleaving language.

In this paper we build on the work presented in [5] further embedding the truly concurrent notions of conflict and confusion in the interleaving formalism CSP by extending the domain of our translation from the simplistic subset of Petri nets, in which each place can hold at most one token, to standard Petri nets, in which the number of tokens in each place is unbounded.

This paper investigates the use of the probabilistic and continuous extensions of action systems in the development and calculation of reliability of continuous, real-time systems. Rather than develop a new semantics to formally combine the existing extensions, it investigates a methodology for using them together, and the conditions under which this methodology is sound. A key feature of the methodology is that it simplifies the development process by separating the probabilistic calculations of system reliability from the details of the system’s real-time, continuous behaviour.

Integrated formal specifications are intrinsically difficult to (automatically) verify due to the combination of complex data and behaviour. In this paper, we present a method for specifications into several smaller parts which can be independently verified. Verification results can then be combined to make a global result according to the original specification.

Instead of relying on an given structure of the system such as a parallel composition of components, we compute the decomposition by ourselves using the technique of . With less effort, significant properties can be verified for the resulting specification parts and be applied to the full specification. We prove correctness of our method and exemplify it according to a specification from the rail domain.

We present the architecture and implementation of the tool to validate high-level Z specifications. The tool was integrated into , by providing a translation of Z into B and by extending the kernel of to accommodate some new syntax and data types. We describe the challenge of going from the tool friendly formalism B to the more specification-oriented formalism Z, and show how many Z specifications can be systematically translated into B. We describe the extensions, such as record types and free types, that had to be added to the kernel to support a large subset of Z. As a side-effect, we provide a way to animate and model check records in . By incorporating into , we have inherited many of the recent extensions developed for B, such as the integration with CSP or the animation of recursive functions. Finally, we present a successful industrial application, which makes use of this fact, and where was able to discover several errors in Z specifications containing higher-order recursive functions.

Multi-agent systems provide an increasingly popular solution in problem domains that require management of uncertainty and a high degree of adaptability. Robustness is a key design criterion in building multi-agent systems. We present a novel approach for the design of robust multi-agent systems. Our approach constructs a model of the design of a multi-agent system in Alloy, a declarative language based on relations, and checks the properties of the model using the Alloy Analyzer, a fully automatic analysis tool for Alloy models. While several prior techniques exist for checking properties of multi-agent systems, the novelty of our work is that we can check properties of coordination and interaction, as well as properties of complex data structures that the agents may internally be manipulating or even sharing. This is the first application of Alloy to checking properties of multi-agent systems. Such unified analysis has not been possible before. We also introduce the use of a formal method as an integral part of testing and validation.

We port verification techniques for device drivers from the Windows domain to Linux, combining several tools and techniques into one integrated tool-chain. Building on ideas from Microsoft’s (SDV) project, we extend their specification language and combine its implementation with the public domain bounded model checker CBMC as a new verification back-end. We extract several API conformance rules from Linux documentation and formulate them in the extended language SLICx. Thus SDV-style verification of temporal safety specifications is brought into the public domain. In addition, we show that SLICx, together with CBMC, can be used to simulate preemption in multi-threaded code, and to find race conditions and to prove the absence of deadlocks and memory leaks.

The verification of cryptographic protocol is an active research topic and has received much attention from the formal verification community. By contrast, the black-box testing of actual of protocols, which is, arguably, as important as verification for ensuring the correct functioning of protocols in the “real” world, is little studied. We propose an approach for checking secrecy and authenticity properties not only on protocol specifications, but also on black-box implementations. The approach is compositional and integrates ideas from verification, testing, and learning. It is illustrated on the Basic Access Control protocol implemented in biometric passports.

Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. is a widely-used calculus equipped with , a graphical and user-friendly tool. is the only process calculus that has led to an international standard, and is supported by the verification toolbox. We propose a translation from to . Since composite processes are hard to encode into , they are translated into networks of automata which are another input language accepted by . Hence, it is possible to use jointly and to validate specifications. Our approach is completely automated by a translator tool we implemented.

In this paper, we introduce a common semantic framework for developing and formally modeling use cases and task models. Use cases are the notation of choice for functional requirements specification and documentation, whereas task models are used as a starting point for user interface design. Based on their intrinsic characteristics we devise an intermediate semantic domain for use cases and for task models, respectively. We describe how the intermediate semantic domain for each model is formally mapped into a common semantic domain which is based on sets of partial order sets. We argue that a two-step mapping results in a semantic framework that can be more easily validated, reused and extended. As a partial validation of our framework we provide a semantics for ConcurTaskTrees (CTT) one of the most popular task model notations as well as our own DSRG use case formalism. Furthermore we use the common semantic model to formally define a satisfiability relation between task model and use case specifications.