Búsqueda avanzada

Resultados de búsqueda para Model checking

Using Model Checking in Requirement-based Test Generation for Reactive Systems

In this article we propose an automatic test generation technique for evaluating the implementation of a reactive system with respect to the set of requirements from which it has been developed. We consider reactive systems that interact with its environment via variables whose values (at each instant) depends on events or sensors. Our test cases are graphs that represent a collection of executions (or traces) of the system that captures all possible behaviours of the environment. Our proposal is a technique to automatically construct these graphs exploding the ability of model checkers to generate counter-examples for temporal properties that are not satisfied by a system model. Further work includes to implement a prototype for experimenting the technique on a test suite of industrial requirements, and also to design and implement some techniques to gain scalability.

Autores: Montserrat Hermo / Paqui Lucio / Josu Oca / 
Palabras Clave: Model checking - Reactive Systems - Test Generation

Verification of ROS Navigation using Maude

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars.Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.

Autores: Enrique Martin-Martin / Manuel Montenegro / Adrián Riesco / Juan Rodríguez-Hortalá / Rubén Rubio / 
Palabras Clave: Dafny - Formal Verification - Maude - Model checking - Navigation - Rewriting Logic - ROS

Model-checking strategy-controlled rewriting systems

Strategies are a widespread but ambiguous concept in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware model checker built on top of the Maude specification language, based on rewriting logic, and its strategy language.Pendiente de publicación en «International Conference on Formal Structures for Computation and Deduction» (FSCD) 2019. Se envía la versión aceptada. La versión definitiva estará lista a finales de abril.

Autores: Rubén Rubio / Narciso Marti-Oliet / Isabel Pita / Alberto Verdejo / 
Palabras Clave: Maude - Model checking - Rewriting Logic - strategies

Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach

25th International Symposium on Temporal Representation and Reasoning (TIME 2018)Warsaw, Poland 15-17 October 2018.

Autores: Alexander Bolotov / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Branching Temporal Logic - Fairness Constraints - Model checking - One-Pass Tableau

An extension of TRIANGLE testbed with model-based testing (Trabajo ya publicado)

Traditional testing methods for mobile apps focus on detecting execution errors. However, the evolution of mobile networks towards 5G will require additional support for app developers to ensure also the performance and user-experience. Manual testing in a number of scenarios is not enough to satisfy the expectations of the apps final users. This paper presents the testing framework developed in the TRIANGLE project1 that integrates a complete mobile network testbed and a model-based testing approach, which is based on model checking, to automatically evaluate the apps performance in different network scenarios.

Autores: Laura Panizo / Almudena Díaz / Bruno García / 
Palabras Clave: mobile network testbed - Model checking - model-based testing

Context-based Model Checking using SMT-solvers (Trabajo en progreso)

In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.

Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Model checking - SAT - SMT - Solvers - Tableux

Constrained Dynamic Partial Order Reduction (Trabajo ya publicado)

The cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both p·t and t·p must be explored. We present constrained dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of conditional independence —the execution of p and t commutes only when certain independence constraints (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving exponential reductions over existing implementations.

Palabras Clave: Conditional Independence - Dynamic Partial Order Reduction - Model checking - SMT - Static Analysis

Towards a formal framework for analyzing stream processing systems in Maude (Trabajo en progreso)

With the rise of Big Data technologies, distributed stream processing systems (SPS) have gained popularity in the last years. Among these systems Spark Streaming stands out as a particularly attractive option, with a growing adoption in the industry, so we will consider in particular some features of SPS in Spark Streaming. Maude is a high-performance logical framework where other systems can be easily specified and executed. In this paper we show how a Maude specification of Spark Streaming would allow developers to analyze and prove properties on their programs.

Autores: Adrián Riesco / Miguel Palomino / Narciso Martí-Oliet / 
Palabras Clave: Maude - Model checking - Stream processing systems

A characterisation of reliability tools for Software Defined Networks (Trabajo original)

Software Defined Network (SDN) is a new paradigm in networking that introduces great flexibility, allowing the dynamic configuration of parts of the network through centralised programming. SDN has been successfully applied in field networks, and is now being applied to wireless and mobile networks, generating Software Defined Mobile/Wireless networks (SDWNs). SDN can be also combined with Network Function Virtualization (NFV) producing a software network in which the specific hardware is replaced by general purpose computing equipment running SDN and NFV software solutions. This highly programmable and flexible network introduces many challenges from the point of view of reliability (or robustness), and operators need to ensure the same level of confidence as in previous, less flexible deployments. This paper provides a first study of the current tools used to analyse the reliability of SDNs before deployment and/or during the exploitation of the network. Most of these tools offer some kind of automatic verification, supported by algorithms based on formal methods, but they do not differentiate between fixed and mobile/wireless networks. In the paper we provide a number of classifications of the tools to make this selection easier for potential users, and we also identify promising research areas where more effort needs to be made.

Autores: Leticia Lavado / Laura Panizo / María del Mar Gallardo / Pedro Merino / 
Palabras Clave: Communication Networks - Model checking - Reliability - Runtime - Software Defined Network - Verification

Analyzing Hybrid Systems with JPF

Hybrid systems are characterized by combining discrete and continuous behaviors. Verification of hybrid systems is, in general, a difficult task due to the potential complexity of the continuous dynamics. Currently, there are different formalisms and tools which are able to analyze specific types of hybrid systems, model checking being one of the most used approaches. In this paper, we propose an extension of the discrete model checker Java Path Finder in order to analyze hybrid systems. We apply a general methodology which has been successfully used to extend SPIN. This methodology is non-intrusive, and uses external libraries, such as Parma Polyhedra Library, to abstract the continuous behavior of the hybrid system independent to the underlying model checker.

Autores: Laura Panizo / María-del-Mar Gallardo / 
Palabras Clave: Hybrid systems - JPF - Model checking

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada