1,721,091 research outputs found
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
Evolving Intentions: Support for Modeling and Reasoning about Requirements that Change over Time
Full text linkIn early-phase requirements engineering, modeling stakeholder goals and intentions helps stakeholders understand the problem context and evaluate tradeoffs, by exploring possible "what if" questions. Prior research allows modelers to make evaluation assignments to desired goals and generate possible selections for task and dependency alternatives, but this treats models as static snapshots, where once the evaluation of the fulfillment of an intention is determined, it remains constant. Using these techniques stakeholders are unable to reason about possible evolutions, leaving questions about project viability unanswered when the fulfillment of goals or availability of components is not guaranteed in the future.
In this dissertation, we propose Evolving Intentions: a framework for specifying, modeling, and reasoning about goals that change over time, enabling stakeholders to explore model evolution. We present Evolving Intentions in the context of both the i* and Tropos goal modeling languages. We specify a set of functions that define how intentions and relationships evolve, and use simulation strategies for asking a variety of "what if" questions about such changes.
We present GrowingLeaf and BloomingLeaf, two web-based goal modeling and analysis tools that implement this technique for iStar and Tropos models, respectively. Using the development of GrowingLeaf as an example, we demonstrate that this technique is effective for debugging goal models and answering stakeholder questions, and show the analysis to be scalable for representative goal models. We describe a between-subjects controlled experiment that empirically validated the effectiveness of our approach and tool usability. We also report on the applicability and effectiveness, of our technique on a substantial case, where we use historical data and rational reconstruction to understand how a project evolved in the past, and explore alternative futures.Ph.D
Reasoning with Constraints: Decision Procedures, Witnesses and Applications
Full text linkLogic, and constraint satisfiability are key ingredients in automated reasoning for solving real-world software engineering problems. A wide range of reasoning tasks such as model checking, verification, and synthesis can be encoded as constraint satisfaction problems in a suitable logic and solved with algorithms that efficiently decide their satisfiability.
To enable the satisfiability-based approach to reason about a problem, some key questions need to be addressed: (1) What is a suitable logic to model the essence of the problem and how to decide its satisfiability? (2) How to trust correctness of the satisfiability result and explain its cause? and (3) How to encode reasoning tasks of interest as satisfiability problems in the logic? In this thesis, we investigate these questions, considering subsets of first-order logic and addressing problems of different complexities.
First, we study the problem of reasoning about infinite state systems through the lens of a variance of FOL, first-order logic with quantifier over relational objects (FOL*). The logic introduces a novel concept: relational objects, to capture system operations of unbounded sizes with time and data from unbounded domains. We develop an efficient semi-decision procedure for FOL* satisfiability with incremental approximations. We also extend FOL* to support aggregation functions over relational objects to enable the specification and efficient reasoning about global properties.
Next, we address the question of validating the correctness of satisfiability results. We propose approaches to support the proof of unsatisfiability (UNSAT) for FOL* and finite-domain monotonic theories (SMMT). To efficiently and soundly verify the unsatisfiability of FOL* and SMMT formulas, we formalize the theory semantics as a set of derivation rules and capture the reasoning towards unsatisfiability as derivation sequences. The correctness of the derivation can be verified on the premise that each derivation step can be efficiently checked against the derivation rules. By checking the UNSAT proof, we can establish a correctness guarantee for the unsatisfiability result and diagnose the causes of unsatisfiability.
Then, we apply FOL* satisfiability to automatically reason about normative requirements written in domain-specific languages. We capture the semantics of requirements in FOL* and encode the tasks of checking the well-formedness properties into FOL* queries. We use the FOL* satisfiability result, including the satisfying solution, and UNSAT diagnosis to provide user-friendly diagnostics to pinpoint the causes of well-formedness issues.
Finally, we conclude this thesis by discussing the limitations and future works.Ph.D
Managing Software Evolution Through Semantic History Slicing
Full text linkSoftware change histories are results of incremental updates made by developers. As a byproduct of the software development process, change history is surprisingly useful for understanding, maintaining and reusing software. However, traditional commit-based sequential organization of version histories lacks semantic structure and thus is insufficient for many development tasks that require high-level, semantic understanding of program functionality.
In this dissertation, we propose a new semantics-based view of software version histories, where a set of related changes satisfying a common high level property (also known as slicing criteria) is recognized as a semantic history slice. As one concrete instantiation, test cases exercising a software functionality can be used as slicing criteria to identify changes implementing the particular functionality.
Specifically, we present a family of automated techniques which analyze the semantics of historical changes and assist developers in many practical software evolution tasks. First, we introduce CSlicer, an efficient static history slicing algorithm which requires only a one-time effort for compilation and test execution. It mostly relies on static analysis of dependencies between change sets and is therefore inexpensive in terms of running time but can be imprecise. Second, we present Definer, a dynamic history slicing algorithm based on delta refinement. It executes tests multiple times and observes the test results while attempting to shorten the history slices iteratively. The semantic slices found by the dynamic approach are guaranteed to be minimal, but the running time can be much longer. Finally, we describe the design and implementation of a Web-based semantic slicing framework CSlicerCloud which aims to find balance between performance and precision, unifies different history slicing algorithms and provides software developers a flexible and ready-to-use environment for various evolution management tasks.
We have successfully applied the history slicing techniques in many development tasks including creating focused pull requests, back-porting bug fixes, locating feature implementations and building feature models to assist evolution understanding. For validation, we evaluate our approaches on a benchmark of developer-annotated version history instances obtained from real-world open-source software projects from GitHub.Ph.D
Approximation and Refinement Techniques for Hard Model-checking Problems
Full text linkFormal verification by model checking verifies whether a system satisfies some given correctness properties, and is intractable in general. We focus on several problems originating from the usage of model checking and from the inherent complexity of model checking itself. We propose approximation and iterative refinement techniques and demonstrate that they help in making these problems tractable on practical cases. Vacuity detection is one of the problems, relating to the trivial satisfaction of properties. A similar problem is query solving, useful in model exploration, when properties of a system are not fully known and are to be discovered rather than checked. Both of these problems have solution spaces structured as lattices and can be solved by model checking using those lattices. The lattices, in the most general formulation of these problems, are too complex to be implemented efficiently. We introduce a general approximation framework for model checking with lattices and instantiate this framework for the two problems, leading to algorithms and implementations that can obtain efficiently partial answers to the problems. We also introduce refinement techniques that consider incrementally larger lattices and compute even the partial answers gradually, to further abate the size explosion of the problems. Another problem we consider is the state-space explosion of model checking. The size of system models is exponential in the number of state variables and that renders model checking intractable. We consider systems composed of several components running concurrently. For such systems, compositional verification checks components individually to avoid composing an entire system. Model checking an individual component uses assumptions about the other components. Smaller assumptions lead to smaller verification problems. We introduce iterative refinement techniques that improve the assumptions generated by previous automated approaches. One technique incrementally refines the interfaces between components in order to obtain smaller assumptions that are sufficient to prove a given property. The smaller assumptions are approximations of the assumption that would be obtained without our interface refinement. Another technique computes assumptions as abstractions of components, as an alternative to current approaches that learn assumptions from counterexamples. Our abstraction refinement has the potential to compute smaller nondeterministic assumptions, in contrast to the deterministic assumptions learned by current approaches. We confirm experimentally the benefits of our new approximation and refinement techniques.Ph
Reliability Analysis of Machine Vision Components in Safety-critical Systems against Human Performance
Full text linkMachine Learning (ML) has revolutionized the field of Computer Vision (CV) by enabling the automation of vision tasks, such as detecting objects in images. Consequently, CV models have been deployed as Machine Vision Components (MVCs) in safety-critical systems such as self-driving cars, where undesired behaviors can lead to fatal accidents. For such systems, the MVC performing the vision task represents a critical function for the overall system safety. Therefore, analyzing MVCs, and assuring their safety and reliability have become a necessity for building trust in their application in safety-critical domains.
Safety analysis depends on clearly defined requirements specifying the expected behaviour. However, vision tasks are difficult to specify and the inability to specify clear requirements is the reason to use ML in the first place. As a first step towards safe and reliable MVCs, one needs to define what it means for an MVC to be correct, which then allows checking its correctness prior to system deployment. In this dissertation, we specifically focus on one correctness property, MVC reliability against scene changes. We study whether the performance of an MVC remains reliably unaffected by potential scene changes that can occur in the deployment environment. We aim to devise methods to specify and analyze MVC reliability in the context of system safety.
Since MVCs are used in systems to automate tasks normally performed by humans, they should be at least as good as humans to be trustworthy. To enable the evaluation of MVC reliability against humans, we present a method to establish human performance as a baseline reference in the form of reliability requirements. Satisfaction of these requirements can be automatically checked thus allowing analysis of MVC reliability and studying the connection between MVC reliability and system safety. Our proposed method first identifies image transformations for simulating scene changes in images, then obtains MVC reliability requirements using human performance as a reference, and next checks whether an MVC satisfies the requirements, and finally, we present a process for analyzing MVC reliability in the context of system safety by integrating reliability into the safety assurance process for autonomous systems.Ph.D
Abstraction for Verification and Refutation in Model Checking
No full textModel checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation.
We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking.
Our second study investigates model checking of \emph{recursive} programs.
Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing
abstract analysis in our software model checker to handle recursive programs.
A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them.
Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.Ph
Abstraction for Verification and Refutation in Model Checking
Full text linkModel checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation.
We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking.
Our second study investigates model checking of \emph{recursive} programs.
Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing
abstract analysis in our software model checker to handle recursive programs.
A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them.
Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.Ph
- …
