157 results found
Discrete event controllers are at the heart of many software systems that require continuous operation. Changing these controllers at runtime to cope with changes in its execution environment or system requirements change is a challenging open problem. In this paper we address the problem of dynamic update of controllers in reactive systems. We present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur and in which the underlying system architecture can reconfigure. Our solution uses discrete event controller synthesis to automatically build a controller that guarantees both progress towards update and safe update.
Braberman V, Garbervetsky D, Godoy J, et al., 2018, Testing and validating end user programmed calculated fields, Pages: 827-832
© 2018 Association for Computing Machinery. This paper reports on an approach for systematically generating test data from production databases for end user calculated field program via a novel combination of symbolic execution and database queries. We also discuss the opportunities and challenges that this specific domain poses for symbolic execution and shows how database queries can help complement some of symbolic execution's weaknesses, namely in the treatment of loops and also of path conditions that exceed SMT solver capabilities.
Castano R, Braberman V, Garbervetsky D, et al., 2017, Model checker execution reports, 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Publisher: IEEE, Pages: 200-205, ISSN: 1527-1366
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe canes, and present the notion of execution reports (ERs), which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the ERs produced and the information that can be extracted.
Uchitel S, Orso A, Robillard M, 2017, Foreword, International Conference on Software Engineering, Pages: xvi-xviii
© 2017 ACM. Self-adaptation is often loosely defined as the ability of systems to alter at runtime their behavior in response to changes in their environment, capabilities and goals. Yet we have been building self-adaptive systems have been engineered for decades. The shift from functional, input-output software, to reactive systems stems from the need to have software that can sense its environment, whose behavior is uncertain, and react accordingly. In this talk I will argue that this definition is too broad and that it dilutes a very real need for a particular quality of today’s software systems. I will postulate that a more refined definition of adaptation should emphasize the need for systems to have the ability to react to changes that were originally unforeseen at design time, and to provide assurances on the correctness of these adaptations. How can systems be designed to account for what is unforeseen? I will argue that a key design decision for achieving self-adaptation is to endow systems with the capability of synthesizing at runtime discrete event controllers. Indeed, reactive systems that are requirements and assumptions aware, if extended with run time controller synthesis capabilities are equipped with a powerful infrastructure towards achieving assured self-adaptation. The vision of runtime discrete event controller synthesis at the heart of self-adaptation requires developing appropriate architectures. I will discuss Morph, a reference architecture that can support not only runtime synthesis but also deal with two other crucial elements: (i) interface, requirements and assumption awareness and (ii) runtime controller deployment and dynamic structural and behavioral reconfiguration.
Braberman V, D Ippolito N, Kramer J, et al., 2017, An extended description of MORPH: A reference architecture for configuration and behaviour self-adaptation, SEFSAS, Pages: 377-408, ISSN: 0302-9743
© Springer International Publishing AG 2017. An architectural approach to self-adaptive systems involves runtime change of system configuration (i.e., the system’s components, their bindings and operational parameters) and behaviour update (i.e., component orchestration). The architecture should allow for both configuration and behaviour changes selected from pre-computed change strategies and for synthesised change strategies at run-time to satisfy changes in the environment, changes in the specified goals of the system or in response to failures or degradation in quality attributes, such as performance, of the system itself. Although controlling configuration and behaviour at runtime has been discussed and applied to architectural adaptation, architectures for self-adaptive systems often compound these two aspects reducing the potential for adaptability. In this work we provide an extended description of our proposal for a reference architecture that allows for coordinated yet transparent and independent adaptation of system configuration and behaviour.
Ciolek D, Braberman V, D'Ippolito N, et al., 2017, Interaction Models and Automated Control under Partial Observable Environments, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, Vol: 43, Pages: 19-33, ISSN: 0098-5589
Pavese E, Braberman V, Uchitel S, 2016, Probabilistic Interface Automata, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, Vol: 42, Pages: 843-865, ISSN: 0098-5589
Czemerinski H, Braberman V, Uchitel S, 2016, Behaviour abstraction adequacy criteria for API call protocol testing, SOFTWARE TESTING VERIFICATION & RELIABILITY, Vol: 26, Pages: 211-244, ISSN: 0960-0833
Pavese E, Braberman V, Uchitel S, 2016, Less is More: Estimating Probabilistic Rewards over Partial System Explorations, ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, Vol: 25, ISSN: 1049-331X
Ben-David S, Chechik M, Uchitel S, 2016, Observational Refinement and Merge for Disjunctive MTSs, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Publisher: SPRINGER INT PUBLISHING AG, Pages: 287-303, ISSN: 0302-9743
Rodriguez N, Braberman V, D'Ippolito N, et al., 2016, 21/2-PLAYER GENERALIZED REACTIVITY (1) GAMES, 55th IEEE Conference on Decision and Control (CDC), Publisher: IEEE, Pages: 6996-7001, ISSN: 0743-1546
Ciolek D, Braberman V, D'Ippolito N, et al., 2016, Directed Controller Synthesis of Discrete Event Systems: Taming Composition with Heuristics, 55th IEEE Conference on Decision and Control (CDC), Publisher: IEEE, Pages: 4764-4769, ISSN: 0743-1546
Alrajeh D, Russo A, Uchitel S, et al., 2016, Logic-based Learning in Software Engineering, 38th IEEE/ACM International Conference on Software Engineering Companion (ICSE), Publisher: IEEE, Pages: 892-893
Colson K, Dupuis R, Montrieux L, et al., 2016, Reusable Self-Adaptation through Bidirectional Programming, 11th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Publisher: IEEE, Pages: 4-15
Nahabedian L, Braberman V, D'Ippolito N, et al., 2016, Assured and Correct Dynamic Update of Controllers, 11th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Publisher: IEEE, Pages: 96-107
Alrajeh D, van Lamsweerde A, Kramer J, et al., 2016, Risk-Driven Revision of Requirements Models, 38th IEEE/ACM International Conference on Software Engineering (ICSE), Publisher: IEEE, Pages: 855-865, ISSN: 0270-5257
Uchitel S, Braberman VA, D'Ippolito N, 2016, Runtime Controller Synthesis for Self-Adaptation: Be Discrete! (Keynote), 11th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Publisher: IEEE, Pages: 1-3
Braberman V, D'Ippolito N, Kramer J, et al., 2015, MORPH: A reference architecture for configuration and behaviour self-adaptation, Pages: 9-16
© 2015 ACM. An architectural approach to self-adaptive systems involves runtime change of system configuration (i.e., the system's components, their bindings and operational parameters) and behaviour update (i.e., component orchestration). Thus, dynamic reconfiguration and discrete event control theory are at the heart of architectural adaptation. Although controlling configuration and behaviour at runtime has been discussed and applied to architectural adaptation, architectures for self-adaptive systems often compound these two aspects reducing the potential for adaptability. In this paper we propose a reference architecture that allows for coordinated yet transparent and independent adaptation of system configuration and behaviour.
D'Ippolito N, Braberman V, Sykes D, et al., 2015, Robust degradation and enhancement of robot mission behaviour in unpredictable environments, Pages: 26-33
© 2015 ACM. Temporal logic based approaches that automatically generate controllers have been shown to be useful for mission level planning of motion, surveillance and navigation, among others. These approaches critically rely on the validity of the environment models used for synthesis. Yet simplifying assumptions are inevitable to reduce complexity and provide mission-level guarantees; no plan can guarantee results in a model of a world in which everything can go wrong. In this paper, we show how our approach, which reduces reliance on a single model by introducing a stack of models, can endow systems with incremental guarantees based on increasingly strengthened assumptions, supporting graceful degradation when the environment does not behave as expected, and progressive enhancement when it does.
Duarte LM, Kramer J, Uchitel S, 2015, Using contexts to extract models from code, Software & Systems Modeling, Vol: 16, Pages: 523-557, ISSN: 1619-1366
Behaviour 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.
Krka I, D'Ippolito N, Medvidovic N, et al., 2014, Revisiting Compatibility of Input-Output Modal Transition Systems, 19th International Symposium on Formal Methods (FM), Publisher: SPRINGER-VERLAG BERLIN, Pages: 367-381, ISSN: 0302-9743
Degiovanni R, Alrajeh D, Aguirre N, et al., 2014, Automated Goal Operationalisation Based on Interpolation and SAT SolvingAutomated Goal Operationalisation Based on Interpolation and SAT Solving, 36th International Conference on Software Engineering (ICSE), Publisher: ASSOC COMPUTING MACHINERY, Pages: 129-139
Krka I, D'Ippolito N, Medvidović N, et al., 2014, Revisiting compatibility of input-output modal transition systems, Pages: 367-381, ISSN: 0302-9743
Modern software systems are typically built of components that communicate through their external interfaces. The external behavior of a component can be effectively described using finite state automata-based formalisms. Such component models can then used for varied analyses. For example, interface automata, which model the behavior of components in terms of component states and transitions between them, can be used to check whether the resulting system is compatible. By contrast, partial-behavior modeling formalisms, such as modal transition systems, can be used to capture and then verify properties of sets of prospective component implementations that satisfy an incomplete requirements specification. In this paper, we study how pairwise compatibility should be defined for partial-behavior models. To this end, we describe the limitations of the existing compatibility definitions, propose a set of novel compatibility notions for modal interface automata, and propose efficient, correct, and complete compatibility checking procedures © 2014 Springer International Publishing Switzerland.
D'Ippolito N, Braberman V, Piterman N, et al., 2014, Controllability in partial and uncertain environments, Pages: 52-61, ISSN: 1550-4808
© 2014 IEEE. Controller synthesis is a well studied problem that attempts to automatically generate an operational behaviour model of the system-to-be that satisfies a given goal when deployed in a given domain model that behaves according to specified assumptions. A limitation of many controller synthesis techniques is that they require complete descriptions of the problem domain. This is limiting in the context of modern incremental development processes when a fully described problem domain is unavailable, undesirable or uneconomical. Previous work on Modal Transition Systems (MTS) control problems exists, however it is restricted to deterministic MTSs and deterministic Labelled Transition Systems (LTS) implementations. In this paper we study the Modal Transition System Control Problem in its full generality, allowing for nondeterministic MTSs modelling the environment's behaviour and nondeterministic LTS implementations. Given an nondeterministic MTS we ask if all, none or some of the nondeterministic LTSs it describes admit an LTS controller that guarantees a given property. We show a technique that solves effectively the MTS realisability problem and it can be, in some cases, reduced to deterministic control problems. In all cases the MTS realisability problem is in same complexity class as the corresponding LTS problem.
D'Ippolito N, Braberman V, Kramer J, et al., 2014, Hope for the Best, Prepare for the Worst: Multi-tier Control for Adaptive Systems, 36th International Conference on Software Engineering (ICSE), Publisher: ASSOC COMPUTING MACHINERY, Pages: 688-699
Uchitel S, Alrajeh D, Ben-David S, et al., 2013, Supporting incremental behaviour model elaboration, Computer Science - Research and Development, Vol: 28, Pages: 279-293, ISSN: 1865-2034
Behaviour model construction remains a difficult and labour intensive task which hinders the adoption of model-based methods by practitioners. We believe one reason for this is the mismatch between traditional approaches and current software development process best practices which include iterative development, adoption of use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modelling and analysis in the presence of partial information about system behaviour. Our objective is to address the limitations of behaviour modelling and analysis by shifting the focus from traditional behaviour models and verification techniques that require full behaviour information to partial behaviour models and analysis techniques, that drive model elaboration rather than asserting adequacy. We aim to develop sound theory, techniques and tools that facilitate the construction of partial behaviour models through model synthesis, enable partial behaviour model analysis and provide feedback that prompts incremental elaboration of partial models. In this paper we present how the different research threads that we have and currently are developing help pursue this vision as part of the "Partial Behaviour Modelling - Foundations for Iterative Model Based Software Engineering" Starting Grant funded by the ERC. We cover partial behaviour modelling theory and construction, controller synthesis, automated diagnosis and refinement, and behaviour validation. © 2012 Springer-Verlag Berlin Heidelberg.
Ben-David S, Chechik M, Uchitel S, 2013, Merging partial behaviour models with different vocabularies, Pages: 91-105, ISSN: 0302-9743
Modal transition systems (MTSs) and their variants such as Disjunctive MTSs (DMTSs) have been extensively studied as a formalism for partial behaviour model specification. Their semantics is in terms of implementations, which are fully specified behaviour models in the form of Labelled Transition Systems. A natural operation for these models is that of merge, which should yield a partial model which characterizes all common implementations. Merging has been studied for models with the same vocabularies; however, to enable composition of specifications from different viewpoints, merging of models with different vocabularies must be supported as well. In this paper, we first prove that DMTSs are not closed under merge for models with different vocabularies. We then define an extension to DMTS called rDMTS, for which we describe a first exact algorithm for merging partial models, provided they satisfy an easily checkable compatibility condition. © 2013 Springer-Verlag.
Sibay GE, Braberman V, Uchitel S, et al., 2013, Synthesizing Modal Transition Systems from Triggered Scenarios, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, Vol: 39, Pages: 975-1001, ISSN: 0098-5589
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.