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

182 results found

Buckworth T, Alrajeh D, Kramer J, Uchitel Set al., 2023, Adapting specifications for reactive controllers, 2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Publisher: IEEE, Pages: 1-12

For systems to respond to scenarios that were unforeseen at design time, they must be capable of safely adapting, at runtime, the assumptions they make about the environment, the goals they are expected to achieve, and the strategy that guarantees the goals are fulfilled if the assumptions hold. Such adaptation often involves the system degrading its functionality, by weakening its environment assumptions and/or the goals it aims to meet, ideally in a graceful manner. However, finding weaker assumptions that account for the unanticipated behaviour and of goals that are achievable in the new environment in a systematic and safe way remains an open challenge. In this paper, we propose a novel framework that supports assumption and, if necessary, goal degradation to allow systems to cope with runtime assumption violations. The framework, which integrates into the MORPH reference architecture, combines symbolic learning and reactive synthesis to compute implementable controllers that may be deployed safely. We describe and implement an algorithm that illustrates the working of this framework. We further demonstrate in our evaluation its effectiveness and applicability to a series of benchmarks from the literature. The results show that the algorithm successfully learns realizable specifications that accommodate previously violating environment behaviour in almost all cases. Exceptions are discussed in the evaluation.

Conference paper

Delgado T, Sanchez Sorondo M, Braberman V, Uchitel Set al., 2023, Exploration policies for on-the-fly controller synthesis: a reinforcement learning approach, International Conference on Automated Planning and Scheduling, Publisher: Association for the Advancement of Artificial Intelligence, Pages: 569-577

Controller synthesis is in essence a case of model-based planning for non-deterministic environments in which plans (actually “strategies”) are meant to preserve system goals indefinitely. In the case of supervisory control environments are specified as the parallel composition of state machines and valid strategies are required to be “non-blocking” (i.e., always enabling the environment to reach certain marked states) in addition to safe (i.e., keep the system within a safe zone). Recently, On-the-fly Directed Controller Synthesis techniques were proposed to avoid the exploration of the entire -and exponentially large- environment space, at the cost of non-maximal permissiveness, to either find a strategy or conclude that there is none. The incremental exploration of the plant is currently guided by a domain-independent human-designed heuristic. In this work, we propose a new method for obtaining heuristics based on Reinforcement Learning (RL). The synthesis algorithm is thus framed as an RL task with an unbounded action space and a modified version of DQN is used. With a simple and general set of features that abstracts both states and actions, we show that it is possible to learn heuristics on small versions of a problem that generalize to the larger instances, effectively doing zero-shot policy transfer. Our agents learn from scratch in a highly partially observable RL task and outperform the existing heuristic overall, in instances unseen during training.

Conference paper

Pecker-Marcosig E, Zudaire S, Castro R, Uchitel Set al., 2023, Correct and efficient UAV missions based on temporal planning and in-flight hybrid simulations, Robotics and Autonomous Systems, Vol: 164, Pages: 1-17, ISSN: 0921-8890

Controller 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.

Journal article

Ciolek D, Duran M, Zanollo F, Pazos N, Braier J, Braberman V, D'Ippolito N, Uchitel Set al., 2023, On-the-fly informed search of non-blocking directed controllers, Automatica, Vol: 147, Pages: 1-10, ISSN: 0005-1098

We study directed control of discrete event system expressed as the parallel composition of interacting automata. Solutionsthat first compose the automata and then compute a controller may result in an exponential blow up. We present a techniquethat builds the composition on-the-fly guided by a novel domain-independent heuristic, which attempts to discover relevantdependencies between the intervening components. We obtain safe and non-blocking directed controllers, or directors, exploringa reduced portion of the state space. We present the first experimental results on directed control comparing on-the-flycomposition with informed search against the original monolithic approach to directed control.

Journal article

Godoy J, Galeotti JP, Garbervetsky D, Uchitel Set al., 2022, Predicate abstractions for smart contract validation, ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS 2022), Publisher: IEEE, Pages: 289-299

Smart contracts are immutable programs deployed on the blockchainthat can manage significant assets. Because of this, verification andvalidation of smart contracts is of vital importance. Indeed, it isindustrial practice to hire independent specialized companies toaudit smart contracts before deployment. Auditors typically relyon a combination of tools and experience but still fail to identifyproblems in smart contracts before deployment, causing significantlosses. In this paper, we propose using predicate abstraction to con-struct models which can be used by auditors to explore and validatesmart contact behaviour at the function call level by proposingpredicates that expose different aspects of the contract. We pro-pose predicates based on requires clauses and enum-type statevariables as a starting point for contract validation and report onan evaluation on two different benchmarks.

Conference paper

Zudaire S, Nahabedian L, Uchitel S, 2022, Assured mission adaptation of UAVs, ACM Transactions on Autonomous and Adaptive Systems, Vol: 16, Pages: 1-27, ISSN: 1556-4665

