Imperial College London

Dr. Sebastian Uchitel

Faculty of EngineeringDepartment of Computing

Reader in Software Engineering
 
 
 
//

Contact

 

+44 (0)20 7594 8269s.uchitel Website

 
 
//

Location

 

573Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

163 results found

Nahabedian L, Braberman V, DIppolito N, Honiden S, Kramer J, Tei K, Uchitel Set al., Dynamic update of discrete event controllers, IEEE Transactions on Software Engineering, ISSN: 0098-5589

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.

Journal article

Ciolek D, Braberman V, D'Ippolito N, Sardina S, Uchitel Set al., Compositional Supervisory Control via Reactive Synthesis and Automated Planning, IEEE Transactions on Automatic Control, ISSN: 0018-9286

Journal article

Uchitel S, Braberman V, Kramer J, Nahabedian L, D'Ippolito Net al., Dynamic reconfiguration of business processes, 17th Int. Conference on Business Process Management (BPM 2019), Publisher: Springer Verlag, ISSN: 0302-9743

Organisations require that their business processes reflecttheir evolving practices by maintaining compliance with their policies,strategies and regulations. Designing workflows which satisfy these re-quirements is complex and error-prone. Business process reconfigurationis even more challenging as not only a new workflow must be devisedbut also an understanding of how the transition between the old andnew workflow must be managed. Transition requirements can includeboth domain independent, such as delayed and immediate change, oruser-defined domain specific requirements. In this paper we present afully automated technique which uses control synthesis to not only pro-duce correct-by-construction workflows from business process require-ments but also to compute a reconfiguration process that guarantees theevolution from an old workflow to a new one while satisfying any user-defined transition requirements. The approach is validated using threeexamples from the BPM Academic Initiative described as Dynamic Con-dition Response Graphs which we reconfigured for a variety of transitionsrequirements.

Conference paper

Van Der Hoek A, Uchitel S, 2019, Message from the technical briefings chairs of ICSE 2019

Conference paper

Postolski I, Braberman V, Garbervetsky D, Uchitel Set al., 2019, Simulator-based diff-time performance testing, Pages: 81-84

© 2019 IEEE. We propose an approach for rapid detection of performance regressions using a simulator built from the original program by dynamic slicing and a certificate built using static analysis that generalizes its correctness. We discuss two case-studies that illustrate the potential benefits of the proposal.

Conference paper

Braberman V, Garbervetsky D, Godoy J, Uchitel S, De Caso G, Perez I, Perez Set al., Testing and Validating End User Programmed Calculated Fields, 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Conference paper

Castano R, Braberman V, Garbervetsky D, Uchitel Set 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.

Conference paper

Uchitel S, Orso A, Robillard M, 2017, Foreword, International Conference on Software Engineering, Pages: xvi-xviii

Conference paper

Uchitel S, 2017, Runtime Controller Synthesis for Self-Adaptation: Discretion Required, 10th Innovations in Software Engineering Conference (ISEC), Publisher: ASSOC COMPUTING MACHINERY, Pages: 1-1

Conference paper

Braberman V, D Ippolito N, Kramer J, Sykes D, Uchitel Set 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.

Conference paper

Ciolek D, Braberman V, D'Ippolito N, Uchitel Set al., 2016, Directed Controller Synthesis of discrete event systems: Taming composition with heuristics, 2016 IEEE 55th Conference on Decision and Control, CDC 2016, Publisher: IEEE, Pages: 4764-4769

This paper presents a Directed Controller Synthesis (DCS) technique for discrete event systems. This DCS method explores the solution space for reactive controllers guided by a domain-independent heuristic. The heuristic is derived from an efficient abstraction of the environment based on the componentized way in which complex environments are described. Then by building the composition of the components on-the-fly DCS obtains a solution by exploring a reduced portion of the state space. This work focuses on untimed discrete event systems with safety and co-safety (i.e. reachability) goals. An evaluation for the technique is presented comparing it to other well-known approaches to controller synthesis (based on symbolic representation and compositional analyses).

Conference paper

Rodriguez N, Braberman V, D'Ippolito N, Uchitel Set al., 2016, 21/2-player generalized reactivity (1) games, 2016 IEEE 55th Conference on Decision and Control, CDC 2016, Publisher: Institute of Electrical and Electronics Engineers (IEEE), Pages: 6996-7001

