Catálogo de publicaciones - libros

This is to advocate the approach to reducing program verification to the algebraic symbolic computation. Recent advances indicate that various verification problems can be reduced to semi-algebraic systems (SAS for short), and resolved through computer algebra tools. In this talk, we report our encouraging attempts at applying DISCOVERER to program termination analysis and state reachability computation. DISCOVERER is a Maple program implementing an algorithm of real solution classification and isolation for SAS, which is based on the discovery of complete discrimination systems of parametric polynomials. The talk also concludes that this approach deserves further attention from the program verification community. For theoretical and technical details of the work, we refer the reader to [1,2,3,4,5].

The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This paper describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

We present three perspectives of the use of formalism in the construction of High-Integrity Embedded Real-time Systems. In the first, we describe the long-term research aims. The scope is the entire system, the goal is to demonstrate intentional correctness, and the emphasis is on scientific certainty . In the second, we present medium-term research aims. The scope is more on the software in the system, and the emphasis shifts to the notion of engineering confidence . Following on from the medium-term view we propose a set of challenges for formal engineering methods research, based on our perception of the technical issues surrounding the provision of viable engineering solutions. In the third perspective we discuss the short term. In particular, we describe how our recent research is attempting to meet some of the proposed challenges, as a first step towards our medium and long-term aspirations.

We present a methodology for the formalization of human-computer interaction under security aspects. As part of the methodology, we give formal semantics for the well-known GOMS methodology for user modeling, and we provide a formal definition of an important aspect of human-computer interaction security. We show how formal GOMS models can be augmented with formal models of (1) the application and (2) the user’s assumptions about the application. In combination, this allows the pervasive formal modeling of and reasoning about secure human-computer interaction. The method is illustrated by a simple eVoting example.

Simulink has been used widely as an industry tool to model and simulate embedded systems. With increasing usage of embedded systems in real-time safety-critical situations, Simulink is deficient to cope with the requirements of high-level assurance and timing analysis. In this paper, we present a systematic approach to translate Simulink diagrams to Timed Interval Calculus (TIC), a notation extending Z to support real-time system specification and verification. This work is based on the same angle chosen by Simulink and TIC where they model systems in terms of continuous time. Translated TIC specifications preserve the functional and timing aspects of the diagrams, and cover a wide range of Simulink blocks. After the translation, we can increase the design space by specifying important requirements, especially timing constraints exactly on the system or its components. Moreover, we can take advantage of TIC reasoning rules to formally verify systems with requirements, and hence elevate the design quality of Simulink.

Verification of parameterized systems for an arbitrary number of instances is generally undecidable. Existing approaches resort to non-trivial restrictions on the system or lack automation. In practice, applications can often provide a suitable bound on the parameter size. We propose a new technique toward the bounded formulation of parameterized reasoning: how to efficiently verify properties of a family of systems over a large finite parameter range. We show how to accomplish this with a single verification run on a model that aggregates the individual instances. Such a run takes significantly less time than if the systems were considered one by one. Our method is applicable to a completely inhomogeneous family of systems, where properties may not even be preserved across instances. In this case the method exposes the parameter values for which the verification fails. If symmetry is present in the systems, it is inherited by the aggregate representation, allowing for verification over a reduced model. Our technique is fully automatic and requires no approximation.

The induction-guided falsification searches a bounded reachable state space of a transition system for a counterexample that the system satisfies an invariant property. If no counterexamples are found, it tries to verify that the system satisfies the property by mathematical induction on the structure of the reachable state space of the system, from which some other invariant properties may be obtained as lemmas. The verification and falsification process is repeated for each of the properties until a counterexample is found or the verification is completed. The NSPK authentication protocol is used as an example to demonstrate the induction-guided falsification.

The language χ has been developed for modeling of industrial systems. Its simulator has been successfully used in many industrial areas for obtaining performance measures. For functional analysis simulation is less applicable and such analysis can be done in other environments. The purpose of this paper is to describe an automatic translator from χ to Promela , the input language of the well known model-checker Spin . We highlight the differences between the two languages and show, in a step by step manner, how some of them can be resolved. We conclude by giving a translation scheme and apply the translator in a small industrial case study.

State space explosion is the main obstacle for model checking concurrent programs. Among the solutions, partial-order reduction (POR), especially dynamic partial-order reduction (DPOR) [1], is one of the promising approaches. However, DPOR only supports stateless explorations for acyclic state spaces. In this paper, we present the stateful DPOR approach for may-cyclic state spaces, which naturally combines DPOR with stateful model checking to achieve more efficient reduction. Its basic idea is to summarize the interleaving information for all transition sequences starting from each visited state, and infer the necessary partial-order information based on the summarization when a visited state is encountered again. Experiment results on two programs coming from [1] show that both of the costs of space and time could be remarkably reduced by stateful DPOR with rather reasonable extra memory overhead.

Transaction is the key mechanism to make service composition reliable. To ensure the relaxed atomicity of transactional composite service (TCS), existing research depends on the analysis to composition structure and exception handling mechanism. However, this approach can not handle various application-specific requirements, and causes lots of unnecessary failure recoveries or even aborts. In this paper, we propose a relaxed transaction model, including system mode, relaxed atomicity criterion, static checking algorithm and dynamic enforcement algorithm. Users can define different relaxed atomicity constraint for different TCS according to the specific application requirements, including accepted configurations and the preference order. The checking algorithm determines whether the constraint can be satisfied. The enforcement algorithm monitors the execution and performs transaction management works according to the constraint. Compared to existing work, our approach is flexible enough to handle complex application requirements and performs the transaction management works automatically. We apply the approach into web service composition language WS-BPEL and illustrate the above advantages through a concrete example.