Sérgio Vale Aguiar Campos

Abstracts

The Verus Language: Representing Time Efficiently with BDDs
S. Campos and E. Clarke

There have been significant advances on formal methods to verify real-time systems recently. Nevertheless, these methods have not yet been accepted as a realistic alternative to the verification of industrial systems. One reason for this is that formal methods are still difficult to apply efficiently. Another reason is that current verification algorithms are still not efficient enough to handle many complex systems. This work addresses this problem by presenting a language designed especially to simplify writing real-time programs. It is an imperative language with a syntax similar to C. Special constructs are provided to allow the straightforward expression of timing properties. The familiar syntax makes it easier for non-experts to use the tool. The special constructs make it possible to model the timing characteristics of the system naturally and accurately. A symbolic representation using BDDs, model checking and quantitative algorithms are used to check system timing properties. The efficiency of the representation allows complex realistic systems to be verified by the method as evidenced by the examples verified such as the aircraft controller discussed in the paper.

Symbolic Techniques for Formally Verifying Industrial Systems
S. Campos, E. Clarke and M. Minea The design of correct computer systems is extremely difficult. However, it is also a very important task. Such systems are frequently used in applications where failures can have catastrophic consequences, or cause significant financial losses. Simulation and testing are the most widely used verification techniques, but they can only show the presence of errors and cannot demonstrate correctness. Until lately formal methods were too expensive to be used in industrial problems, but recent research has made it possible to apply formal techniques to the verification of complex real-world systems. Symbolic model checking is an example of such a technique that has been successful in verifying large finite-state systems. It has also been extended to produce timing and performance information. These properties are extremely important in the design of high-performance systems and time-critical applications. A more detailed analysis of a model is possible using these extensions than by simply determining whether a property is satisfied or not. We present algorithms that determine the exact bounds on the delay between two specified events and the number of occurrences of another event in all such intervals. To demonstrate how our method works, we present two complex examples: the verification of the Futurebus+ cache coherence protocol and the timing analysis of the PCI local bus. These results show the usefulness of symbolic model checking in analyzing modern industrial designs.

Verifying the Performance of the PCI Local Bus using Symbolic Techniques
S. Campos, E. Clarke, W. Marrero and M. Minea Symbolic model checking is a successful technique for checking properties of large finite-state systems. This method has been used to verify a number of real-world hardware designs. This methodology, however, is not able to determine timing or performance properties directly. Since these properties are extremely important in the design of high-performance systems and in time-critical applications, we have extended model checking techniques to produce timing information. These results allow a more detailed analysis of a model than is possible with tools that simply determine whether a property is satisfied of not. We present algorithms that determine the exact bounds on the delay between two specified events and the number of occurrences of another event in all such intervals. To demonstrate how our method works, we have modelled the PCI local bus and analyzed its temporal behavior. These results show the usefulness of this technique in analyzing complex modern designs.

Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems
S. Campos, E. Clarke, W. Marrero and M. Minea

Symbolic model checking is a technique for verifying finite-state concurrent systems that has been extended to handle real-time systems. Models with up to 10E30 states can often be verified in minutes. In this paper, we present a new tool to analyze real-time systems, based on this technique. We have designed a language, called Verus, for the description of real-time systems. Such a description is compiled into a state-transition graph and represented symbolically using binary decision diagrams. We have developed new algorithms for exploring the state space and computing quantitative information about the system. In addition to determining the exact bounds on the delay between two specified events, we compute the number of occurrences of an event in all such intervals. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of the behavior of the system, in addition to verifying if its timing requirements are satisfied. We integrate these ideas into the Verus tool, currently under development. To demonstrate how our technique works, we have verified a robotics control system. The results obtained demonstrate that our method can be successfully applied in the analysis of real-time system designs.

Computing Quantitative Characteristics of Finite-State Real-Time Systems
S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi

Current methods for verifying real-time systems are essentially decision procedures that establish whether the system model satisfies a given specification. We present a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. We also show that our technique can be extended to a more general representation of real-time systems, namely, timed transition graphs. The algorithms presented in this paper have been incorporated into the SMV model checker and used to verify a model of an aircraft control system. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.

De volta a página principal