Search

This paper presents the foundations and the real use of a tool to automatically detect anomalies in Internet traffic produced by mobile applications. In particular, our MVE tool is focused on analyzing the impact that user interactions have on the traffic produced and received by the smartphones. To make the analysis exhaustive with regard to the potential user behaviors, we follow a model-based approach to automatically generate test cases to be executed on the smartphones. In addition, we make use of a specification language to define traffic patterns to be compared with the actual traffic in the device. MVE also includes monitoring and verification support to detect executions that do not fit the patterns. In these cases, the developer will obtain detailed information on the user actions that produce the anomaly in order to improve the application. To validate the approach, the paper presents an experimental study with the well-known Spotify app for Android, in which we detected some interesting behaviors. For instance, some HTTP connections do not end successfully due to timeout errors from the remote Spotify service.

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs.

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.

Software model checking consists in applying the most powerful results in formal verification research to programming languages such as C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, such as SPIN. This paper focusses on the application of this approach to the avionics software constructed on top of the Application Executive Software (APEX) Interface, which is widely employed by manufacturers in the avionics industry. It presents a method to automatically extract PROMELA models from the C source code. In order to close the extracted model during verification, we built a reusable APEX-specific environment. This APEX environment models the execution engine (i.e. an APEX compliant real-time operating system) that implements APEX services. In particular, it explains how to deal with aspects such as real-time and APEX scheduling. Time is modelled in such a way that the we save time and memory by avoiding the analysis of irrelevant steps. This model of time and the construction of a deterministic scheduler guarantees the scalability of our approach. The paper also presents a tool that can verify realistic applications, and that has been used as a novel testing method to ensure the correctness of our APEX environment. This testing method uses SPIN to execute official APEX test cases. Copyright © 2010 John Wiley & Sons, Ltd.

Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.

Locating potential execution errors in software is gaining more attention due to the economical and social impact of software crashes. For this reason, many software engineers are now in need of automatic debugging tools in their development environments. Fortunately, the work on formal method technologies during the past 25 years has produced a number of techniques and tools that can make the debugging task almost automatic, using standard computer equipment and with a reasonable response time. In particular, verification techniques like model-checking that were traditionally employed for formal specifications of the software can now be directly employed for real source code. Due to the maturity of model-checking technology, its application to real software is now a promising and realistic approach to increase software quality. There are already some successful examples of tools for this purpose that mainly work with self-contained programs (programs with no system-calls). However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend. In this paper, we propose a method for using the tool spin to verify C software systems that use services provided by the operating system thorough a given API. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker spin. The whole modeling process is transparent for the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we guarantee that the system only reports potential (non-spurious) errors. We present the applicability of our approach focusing on the verification of distributed software systems that use the API Socket and the network protocol stack TCP/IP for communications. In order to ensure correctness, we define and use a formal semantics of the API to conduct the construction of correct models.

A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification.

The combination of static and dynamic software analysis, such as data flow analysis (Dfa) and model checking, provides benefits for both disciplines. On the one hand, the information extracted by Dfas about program data may be utilized by model checkers to optimize the state space representation. On the other hand, the expressiveness of logic formulas allows us to consider model checkers as generic data flow analyzers. Following this second approach, we propose in this paper an algorithm to calculate Dfas using on-the-fly resolution of boolean equation systems (Bess). The overall framework includes the abstraction of the input program into an implicit labeled transition system (Lts), independent of the program specification language. Moreover, using Bess as an intermediate representation allowed us to reformulate classical Dfas encountered in the literature, which were previously encoded in terms of μ-calculus formulas with forward and backward modalities. Our work was implemented and integrated into the widespread verification platform Cadp, and experimented on real examples.

The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can still be generated, which may prevent model-checking tools from verifying tccp programs completely. Model checking tccp programs is a difficult task due to the subtleties of the underlying operational semantics, which combines constraints, concurrency, non-determinism and time. Currently, there is no practical model-checking tool that is applicable to tccp. In this work, we introduce an abstract methodology which is based on over- and under-approximating tccp models and which mitigates the state explosion problem that is common to traditional model-checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that this preliminary abstract semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension. Finally, we complete our methodology by approximating the temporal properties that must be verified.