We introduce a new class of 21/2-player games, the 21/2-player GR(1) games, that allows for solving problems of stochastic nature by adding a probabilistic component to simple 2-player GR(1) games. Further, we present an efficient approach for solving qualitative 21/2-player GR(1) games with polynomial-time complexity. Our approach is based on a reduction from 21/2-player GR(1) games to 2-player GR(1) games that allows for solving the game and constructing, from a sure winning strategy for player □ (resp. L) in a 2-player GR(1) game, an almost-sure (resp. positively) winning strategy for its corresponding 21/2-player GR(1) game. Key to the effectiveness of the proposed approach is the fact that the reduction generates a 2-player game that is linearly larger than the original 21/2-player game, more precisely, it is linear with respect to the number of probabilistic states in the 21/2-player GR(1) game.

Conference paper

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, Pages: 287-303, ISSN: 0302-9743

Modal Transition System (MTS) is a well studied formal-ism for partial model specification. It allows a modeller to distinguishbetween required, prohibited and possible transitions. Disjunctive MTS(DMTS) is an extension of MTS that has been getting attention in re-cent years. A key concept for (D)MTS isrefinement, supporting a devel-opment process where abstract specifications are gradually refined intomore concrete ones. Refinement comes in different flavours:strong,ob-servational(whereτ-labelled transitions are taken into account), andalphabet(allowing the comparison of models defined on different alpha-bets). Another important operation on (D)MTS is that ofmerge: giventwo modelsMandN, their merge is a modelPwhich refines bothMandN, and which is the least refined one.In this paper, we fill several missing parts in the theory of DMTS refine-ment and merge. First and foremost, we define observational refinementfor DMTS. While an elementary concept, such a definition is missingfrom the literature to the best of our knowledge. We prove that our defi-nition is sound and that it complies with all relevant definitions from theliterature. Based on the new observational refinement for DMTS, we ex-amine the question of DMTS merge, which was defined so far for strongrefinement only. We show that observational merge can be achieved as anatural extension of the existing algorithm for strong merge of DMTS.For alphabet merge however, the situation is different. We prove thatDMTSs do not have a merge under alphabet refinement.

Conference paper

Alrajeh D, Lamsweerde A, Kramer J, Russo A, Uchitel Set al., 2016, Risk-driven revision of requirements models, 38th International Conference on Software Engineering (ICSE '16), Publisher: Association for Computing Machinery, Pages: 855-865, ISSN: 0270-5257

Requirements incompleteness is often the result of unanticipated adverse conditions which prevent the software and its environment from behaving as expected. These conditions represent risks that can cause severe software failures. The identification and resolution of such risks is therefore a crucial step towards requirements completeness. Obstacle analysis is a goal-driven form of risk analysis that aims at detecting missing conditions that can obstruct goals from being satisfied in a given domain, and resolving them.This paper proposes an approach for automatically revising goals that may be under-specified or (partially) wrong to resolve obstructions in a given domain. The approach deploys a learning-based revision methodology in which obstructed goals in a goal model are iteratively revised from traces exemplifying obstruction and non-obstruction occurrences. Our revision methodology computes domain-consistent, obstruction-free revisions that are automatically propagated to other goals in the model in order to preserve the correctness of goal models whilst guaranteeing minimal change to the original model. We present the formal foundations of our learning-based approach, and show that it preserves the properties of our formal framework. We validate it against the benchmarking case study of the London Ambulance Service.

Conference paper

Alrajeh D, Russo A, Uchitel S, Kramer Jet al., 2016, Logic-based learning in software engineering, 38th IEEE/ACM International Conference on Software Engineering Companion (ICSE), Publisher: IEEE, Pages: 892-893

In recent years, research efforts have been directed towards the use of Machine Learning (ML) techniques to support and automate activities such as program repair, specification mining and risk assessment. The focus has largely been on techniques for classification, clustering and regression. Although beneficial, these do not produce a declarative, interpretable representation of the learned information. Hence, they cannot readily be used to inform, revise and elaborate software models. On the other hand, recent advances in ML have witnessed the emergence of new logic-based learning approaches that differ from traditional ML in that their output is represented in a declarative, rule-based manner, making them well-suited for many software engineering tasks.In this technical briefing, we will introduce the audience to the latest advances in logic-based learning, give an overview of how logic-based learning systems can successfully provide automated support to a variety of software engineering tasks, demonstrate the application to two real case studies from the domain of requirements engineering and software design and highlight future challenges and directions.

Conference paper

Nahabedian L, Braberman V, D'Ippolito N, Honiden S, Kramer J, Tei K, Uchitel Set al., 2016, Assured and correct dynamic update of controllers, 11th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS '16), Publisher: ACM, Pages: 96-107

In many application domains, continuous operation is a desirable attribute for software-intensive systems. As the environment or system requirements change, so the system should change and adapt without stopping or unduly disturbing its operation. There is, therefore, a need for sound engineering techniques that can cope with dynamic change. In this paper we address the problem of dynamic update of controllers in reactive systems when the specification (environment assumptions, requirements and interface) of the current system changes. 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. Indeed, using controller synthesis we show how to automatically build a controller that guarantees both progress towards update and safe update. Seven case studies have been implemented to validate the approach.