The design of systems that can change their behaviour to account for scenarios that were not foreseen at design time remains an open challenge. In this paper we propose an approach for adaptation of mobile robotmissions that is not constrained to a predefined set of mission evolutions. We implement an adaptive software architecture and show how controller synthesis can be used both to guarantee correct transitioning from theold to the new mission goals with runtime architectural reconfiguration to include new software actuators and sensors if necessary. The architecture brings together architectural concepts that are commonplace in robotics such as temporal planning, discrete, hybrid and continuous control layers together with architectural concepts from adaptive systems such as runtime models and runtime synthesis. We validate the architecture flying several missions taken from the robotic literature for different real and simulated UAVs.

Journal article

Keegan M, Braberman VA, D'Ippolito N, Piterman N, Uchitel Set al., 2022, Control and discovery of environment behaviour, IEEE Transactions on Software Engineering, Vol: 48, Pages: 1965-1978, ISSN: 0098-5589

An important ability of self-adaptive systems is to be able to autonomously understand the environment in which they operate and use this knowledge to control the environment behaviour in such a way that system goals are achieved. How can this be achieved when the environment is unknown? Two phase solutions that require a full discovery of environment behaviour before computing a strategy that can guarantee the goals or report the non-existence of such a strategy (i.e., unrealisability) are impractical as the environment may exhibit adversarial behaviour to avoid full discovery. In this paper we formalise a control and discovery problem for reactive system environments. In our approach a strategy must be produced that will, for every environment, guarantee that unrealisablity will be correctly concluded or system goals will be achieved by controlling the environment behaviour. We present a solution applicable to environments characterisable as labeled transition systems (LTS). We use modal transition systems (MTS) to represent partial knowledge of environment behaviour, and rely on MTS controller synthesis to make exploration decisions. Each decision either contributes more knowledge about the environment's behaviour or contributes to achieving the system goals. We present an implementation restricted to GR(1) goals and show its viability.

Journal article

Nahabedian L, Braberman V, DIppolito N, Kramer J, Uchitel Set al., 2022, Assured automatic dynamic reconfiguration of business processes, Information Systems, Vol: 104, Pages: 1-19, ISSN: 0306-4379

In order to manage evolving organisational practice and maintain compliance with changes in policies and regulations, businesses must be capable of dynamically reconfiguring their business processes. However, such dynamic reconfiguration is a complex, human-intensive and error prone task. Not only must new business process rules be devised but also, crucially, the transition between the old and new rules must be managed.In this paper we present a fully automated technique based on formal specifications and discrete event controller synthesis to produce correct-by-construction reconfiguration strategies. These strategies satisfy user-specified transition requirements, be they domain independent - such as delayed and immediate change - or domain specific. To achieve this, we provide a discrete-event control theoretic approach to operationalise declarative business process specifications, and show how this can be extended to resolve reconfiguration problems. In this way, given the old and the new business process rules described as Dynamic Condition Response Graphs, and given the transition requirements described with linear temporal logic, the technique produces a control strategy that guides the organisation through a business process reconfiguration ensuring that all transition requirements and process rules are satisfied. The technique outputs a reconfiguration DCR whose traces reproduce the controller’s reconfiguration strategy. We illustrate and validate the approach using realistic cases and examples from the BPM Academic Initiative.

Journal article

Gorostiaga F, Zudaire S, Sánchez C, Schneider G, Uchitel Set al., 2022, Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification, Pages: 397-414, ISBN: 9783031198489

Temporal task planning uses formal techniques such as reactive synthesis to guarantee that a robot will succeed in its mission. This technique requires certain explicit and implicit assumptions and simplifications about the operating environment of the robot, including its sensors and capabilities. A robot executing a plan can produce a silent mission failure, where the user may believe that the mission goals were achieved when instead the assumptions were violated at runtime. This entails that mitigation and remediation opportunities are missed. Monitoring at runtime can detect complex assumption violations and identify silent failures, but such monitoring requires the ability to describe and detect sophisticated temporal properties together with quantitative and complex data. Additional challenges include (1) ensuring the correctness of the monitors and a correct interplay between the planning execution and the monitors, and (2) that monitors run under constrained environments in terms of resources. In this paper we propose a solution based on stream runtime verification, which offers a high-level declarative language to describe sophisticated monitors together with guarantees on the execution time and memory usage. We show how monitors can be combined with temporal planning not only to monitor assumptions but also to support mitigation and remediation in UAV missions. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.

Book chapter

Alrahman YA, Braberman V, D'Ippolito N, Piterman N, Uchitel Set al., 2021, Synthesis of run-to-completion controllers for discrete event systems, 2021 American Control Conference (ACC), Publisher: IEEE

A controller for a Discrete Event System must achieve its goals despite its environment being capable of resolving race conditions between controlled and uncontrolled events. Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.

Conference paper

Godoy J, Galeotti JP, Garbervetsky D, Uchitel Set al., 2021, Enabledness-based testing of object protocols, ACM Transactions on Software Engineering and Methodology, Vol: 30, Pages: 1-29, ISSN: 1049-331X