Increasing the quality of software for new telecommunication services requires the joint use of different testing techniques. For instance, automatic verification and performance evaluation are necessary to ensure desired throughput and reliability. However, both kinds of analysis were traditionally performed without sharing a common description of the system, and much work and time was wasted constructing different specifications oriented to particular tools.In recent years a lot of research has been carried out to design languages and tools to manage both functional and performance analysis with only one description, specially within communities devoted to process algebras and Petri nets. These homogeneous frameworks remove the inconveniences of maintaining a set of specifications for the same software.In the paper, we explore an alternative approach to keep the specification of different aspects to be analyzed consistent. Taking into account the number and quality of existing tools for modelling and analyzing telecommunication software, we explore semi-automatic methods to integrate these tools in a way that is as transparent as possible for users. Ideally, the designer of new services will provides only one description of the software with its most familiar language, and a toolset will generate particular specifications to analyze each aspect of interest (currently, reliability and performance). Our proposal takes advantages of recent work on model-driven architecture (mda) and xml for automating tool construction. Its applicability is shown in the context of developing new services with the active network paradigm, integrating the features of the model checker spin and the network simulator ns2.

Recent advances in languages and execution environments (EEs) for active networks make it now possible to develop applications with this new exciting approach. In particular, active networks have proven to be very suitable for multicast services. Nevertheless, to open the network nodes to the code written by users requires the use of analysis techniques to avoid the degradation of the network performance. Model checking is one of the most powerful techniques to ensure software reliability. This technique has been successfully applied to many protocols developed with the classic (non-active) approach. Our aim is to extend its application to the area of active protocols. The paper consists of two main contributions: (a) a clear scheme to use the language promela in order to formalize different elements in the active service (network EE, capsules and user applications) and (b) the practical (and successful) application of the approach to analyze an active multicast protocol using the model checker spin.

The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate to analyze by model checking timing properties of concurrent systems. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can be still generated which may prevent model checking tools from verifying tccp programs completely. In this paper, we introduce an abstract methodology which is based on over- and under-approximating tccp models and mitigates the state explosion problem which is common to traditional model checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that, due to the timing aspects of the language, this semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension.

Semantics of description languages for complex systems are a central issue for implementing verification methods such as abstract model checking . This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool αspin as an extension of spin.

ion methods have become one of the most interesting topics in the automatic verification of software systems because they can reduce the state space to be explored and allow model checking of more complex systems. Nevertheless, there is a lack of tools actually supporting this technique. One direction for abstracting a system is to transform its formal description (its model) into a simpler version specified in the same language, thus skipping the construction of a specific (model checking) tool for the abstract model. The abstraction of the model should be followed by the abstraction of the temporal formulas to be checked. This paper presents źspin, a tool for the integration of abstraction (for models and formulas) into the well-known model checker spin. We present the theoretical results supporting the implementation together with a case study.

Abstraction methods have become one of the most interesting topics in the automatic verification of software systems because they can reduce the state space to be explored and allow model checking of more complex systems. Nevertheless, there is a lack of tools actually supporting this technique. One direction for abstracting a system is to transform its formal description (its model) into a simpler version specified in the same language, thus skipping the construction of a specific (model checking) tool for the abstract model. The abstraction of the model should be followed by the abstraction of the temporal formulas to be checked. This paper presents αSpin, a tool for the integration of several abstraction approaches (for models and formulas) into the well known model checker Spin. In particular, αSpin integrates two dual approaches, the classic abstraction method, based on under-approximating properties, and an alternative approach, proposed by the authors, where abstraction provides an over-approximation of the formulas. 2

