Resultados de búsqueda para Model checking

La referencia completa es:Abuin, A., Díaz de Cerio, U., Hermo, M. and Lucio, P., Verified Model Checking for Conjunctive Positive Logic. SN COMPUTER SCIENCE, VOL 2, Springer 2021. https://doi.org/10.1007/s42979-020-00417-3

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.

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.

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.

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

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.

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.

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.

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.

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.