A significant proportion of classes in modern software introduce or use object protocols, prescriptions on the temporal orderings of method calls on objects. This paper studies search-based test generation techniques that aim to exploit a particular abstraction of object protocols (enabledness preserving abstractions, EPAs) to findfailures. 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.

Journal article

Uchitel S, Zudaire S, Gorostiaga F, Sanchez C, Schneider Get al., 2021, Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions, International Conference on Robotics and Automation

Conference paper

Alrajeh D, Benjamin P, Uchitel S, 2021, Adaptation<SUP>2</SUP>: Adapting Specification Learners in Assured Adaptive Systems, 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), Publisher: IEEE, Pages: 1347-1352

Conference paper

Pecker-Marcosig E, Zudaire S, Garrett M, Uchitel S, Castro Ret al., 2020, Unified devs-based platform for modelling and simulation of hybrid control systems, Winter Simulation Conference, Publisher: IEEE, Pages: 1051-1062, ISSN: 0891-7736

Recent robotic research has led to different architectural approaches that support enactment of automatically synthesized discrete event controllers from user specifications over low-level continuous variable controllers. Simulation of these hybrid control approaches to robotics can be a useful validation tool for robot users and architecture designers, but presents the key challenge of working with discrete and continuous representations of the robot, its environment and its mission plans. In this work we address this challenge showcasing a unified DEVS-based hybrid simulation platform. We model and simulate the hybrid robotic software architecture of a fixed-wing UAV, including the full stack of controllers involved: discrete, hybrid and continuous. We validate the approach experimentally on a typical UAV mapping mission and show that with our unified approach we are able to achieve simulation speed-ups up to one order of magnitude above our previous Software In The Loop simulation setup.

Conference paper

Nahabedian L, Braberman V, DIppolito N, Honiden S, Kramer J, Tei K, Uchitel Set al., 2020, Dynamic update of discrete event controllers, IEEE Transactions on Software Engineering, Vol: 46, Pages: 1220-1240, 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., 2020, Compositional supervisory control via reactive synthesis and automated planning, IEEE Transactions on Automatic Control, Vol: 65, Pages: 3502-3516, ISSN: 0018-9286

We show how reactive synthesis and automatedplanning can be leveraged effectively to find non-maximal solu-tions to deterministic supervisory control problems of discreteevent systems. To do so, we propose efficient translations ofthe supervisory control problem into the reactive synthesis andplanning frameworks. Notably, our translation methods capturethe compositional and reactive nature of control specifications,avoiding a potential exponential explosion found in alternativetranslation approaches. Additionally, we report on experimentalresults comparing the efficacy of different tools from the threedisciplines, for a particular supervisory control benchmark.

Journal article

Castellano E, Braberman V, D'Ippolito N, Uchitel S, Tei Ket al., 2020, Minimising makespan of discrete controllers: a qualitative approach, 2019 IEEE 58th Conference on Decision and Control (CDC), Publisher: IEEE

Qualitative controller synthesis techniques produce controllers that guarantee to achieve a given goal in the presence of an adversarial environment. However, qualitative synthesis only produces one controller out of many possible solutions and typically does not provide support for expressing preferences over other alternatives. In this paper, we thus present a formal approach to reason about preferences qualitatively, restricting attention to makespan of discrete eventbased controllers for reachability goals. Time is reasoned upon symbolically, which relieves the user from providing concrete quantitative measures. In particular, we study the scenario in which durations of individual activities are not known up-front. We first show how controllers can be symbolically and fairly compared by fixing the contingencies. Then, we present an algorithm to produce controllers that are makespan-minimising.

Conference paper

Zudaire S, Garret M, Uchitel S, 2020, Iterator-based temporal logic task planning, IEEE International Conference on Robotics and Automation, Publisher: IEEE, ISSN: 2152-4092

Temporal logic task planning for robotic systemssuffers from state explosion when specifications involve largenumbers of discrete locations. We provide a novel approach,particularly suited for tasks specifications with universallyquantified locations, that has constant time with respect tothenumber of locations, enabling synthesis of plans for an arbitrarynumber of them. We propose a hybrid control framework thatuses an iterator to manage the discretised workspace hidingitfrom a plan enacted by a discrete event controller. A downsideof our approach is that it incurs in increased overhead whenexecuting a synthesised plan. We demonstrate that the overheadis reasonable for missions of a fixed-wing Unmanned AerialVehicle in simulated and real scenarios for up to700 000locations.

Conference paper

Uchitel S, Braberman V, Kramer J, Nahabedian L, D'Ippolito Net al., 2019, Dynamic reconfiguration of business processes, 17th Int. Conference on Business Process Management (BPM 2019), Publisher: Springer Verlag, Pages: 35-51, 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, 41st IEEE/ACM International Conference on Software Engineering - New Ideas and Emerging Results (ICSE-NIER), Publisher: IEEE COMPUTER SOC, Pages: 81-84

Conference paper

Braberman V, Garbervetsky D, Godoy J, Uchitel S, De Caso G, Perez I, Perez Set al., 2018, 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, Publisher: Springer Verlag, Pages: 377-408, ISSN: 0302-9743

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

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

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