UML (Unified Modeling Language) and XML (Extensible Markup Language) related technologies have matured, and at present many novel applications of both languages are frequently appearing. This chapter discusses the combined use of both UML and XML in the exciting application domain of software abstraction for verification. In particular, software development environments that use UML notations are now including verification capabilities based on state exploration. This method is effective for many realistic problems, although it is well known that it is affected by the state explosion problem for many complex systems and that some kind of abstraction is needed. This is the point where XML can be used as a powerful technology, due to its features for program transformation. We describe how to use XML-related standards like dom or xmi in order to extend UML verification tools with automatic abstraction.

One of the most exciting and promising approaches to ensure the correctness of critical systems is software model checking, which considers real code, written with standard programming languages like C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, like spin. This paper presents the application of the technique to avionics software constructed on top of an application interface (API) compliant with the ARINC 653 specification (APEX), which is widely employed by the manufacturers in the avionics industry. The paper uses techniques to automatically extract promela models from C source code. These techniques were previously developed by the authors. However, they are now extended to deal with new problems, like real-time aspects and APEX scheduling. In order to close the extracted model during the verification, we built a reusable APEX-specific environment. This APEX environment models the execution engine (i.e. an APEX compliant RTOS) that implements APEX services. Finally, this paper also contains a novel testing method to ensure the correctness of this APEX environment. This testing method uses SPIN to execute official ARINC 653 test cases.

This paper describes a set of verification components that open the way to perform on-the-fly software model checking with the Cadp toolbox, originally designed for verifying the functional correctness of Lotos specifications. Two new tools (named C. OPEN and ANNOTATOR) have been added to the toolbox. The approach taken fits well within the existing architecture of CADP which doesn't need to be altered to enable C program verification.

Model Checking is a powerful verification method to increase the quality of software systems. However, the application of this technique is only possible and fruitful if useful models of the software are available. A useful model is an abstract representation of a system, containing only the details necessary to ensure that satisfaction (non-satisfaction) of interesting properties in the model provides information about the behavior of the real system. Abstraction methods have become one of the hottest topics in the automatic verification of software systems because they can reduce the state space to be explored and allow the verification of more complex systems [1],[3].

The execution of a concurrent logic program on a distributed system is very dependent on the program granularity and the communication costs. We present a framework based on the abstract interpretation technique to obtain information about these program characteristics and show how its execution time can be improved using the analysis.

Model Checking is currently one of the most exciting techniques to improve the quality of complex software systems. It is a computer aided verification method that, in many cases, has discovered design bugs in early development steps, thus saving time and costs to produce the final code. Although this technique is successfully applied to many formal description techniques, it is not commonly used by the object oriented programming community, in general, nor by UML developers, in particular. In this paper, we provide a comprehensive overview and rules to integrate model checking into UML-based designs, showing its usefulness from a practical point of view, and giving some guidelines to exploit the benefits of the integration.

The application of model checking technology to real software seems to be a promising and realistic approach to increase its quality. There are some successful examples of tools for this purpose, mainly working with self-contained programs. However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend.In this paper, we give a method for using the tool SPIN to verify distributed software systems that use the API Socket and the network protocol stack TCPIP for communications. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker. We define and use a formal semantics of the API to conduct the correct construction of models. The whole modelling process is transparent to the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we ensure that the system only reports potential (non-spurious) errors.

This paper presents our experiences on using xml technologies and standards for the integration of analysis tools for protocols. The core proposal consists in the design of a new xml-based language named PiXL (Protocol Interchange using xml Languages), responsible for interchanging the whole specification of the protocol (data and control) among different existing tools. The structure and flexibility of xml has proven to be very useful when implementing new tools such as abstract model checkers. In addition, the suitability of the proposal has been applied to achieve a new kind of analysis, where PiXL and new mda methodologies have been proposed to build integrated environments for reliability and performance analysis of Active Network protocols.

Model Checking has become one of the most powerful methods for automatic verification of software systems. However it is widely accepted that this technique is only usable when the behavior of the system to be analyzed is given by small models, in order to avoid the state explosion problem. The paper presents αSPIN, an XML-based tool for obtaining abstract versions from a given model written in PROMELA, which can be verified with the model checker SPIN. This tool follows the theoretical basis presented in [9].