Catálogo de publicaciones - libros

CSP-style synchronizations have been used extensively in the construction of mathematical models for the verification of embedded systems. Although they allow for the modeling of complex cooperation among many processes in a natural environment, not many tools have been developed to support the modeling capability in this regard. In this paper, we first give examples to argue that special algorithms are needed for the efficient verification of systems with complex synchronizations. We then define our models of distributed real-time systems with synchronized cooperation among many processes. We present algorithms for the construction of BDD-like data-structures for the characterization of complex synchronizations among many processes. We present weakest precondition algorithms that take advantage of the just-mentioned BDD-like data-structures for the efficient verification of complex real-time systems. Finally, we report experiments and argue that the techniques could be useful in practice.

Performance and usability of deductive program verification systems can be enhanced if specifications not only consist of pre-/post-condition pairs and invariants but also include information on which memory locations are modified by the program. This allows to separate the aspects of (a) which locations change and (b) how they change, state the change information in a compact way, and make the proof process more efficient. In this paper, we extend this idea from method specifications to loop invariants ; and we define a proof rule for while loops that makes use of the change information associated with the loop body. It has been implemented and is successfully used in the KeY software verification system.

Stålmarck’s 1-saturation algorithm is an incomplete but fast method for computing partial equivalence relations over propositional formulae. Aside from anecdotal evidence, until now little has been known about what it can prove. In this paper we characterize a set of formulae with bitvector-inequalities for which 1-saturation is sufficient to prove unsatisfiability. This result has application to fast predicate abstraction for software with fixed-width bit-vectors.

Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and implementation for B. It is based on using an operational semantics of B, obtained in practice by the ProB animator. The refinement checker has been integrated into ProB toolset and we present various case studies and empirical results in the paper, showing the algorithm to be surprisingly effective. The algorithm checks that a refinement preserves the trace properties of a specification. We also compare our tool against the refinement checker FDR for CSP and discuss an extension for singleton failure refinement.

Model checking specifications with complex data and behaviour descriptions often fails due to the large state space to be processed. In this paper we propose a technique for reducing such specifications (with respect to certain properties under interest) before verification. The method is an adaption of the slicing technique from program analysis to the area of integrated formal notations and temporal logic properties. It solely operates on the syntactic structure of the specification which is usually significantly smaller than its state space. We show how to build a reduced specification via the construction of a so called program dependence graph, and prove correctness of the technique with respect to a projection relationship between full and reduced specification. The reduction thus preserves all properties formulated in temporal logics which are invariant under stuttering, as for instance LTL_−  X .

A schema of communication elimination laws for distributed programs and systems is mathematically justified in a new equivalence, which was introduced in a recent work. A complete set of applicability conditions is derived for them. A formal communication elimination algorithm, applying the laws as reductions, is mathematically justified for an important class of distributed programs and systems, whose communications are outside the scope of selections. The analysis provides the basis for extensions to general statements. State-vector reduction stands as one of the motivations for this static analysis approach. It has already been applied in an equivalence proof of a non-trivial pipelined distributed system, reported in prior works. The state-vector reduction obtained in this proof, yielding a reduction factor of 2^− − 607 for the upper-bound on the number of states, is presented in this communication.

Verifications of parallel programs are frequently based on automated state-space exploration techniques known as model checking. To avoid state-space explosion problems, theorem proving techniques can be used, for example by manually annotating programs with suitable assertions and using these assertions to prove their correctness (e.g. using the Owicki/Gries theory). We propose a method to support assertion-based methods with theorem provers like PVS. Emphasis is on the typical incremental character of assertion-based methods, and on automated strategies for proving correctness of the proof outlines.

Many safety-critical systems deal with geometric objects. Reasoning about the correctness of such systems is mandatory and requires the use of basic definitions of geometry for the specification of these systems. Despite the intuitive meaning of such definitions, their formalisation is not at all straightforward: In particular, degeneracies lead to situations where none of the Boolean truth values adequately defines a geometric primitive. Therefore, we use a three-valued logic for the definition of geometric primitives to explicitly handle such degenerate cases. We have implemented a three-valued library of linear geometry in an interactive theorem prover for higher order logic which allows us to specify and verify entire algorithms of computational geometry.

In this paper, we describe how formal specification is adopted to improve the commonly used verification and validation technique known as program inspection , in order to establish a more rigorous, repeatable, and efficient inspection process than the conventional practice. We present a systematic approach to inspecting program code on the basis of the relation between functional scenarios defined in a specification and execution paths implemented in its program. We report a prototype tool for the approach to support both forward and backward inspection strategies, and a case study of inspecting an Automatic Teller Machine system to evaluate the performance of the approach and the tool.

The development of Web Services has transformed the World Wide Web into a more application-aware information portal. The various standards ensure that Web Services are interpretable and extensible, opening up possibilities for simple services to be combined to build complex ones. The Semantic Web presents a new mechanism for users and software agents to discover, describe, invoke, compose and monitor Web services. For these purposes the Semantic Web Services (OWL-S) ontologies have been developed to provide vocabularies to describe Web Services in a precise and machine-understandable way. It is necessary to ensure the ontological descriptions of the services capture the intended meaning as erroneous description may cause invocation of wrong services, with wrong parameters, resulting in undesired outcome. In this paper, we propose to apply software engineering method and tools to visualize, simulate and verify OWL-S process models. Namely, Live Sequence Charts (LSCs) is used to model services, capturing the inner workings of services, and its tool support Play-Engine is used to perform automated visualization, simulation and checking.