Catálogo de publicaciones - libros

CSP is a well-established formalism for modelling and verification of concurrent reactive systems based on refinement. Consolidated denotational models and an effective tool have encouraged much work on algebraic reasoning and model checking. Testing techniques based on CSP, however, have not been widely explored, and in this paper we take a first step by instantiating Gaudel et al’s theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to use CSP models as a basis for testing. We also define test sets that we prove to be exhaustive with respect to traces and failures refinement, and consider optimisations, inputs and outputs, and selection strategies. Our results are proved in terms of the CSP denotational models; they are a sound foundation for the development of test-generation techniques.

Conformance testing has been extensively studied in the context where the desired behavior of the is modeled in terms of finite state machines. An essential issue in FSM-based conformance testing is to generate from a given finite state machine a test sequence that is both effective in detecting the faults in the and efficient in terms of its length. In this paper, we consider test sequences satisfying the test criterion of the U-method as they have been proved to have high fault detectability. We present our solution to reduce the length of such a test sequence by maximizing the overlap among the test segments through the use of .

Bounded semantics of LTL with existential interpretation and that of ECTL (the existential fragment of CTL), and the characterization of these existentially interpreted properties have been studied and used as the theoretical basis for SAT-based bounded model checking [2,18]. This has led to a lot of successful work with respect to error detection in the checking of LTL and ACTL (the universal fragment of CTL) properties by satisfiability testing. Bounded semantics of LTL with the universal interpretation and that of ACTL, and the characterization of such properties by propositional formulas have not been successfully established and this hinders practical verification of valid universal properties by satisfiability checking. This paper studies this problem and the contribution is a bounded semantics for ACTL and a characterization of ACTL properties by propositional formulas. Firstly, we provide a simple bounded semantics for ACTL without considering the practical aspect of the semantics, based on converting a Kripke model to a model (called a -model) in which the transition relation is captured by a set of -paths (each path with transitions). This bounded semantics is not practically useful for the evaluation of a formula, since it involves too many paths in the -model. Then the technique is to divide the -model into submodels with a limited number of -paths (which depends on and the ACTL property to be verified) such that if an ACTL property is true in every such model, then it is true in the -model as well. This characterization can then be used as the basis for practical verification of valid ACTL properties by satisfiability checking. A simple case study is provided to show the use of this approach for both verification and error detection of an abstract two-process program written as a first order transition system.

Refinement plays a crucial role in “top-down” styles of verification, such as the refinement calculus, but for probabilistic systems is a particularly challenging task due to the combination of probability and nondeterminism which typically arises in partially-specified systems.

Whilst the theory of probabilistic refinement is well-known [18] there are few tools to help with establishing refinements between programs.

In this paper we describe a tool which provides partial support during refinement proofs. The tool essentially builds small models of programs using an algebraic rewriting system to extract the overall probabilistic behaviour. We use that behaviour to recast refinement-checking as a , which can then be exported to a linear arithmetic solver.

One of the major benefits of this approach is the ability to generate counterexamples, alerting the prover to a problem in a proposed refinement.

We demonstrate the technique on a small case study based on Schneider et al.’s Tank Monitoring [26].

This work presents a case study of the use of model checking for analyzing an industrial software, the Generic Bootloader. Analysis of the software have been carried out using the automated verification system SPIN. A model of the software has been developed using the specification language PROMELA, and the properties expressed in the LTL have been verified against the model. We propose a new modeling technique that helps to model communication protocols efficiently. Formal analysis has also helped us to reveal a flaw in the implementation of the software which otherwise remain undetected through testing process.

This paper investigates a model checking algorithm for Propositional Projection Temporal Logic (PPTL) with finite models. To this end, a PPTL formula is transformed to a Normal Form Graph (NFG), and then a Nondeterministic Finite Automaton (NFA). The NFA precisely characterizes the finite models satisfying the corresponding formula and can be equivalently represented as a Deterministic Finite Automaton (DFA). When the system to be verified can be modeled as a DFA , and the property of the system can be specified by a PPTL formula , then ¬ can be transformed to a DFA . Thus, whether the system satisfies the property or not can be checked by computing the product automaton of and , and then checking whether or not the product automaton accepts the empty word. Further, this method can be implemented by means of the verification system .

Handel-C is a hybrid language based on C and CSP for the high level description of hardware components. Several semantic models for the language and a non-rigorous compilation mechanism have been proposed for it. The compilation has been empirically validated and used in commercial tools, but never formally verified. This work presents a semantic model of the generated hardware and establishes the foundations for the formal verification of correctness of the transformation approach.

The complexity inherent to concurrent systems can turn their development into a very complex and error-prone task. The use of formal languages like CSP and tools that support them simplifies considerably the task of developing such systems. This process, however, usually aims at reaching an executable program: a translation between the specification language and a practical programming language is still needed and is usually rather problematic. In this paper we present a translation framework and a tool, , that implements it. This framework provides an automatic translation from a subset of CSP to Handel-C, a programming language that is similar to standard C, but whose programs can be converted to produce files to program an FPGA.

An accurate and reliable clock synchronization mechanism is a basic requirement for the correctness of many safety-critical systems. Establishing the correctness of such mechanisms is thus imperative. This paper addresses the modeling and formal verification of a specific fault-tolerant master/slave clock synchronization system for the Controller Area Network. It is shown that this system may be modeled with hybrid automata in a very natural way. However, the verification of the resulting hybrid automata is intractable, since the modeling requires variables that are dependent. This particularity forced us to develop some modeling techniques by which we translate the hybrid automata into single-rate timed automata verifiable with the model-checker . These techniques are described and illustrated by means of a simple example.

This paper describes three optimization techniques for a process algebra interpreter called . This interpreter supports the method, which was developed for the purpose of automating the development of information systems using of abstract specifications. The proposed optimizations allow an interpreter to execute actions on a quantified choice in constant time and on a quantified parallel composition in logarithmic time with respect to the number of entities in a quantified entity type. This time complexity is comparable to that of programmer-derived implementation of process expressions and significantly better than the time complexity of common process algebra simulators, which execute quantifications by computing their expansion into binary expressions.