Conference paper

Ciolek D, Braberman V, D'Ippolito N, Piterman N, Uchitel Set al., 2016, Interaction Models and Automated Control under Partial Observable Environments, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, Vol: 43, Pages: 19-33, ISSN: 0098-5589

The problem of automatically constructing a software component such that when executed in a given environment satisfies a goal, is recurrent in software engineering. Controller synthesis is a field which fits into this vision. In this paper we study controller synthesis for partially observable LTS models. We exploit the link between partially observable control and non-determinism and show that, unlike fully observable LTS or Kripke structure control problems, in this setting the existence of a solution depends on the interaction model between the controller-to-be and its environment. We identify two interaction models, namely Interface Automata and Weak Interface Automata, define appropriate control problems and describe synthesis algorithms for each of them.

Journal article

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: 1557-7392

Model-based reliability estimation of systems can provide useful insights early in the development process.However, computational complexity of estimating metrics such as mean time to first failure (MTTF),turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, spaceand precision. In this paper we present an alternative to exhaustive model exploration–as in probabilisticmodel checking–and partial random exploration–as in statistical model checking. Our hypothesis is thata (carefully crafted) partial systematic exploration of a system model can provide better bounds for thesequantitative model metrics at lower computation cost. We present a novel automated technique for metricestimation that combines simulation, invariant inference and probabilistic model checking. Simulationproduces a probabilistically relevant set of traces from which a state invariant is inferred. The invariantcharacterises a partial model which is then exhaustively explored using probabilistic model checking. Wereport on experiments that suggest that metric estimation using this technique (for both fully probabilisticmodels and those exhibiting non-determinism) can be more effective than (full model) probabilistic andstatistical model checking especially for system models where the events of interest are rare.

Journal article

Pavese E, Braberman V, Uchitel S, 2016, Probabilistic Interface Automata, IEEE Transactions on Software Engineering, Vol: 42, Pages: 843-865, ISSN: 0098-5589

System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. T-

Journal article

Colson K, Dupuis R, Montrieux L, Hu Z, Uchitel S, Schobbens P-Yet 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

Conference paper

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

Conference paper

Czemerinski H, Braberman V, Uchitel S, 2015, Behaviour abstraction adequacy criteria for API call protocol testing, Software Testing Verification & Reliability, Vol: 26, Pages: 211-244, ISSN: 1099-1689

Code artefacts that have non-trivial 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. Testing such code artefacts to gain confidence that they conform to their intended protocols is an important and challenging problem. This paper proposes conformance testing adequacy criteria based on covering an abstraction of the intended behaviour's semantics. Thus, the criteria are independent of the specification language and structure used to describe the intended protocol and the language used to implement it. As a consequence, the results may be of use to black box conformance testing approaches in general. Experimental results show that the criteria are a good predictor for fault detection for protocol conformance and for classical structural coverage criteria such as statement and branch coverage. They also show that the division of the domain derived from the criterion produces subdomains such that most of its inputs are fault revealing.

Journal article

D'Ippolito N, Braberman V, Sykes D, Uchitel Set al., 2015, Robust degradation and enhancement of robot mission behaviour in unpredictable environments, 1st International Workshop on Control Theory for Software Engineering (CTSE 2015), Publisher: Association for Computing Machinery, Pages: 26-33

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.

Conference paper

Braberman V, D'Ippolito N, Kramer J, Sykes D, Uchitel Set al., 2015, MORPH: a reference architecture for configuration and behaviour self-adaptation, 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, Publisher: Association for Computing Machinery, Pages: 9-16

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.

Conference paper

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.

Journal article

Alrajeh D, Kramer J, Russo A, Uchitel Set al., 2015, Automated Support for Diagnosis and Repair, Commun. ACM, Vol: 58, Pages: 65-72, ISSN: 0001-0782

Journal article

D'Ippolito N, Braberman V, Piterman N, Uchitel Set al., 2014, Controllability in partial and uncertain environments, 14th International Conference on Application of Concurrency to System Design, Publisher: IEEE, Pages: 52-61, ISSN: 1550-4808

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.

Conference paper

D'ippolito N, braberman V, Kramer J, Magee J, sykes D, Uchitel Set al., 2014, Hope for the Best, Prepare for the Worst: Multi-tier Control for Adaptive Systems, 36th International Conference on Software Engineering, Publisher: ACM, Pages: 688-699

Conference paper

Krka I, D'Ippolito N, Medvidovic N, Uchitel Set 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

Conference paper

Krka I, D'Ippolito N, Medvidović N, Uchitel Set 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.

Conference paper

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.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00307382&limit=30&person=true