1,721,016 research outputs found
Automated support for diagnosis and repair
Full text linkModel checking and logic-based learning together deliver automated support, especially in adaptive and autonomous systems.Fil: Alrajeh, Dalal . Imperial College London; Reino UnidoFil: Russo, Alessandra. Imperial College London; Reino UnidoFil: Kramer, Jeff . Imperial College London; Reino UnidoFil: Uchitel, Sebastian. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Synthesizing nonanomalous event-based controllers for liveness goals
Full text linkWe present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behaviour models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modelled carefully in order to avoid synthesising anomalous behaviour models. We characterise non-anomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.Fil: D'ippolito, Nicolás Roque. Imperial College London; Reino Unido. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Braberman, Victor Adrian. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Piterman, Nir. University of Leicester; Reino UnidoFil: Uchitel, Sebastian. Imperial College London; Reino Unido. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Exploring inconsistencies between modal transition systems
Full text linkIt is commonplace to have multiple behaviour models that describe the same system but have been produced by different stakeholders or synthesized from different sources. Although in practice, such models frequently exhibit inconsistencies, there is a lack of tool support for analyzing them. There are two key difficulties in explaining why two behavioural models are inconsistent: (1) explanations often require branching structures rather than linear traces, or scenarios; and (2) there can be multiple sources of inconsistency and many different ways of explaining each one. In this paper, we present an approach that supports exploration of inconsistencies between modal transition systems, an extension to labelled transition systems. We show how to produce sound graphical explanations for inconsistencies, how to compactly represent all possible explanations in a composition of the models being compared, and how modelers can use this composition to explore the explanations encoded therein.Fil: Sassolas, Mathieu. Universite Pierre et Marie Curie; FranciaFil: Chechik, Marsha. University of Toronto; CanadáFil: Uchitel, Sebastian. Imperial College London; Reino Unido. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Using contexts to extract models from code
Full text linkBehaviour models facilitate the understanding and analysis of software systems by providing an abstract view of their behaviours and also by enabling the use of validation and verification techniques to detect errors. However, depending on the size and complexity of these systems, constructing models may not be a trivial task, even for experienced developers. Model extraction techniques can automatically obtain models from existing code, thus reducing the effort and expertise required of engineers and helping avoid errors often present in manually constructed models. Existing approaches for model extraction often fail to produce faithful models, either because they only consider static information, which may include infeasible behaviours, or because they are based only on dynamic information, thus relying on observed executions, which usually results in incomplete models. This paper describes a model extraction approach based on the concept of contexts, which are abstractions of concrete states of a program, combining static and dynamic information. Contexts merge some of the advantages of using either type of information and, by their combination, can overcome some of their problems. The approach is partially implemented by a tool called LTS Extractor, which translates information collected from execution traces produced by instrumented Java code to labelled transition systems (LTS), which can be analysed in an existing verification tool. Results from case studies are presented and discussed, showing that, considering a certain level of abstraction and a set of execution traces, the produced models are correct descriptions of the programs from which they were extracted. Thus, they can be used for a variety of analyses, such as program understanding, validation, verification, and evolution.Fil: Duarte, Lucio Mauro. Federal University of Rio Grande do Sul; BrasilFil: Kramer, Jeff. Imperial College London; Reino UnidoFil: Uchitel, Sebastian. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Imperial College London; Reino Unid
Elaborating requirements using model checking and inductive learning
Full text linkThe process of requirements engineering includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer´s knowledge of the domain and the envisioned system.Fil: Uchitel, Sebastian. Imperial College London; Reino Unido. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; ArgentinaFil: Alrajeh, Dalal. Imperial College London; Reino UnidoFil: Kramer, Jeff. Imperial College London; Reino UnidoFil: Russo, Alessandra. Imperial College London; Reino Unid
Deriving event-based transition systems from goal-oriented requirements models
Full text linkGoal-oriented methods are increasingly popular for elaborating software requirements. They offer systematic support for incrementally building intentional, structural, and operational models of the software and its environment. Event-based transition systems on the other hand are convenient formalisms for reasoning about software behaviour at the architectural level. The paper relates these two worlds by presenting a technique for translating formal specification of software operations built according to the KAOS goal-oriented method into event-based transition systems analysable by the LTSA toolset. The translation involves moving from a declarative, state-based, timed, synchronous formalism typical of requirements modelling languages to an operational, event-based, untimed, asynchronous one typical of architecture description languages. The derived model can be used for the formal analysis and animation of KAOS operation models in LTSA. The paper also provides insights into the two complementary formalisms, and shows that the use of synchronous temporal logic for requirements specification hinders a smooth transition from requirements to software architecture models.Fil: Letier, Emmanuel. University College London; Estados Unidos. London Software Systems; Reino UnidoFil: Kramer, Jeff. University College London; Estados Unidos. London Software Systems; Reino UnidoFil: Magee, Jeff. Imperial College London; Reino Unido. London Software Systems; Reino UnidoFil: Uchitel, Sebastian. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria; Argentina. Universidad de Buenos Aires. Facultad de Ingeniería. Departamento de Computacion; Argentina. Imperial College London; Reino Unido. London Software Systems; Reino Unid
Correct and efficient UAV missions based on temporal planning and in-flight hybrid simulations
No full textController synthesis has been successfully applied in UAV applications, to construct a mission plan that is guaranteed to be correct with respect to a user-provided specification. Albeit being correct, these plans may not be optimal in the vehicle´s trajectory, battery consumption, or other criteria which the user may consider relevant. A possibility would be to apply a quantitative synthesis approach where the target is to compute efficient plans before the mission, at a higher cost of complexity and potential limitations in the optimization goals to achieve. As an alternative, in this paper we propose doing the plan optimization in-flight. For this, we use available tools that synthesize controllers with multiple controllable choices and later select among these choices in-flight using hybrid simulations ranking them according to the optimization objective. We present the advantages of our approach and validate them using software-in-the-loop simulation with typical UAV mission scenarios.Fil: Pecker Marcosig, Ezequiel. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación; ArgentinaFil: Zudaire, Sebastián Alfredo. Comisión Nacional de Energía Atómica. Gerencia del Área de Energía Nuclear. Instituto Balseiro; ArgentinaFil: Castro, Rodrigo Daniel. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación; ArgentinaFil: Uchitel, Sebastian. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación; Argentina. Imperial College London; Reino Unid
Enabledness-based Testing of Object Protocols
No full textA significant proportion of classes in modern software introduce or use object protocols, prescriptions on the temporal orderings of method calls on objects. This article studies search-based test generation techniques that aim to exploit a particular abstraction of object protocols (enabledness preserving abstractions (EPAs)) to find failures. We define coverage criteria over an extension of EPAs that includes abnormal method termination and define a search-based test case generation technique aimed at achieving high coverage. Results suggest that the proposed case generation technique with a fitness function that aims at combined structural and extended EPA coverage can provide better failure-detection capabilities not only for protocol failures but also for general failures when compared to random testing and search-based test generation for standard structural coverage.Fil: Godoy, Javier Ignacio. Universidad Nacional de General Sarmiento; ArgentinaFil: Galeotti, Juan Pablo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Uchitel, Sebastian. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigación en Ciencias de la Computación; Argentin
Enabledness-based program abstractions for behavior validation
Full text linkCode artifacts that have nontrivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. This work addresses the problem of validating if API implementations provide their intended behavior when descriptions of this behavior are informal, partial, or nonexistent. The proposed approach addresses this problem by generating abstract behavior models which resemble typestates. These models are statically computed and encode all admissible sequences of method calls. The level of abstraction at which such models are constructed has shown to be useful for validating code artifacts and identifying findings which led to the discovery of bugs, adjustment of the requirements expected by the engineer to the requirements implicit in the code, and the improvement of available documentation.Fil: de Caso, Guido. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Braberman, Victor Adrian. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Garbervetsky, Diego David. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Uchitel, Sebastian. Universidad de Buenos Aires; Argentina. Imperial College London; Reino Unido. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Applying LSCs to the Specification of an Air Traffic Control System
No full textWe demonstrate the use of the language of Live Sequence Charts (LSCs) for specifying part of the air traffic control system CTAS (Center TRACON Automation System). We use a recent extension of LSCs to handle symbolic instances, allowing an instance to be associated with a class rather than with an object. This allows us to specify scenario-based requirements that could not have been expressed using concrete objects only. This work can form the basis for applying execution, verification and synthesis methods developed for LSCs, on a real-world case study
- …
