159 results found
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, ISSN: 0270-5257
© 2014 ACM. Most approaches for adaptive systems rely on models, particularly behaviour or architecture models, which describe the system and the environment in which it operates. One of the difficulties in creating such models is uncertainty about the accuracy and completeness of the models. Engineers therefore make assumptions which may prove to be invalid at runtime. In this paper we introduce a rigorous, tiered framework for combining behaviour models, each with different associated assumptions and risks. These models are used to generate operational strategies, through techniques such controller synthesis, which are then executed concurrently at runtime. We show that our framework can be used to adapt the functional behaviour of the system: through graceful degradation when the assumptions of a higher level model are broken, and through progressive enhancement when those assumptions are satisfied or restored.
Sykes D, Corapi D, Magee J, et al., 2013, Learning Revised Models for Planning in Adaptive Systems, 35th International Conference on Software Engineering (ICSE), Publisher: IEEE, Pages: 63-71, ISSN: 0270-5257
Environment domain models are a key part of the information used by adaptive systems to determine their behaviour. These models can be incomplete or inaccurate. In addition, since adaptive systems generally operate in environments which are subject to change, these models are often also out of date. To update and correct these models, the system should observe how the environment responds to its actions, and compare these responses to those predicted by the model. In this paper, we use a probabilistic rule learning approach, NoMPRoL, to update models using feedback from the running system in the form of execution traces. NoMPRoL is a technique for nonmonotonic probabilistic rule learning based on a transformation of an inductive logic programming task into an equivalent abductive one. In essence, it exploits consistent observations by finding general rules which explain observations in terms of the conditions under which they occur. The updated models are then used to generate new behaviour with a greater chance of success in the actual environment encountered. © 2013 IEEE.
McVeigh A, Kramer J, Magee J, et al., 2011, Evolve: Tool Support for Architecture Evolution, 33rd International Conference on Software Engineering (ICSE), Publisher: IEEE, Pages: 1040-1042, ISSN: 0270-5257
Incremental change is intrinsic to both the initial development and subsequent evolution of large complex software systems. Evolve is a graphical design tool that captures this incremental change in the definition of software architecture. It supports a principled and manageable way of dealing with unplanned change and extension. In addition, Evolve supports decentralized evolution in which software is extended and evolved by multiple independent developers. Evolve supports a model-driven approach in that architecture definition is used to directly construct both initial implementations and extensions to these implementations. The tool implements Backbone - an architectural description language (ADL), which has both a textual and a UML2, based graphical representation. The demonstration focuses on the graphical representation. © 2011 Authors.
Foster H, Uchitel S, Magee J, et al., 2010, An Integrated Workbench for Model-Based Engineering of Service Compositions, IEEE TRANSACTIONS ON SERVICES COMPUTING, Vol: 3, Pages: 131-144, ISSN: 1939-1374
The Service-Oriented Architecture (SOA) approach to building systems of application and middleware components promotes the use of reusable services with a core focus of service interactions, obligations, and context. Although services technically relieve the difficulties of specific technology dependency, the difficulties in building reusable components is still prominent and a challenge to service engineers. Engineering the behavior of these services means ensuring that the interactions and obligations are correct and consistent with policies set out to guide partners in building the correct sequences of interactions to support the functions of one or more services. Hence, checking the suitability of service behavior is complex, particularly when dealing with a composition of services and concurrent interactions. How can we rigorously check implementations of service compositions? What are the semantics of service compositions? How does deployment configuration affect service composition behavior safety? To facilitate service engineers designing and implementing suitable and safe service compositions, we present in this paper an approach to consider different viewpoints of service composition behavior analysis. The contribution of the paper is threefold. First, we model service orchestration, choreography behavior, and service orchestration deployment through formal semantics applied to service behavior and configuration descriptions. Second, we define types of analysis and properties of interest for checking service models of orchestrations, choreography, and deployment. Third, we describe mechanical support by providing a comprehensive integrated workbench for the verification and validation of service compositions. © 2008 IEEE.
Lang F, Salauen G, Herilier R, et al., 2010, Translating FSP into LOTOS and networks of automata, FORMAL ASPECTS OF COMPUTING, Vol: 22, Pages: 681-711, ISSN: 0934-5043
Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Finite state processes (FSP) is a widely used calculus equipped with Ltsa, a graphical and user-friendly tool. Language of temporal ordering specification (Lotos) is the only process calculus that has led to an international standard, and is supported by the Cadp verification toolbox. We propose a translation of FSP sequential processes into Lotos. Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in Lotos, they are translated into networks of automata which are another input language accepted by Cadp. Hence, it is possible to use jointly Ltsa and Cadp to validate FSP specifications. Our approach is completely automated by a translator tool. © 2009 British Computer Society.
Mens T, Magee J, Rumpe B, et al., 2010, EVOLVING SOFTWARE ARCHITECTURE DESCRIPTIONS OF CRITICAL SYSTEMS, COMPUTER, Vol: 43, Pages: 42-48, ISSN: 0018-9162
Foster H, Uchitel S, Kramer J, et al., 2009, Towards Self-management in Service-oriented Computing with Modes, 5th International Conference on Service-Oriented Computing (ICSOC 2007), Publisher: SPRINGER-VERLAG BERLIN, Pages: 338-350, ISSN: 0302-9743
A self-managed system is both self-assembling and self-healing. Service-oriented Computing (SoC) architectures, such as a Web Services Architecture (WS-A)illustrate a highly distributed, potentially dynamic,domain for component configurations. We propose the use of component architecture "modes" to facilitate the self-management of services within a SoC environment. A mode abstracts a set of services that are composed to complete a given task. Our approach, named "SelfSoC" includes designing and implementing key parts of a self-managed system specifically aimed at supporting a dynamic services architecture. We extend Darwin component models, Alloy constraint models and distributed system management policies to specify the mode architectures. We also propose the generation of dynamic orchestrations for service compositions to coordinate different modes of an automotive services platform. © 2009 Springer Berlin Heidelberg.
Heaven W, Sykes D, Magee J, et al., 2009, A Case Study in Goal-Driven Architectural Adaptation, Dagstuhl Seminar on Software Engineering for Self-Adaptive Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 109-127, ISSN: 0302-9743
To operate reliably in environments where interaction with an operator is infrequent or undesirable, an autonomous system should be capable of both determining how to achieve its objectives and adapting to novel circumstances on its own. We have developed an approach to constructing autonomous systems that synthesise tasks from high-level goals and adapt their software architecture to perform these tasks reliably in a changing environment. This paper presents our approach through a detailed case study, highlighting the challenges involved. © 2009 Springer Berlin Heidelberg.
Kramer J, Magee J, Kramer J, et al., 2009, A Rigorous Architectural Approach to Adaptive Software Engineering, JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, Vol: 24, Pages: 183-188, ISSN: 1000-9000
The engineering of distributed adaptive software is a complex task which requires a rigorous approach. Software architectural (structural) concepts and principles are highly beneficial in specifying, designing, analysing, constructing and evolving distributed software. A rigorous architectural approach dictates formalisms and techniques that are compositional, components that are context independent and systems that can be constructed and evolved incrementally. This paper overviews some of the underlying reasons for adopting an architectural approach, including a brief "rational history" of our research work, and indicates how an architectural model can potentially facilitate the provision of self-managed adaptive software system. © 2009 Springer.
Letier E, Kramer J, Magee J, et al., 2008, Deriving event-based transition systems from goal-oriented requirements models, AUTOMATED SOFTWARE ENGINEERING, Vol: 15, Pages: 175-206, ISSN: 0928-8910
Goal-oriented methods are increasingly popular for elaborating software requirements. They offer systematic support for incrementally building intentional, structural, and operational models of the software and its environment. Event-based transition systems on the other hand are convenient formalisms for reasoning about software behaviour at the architectural level. The paper relates these two worlds by presenting a technique for translating formal specification of software operations built according to the KAOS goal-oriented method into event-based transition systems analysable by the LTSA toolset. The translation involves moving from a declarative, state-based, timed, synchronous formalism typical of requirements modelling languages to an operational, event-based, untimed, asynchronous one typical of architecture description languages. The derived model can be used for the formal analysis and animation of KAOS operation models in LTSA. The paper also provides insights into the two complementary formalisms, and shows that the use of synchronous temporal logic for requirements specification hinders a smooth transition from requirements to software architecture models. © 2008 Springer Science+Business Media, LLC.
Self-management is put forward as one of the means by which we could provide systems that are scalable, support dynamic composition and rigorous analysis, and are flexible and robust in the presence of change. In this paper, we focus on architectural approaches to self-management, not because the language-level or network-level approaches are uninteresting or less promising, but because we believe that the architectural level seems to provide the required level of abstraction and generality to deal with the challenges posed. A self-managed software architecture is one in which components automatically configure their interaction in a way that is compatible with an overall architectural specification and achieves the goals of the system. The objective is to minimise the degree of explicit management necessary for construction and subsequent evolution whilst preserving the architectural properties implied by its specification. This paper discusses some of the current promising work and presents an outline three-layer reference model as a context in which to articulate some of the main outstanding research challenges. © 2007 IEEE.
Salauen G, Kramer J, Lang F, et al., 2007, Translating FSP into LOTOS and networks of automata, 6th International Conference on Integrated Formal Methods, Publisher: SPRINGER-VERLAG BERLIN, Pages: 558-578, ISSN: 0302-9743
Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. FSP is a widely-used calculus equipped with LTSA, a graphical and user-friendly tool. LOTOS is the only process calculus that has led to an international standard, and is supported by the CADP verification toolbox. We propose a translation from FSP to LOTOS. Since FSP composite processes are hard to encode into LOTOS, they are translated into networks of automata which are another input language accepted by CADP. Hence, it is possible to use jointly LTSA and CADP to validate FSP specifications. Our approach is completely automated by a translator tool we implemented. © Springer-Verlag Berlin Heidelberg 2007.
Bonta E, Bernardo M, Magee J, et al., 2006, Synthesizing concurrency control components from process algebraic specifications, 8th International Conference on Coordination Models and Languages (COORDINATION 2006), Publisher: SPRINGER-VERLAG BERLIN, Pages: 28-43, ISSN: 0302-9743
Process algebraic specifications can provide useful support for the architectural design of software systems due to the possibility of analyzing their properties. In addition to that, such specifications can be exploited to guide the generation of code. What is needed at this level is a general methodology that accompanies the translation process, which in particular should help understanding whether and when it is more appropriate to implement a software component as a thread or as a monitor. The objective of this paper is to develop a systematic approach to the synthesis of correctly coordinating monitors from arbitrary process algebraic specifications that satisfy some suitable constraints. The whole approach will be illustrated by means of the process algebraic specification of a cruise control system. © Springer-Verlag Berlin Heidelberg 2006.
Foster H, Uchitel S, Magee JN, et al., 2006, Model-Based Analysis of Obligations in Web Service Choreography, IEEE International Conference on Internet & Web Applications and Services 2006, Guadeloupe, FC.
Foster H, Uchitel S, Magee JN, et al., 2006, WS-Engineer: A Tool for Model-Based Verification of Web Service Compositions and Choreography, IEEE International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 2006.
Foster H, Uchitel S, Magee J, et al., 2006, Model-based analysis of obligations in Web Service Choreography, IEEE International Conference on Internet & Web Applications and Services 2006, Guadeloupe, FC., Publisher: IEEE Computer Society, Pages: 149-149
In this paper we discuss a model-based approach to the analysis of service interactions for coordinated web service compositions using obligation policies specified in the form of Message Sequence Charts (MSCs) and implemented in the Web Service Choreography Description Language (WSCDL). The approach uses finite state machine representations of web service compositions (implemented in BPEL4WS) and service choreography rules, and assigns semantics to the distributed process interactions. The move towards implementing web service choreography requires design time verification of these service interactions to ensure that service implementations fulfill requirements for multiple interested partners before such compositions and choreographies are deployed. The described approach is supported by a suite of cooperating tools for specification, formal modeling, animation and providing verification results from choreographed web service interactions. © 2006 IEEE.
© Springer-Verlag Berlin Heidelberg 2006. Modern systems are heterogeneous, geographically distributed and highly dynamic since the communication topology can vary and the components can, at any moment, connect to or detach from the system. Service Oriented Computing (SOC) has emerged as a suitable paradigm for specifying and implementing such global systems. The variety and dynamics in the possible scenarios implies that considering such systems as belonging to a single architectural style is not helpful. This considerations take us to propose the notion of Mode as a new element of architectural descriptions. A mode abstracts a specific set of services that must interact for the completion of a specific subsystem task. This paper presents initial ideas regarding the formalization of modes and mode transitions as explicit elements of architectural descriptions with the goal of providing flexible support for the description and verification of complex adaptable service oriented systems. We incorporate the notion of mode to the Darwin architectural language and apply it to illustrate how modes may help on describing systems from the Automotive domain.
Magee J, Kramer J, Magee J, et al., 2006, Concurrency: State Models & Java Programs, 2nd Edition, Publisher: John Wiley & Sons, ISBN: 978-0-470-09355-9
Uchitel S, Chatley R, Kramer J, et al., 2006, Goal and scenario validation: a fluent combination, IEEE Conference on Requirement Engineering, Publisher: SPRINGER, Pages: 123-137, ISSN: 0947-3602
Scenarios and goals are effective techniques for requirements definition. Goals are objectives that a system has to meet. They are elaborated into a structure that decomposes declarative goals into goals that can be formulated in terms of events and can be controlled or monitored by the system. Scenarios are operational examples of system usage. Validation of goals and scenarios is essential in order to ensure that they represent what stakeholders actually want. Rather than validating scenarios and goals separately, possibly driving the elaboration of one through the validation of another, this paper exploits the relationship between goals and scenarios. The aim is to provide effective graphical animations as a means of supporting such a validation. The relation between scenarios and goals is established by means of fluents that describe how events of the operational description change the state of the basic propositions from which goals are expressed. Graphical animations are specified in terms of fluents and driven by a behaviour model synthesised from the operational scenarios. In addition, goal model checking over operational scenarios is provided to guide animations through goal violation traces. © Springer-Verlag London Limited 2005.
Chatley R, Uchitel S, Kramer J, et al., 2005, Fluent-based web animation: Exploring goals for requirements validation, 27th IEEE/ACM International Conference on Software Engineering (ICSE), St. Louis, 2005., Publisher: ACM, Pages: 674-675
We present a tool that provides effective graphical animations as a means of validating both goals and software designs. Goals are objectives that a system is expected to meet. They are decomposed until they can be represented as fluents. Animations are specified in terms of fluents and driven by behaviour models.
Chatley R, Uchitel S, Kramer J, et al., 2005, Fluent-based web animation: exploring goals for requirements validation, Icse 05: 27Th International Conference on Software Engineering, Proceedings, Pages: 674-675, ISSN: 0270-5257
Chatley R, Uchitel S, Kramer J, et al., 2005, Fluent-based web animation: exploring goals for requirements validation, Icse 05: 27Th International Conference on Software Engineering, Proceedings, Pages: 674-675, ISSN: 0270-5257
We present a toot that provides effective graphical animations as a means of validating both goals and software designs. Goals are objectives that a system is expected to meet. They are decomposed until they can be represented as fluents. Animations are specified in terms of fluents and driven by behaviour models.
Foster H, Uchitel S, Magee JN, et al., 2005, Leveraging Eclipse for Integrated Model-Based Engineering of Web Service Compositions, ETX2005 Workshop at OOPSLA05, San Diego, CA, October 2005.
Foster H, Uchitel S, Magee J, et al., 2005, Leveraging Eclipse for integrated model-based engineering of web service compositions, ETX2005 Workshop at OOPSLA05, San Diego, CA, October 2005., Publisher: ACM, Pages: 95-99
In this paper we detail the design and implementation of an Eclipse plug-in for an integrated, model-based approach, to the engineering of web service compositions. The plug-in allows a designer to specify a service's obligations for coordinated web service compositions in the form of Message Sequence Charts (MSCs) and then generate policies in the form of WS-CDL and services in the form of BPEL4WS. The approach uses finite state machine representations of web service compositions and service choreography rules, and assigns semantics to the distributed process interactions. The move towards implementing web service choreography requires design time verification of these service interactions to ensure that service implementations fulfill requirements for multiple interested partners before such compositions and choreographies are deployed. The plug-in provides a tool for integrated specification, formal modeling, animation and providing verification results from choreographed web service interactions. The LTSA-Eclipse (for Web Services) plug-in is publicly available, along with other plug-ins, at: http://www.doc.ic.ac.uk/ltsa. Copyright © 2005 IBM.
Foster H, Uchitel S, Magee J, et al., 2005, Using a rigorous approach for engineering web service compositions: A case study, IEEE International Conference on Services Computing, Publisher: IEEE COMPUTER SOC, Pages: 217-224
In this paper we discuss a case study for the UK Police IT Organisation (PITO) on using a model-based approach to verifying web service composition interactions for a coordinated service-oriented architecture. The move towards implementing web service compositions by multiple interested parties as a form of distributed system architecture promotes the ability to support 1) early verification of service implementations against design specifications and 2) that compositions are built with compatible interfaces for differing scenarios in such a collaborative environment. The approach uses finite state machine representations of web service orchestrations and distributed process interactions. The described approach is supported by an integrated tool environment for for providing verification and validation results from checking designated properties of service models. © 2005 IEEE.
Foster H, Uchitel S, Magee J, et al., 2005, Tool support for model-based engineering of web service compositions, Los Alamitos, IEEE international conference on services computing. Orlando, FL, 11 - 15 July 2005, Publisher: IEEE Computer Society, Pages: 95-102
In this paper we describe tool support for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The tool is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling and trace animation of the composition process.
Kramer J, Magee J, 2005, Model-based Design of Concurrent Programs, Communicating Sequential Processes: The First 25 Years, Publisher: Springer-Verlag, Pages: 211-219
Letier E, Kramer J, Magee J, et al., 2005, Monitoring and control in scenario-based requirements analysis., 27th IEEE/ACM International Conference on Software Engineering (ICSE), St. Louis, 2005., Publisher: ACM, Pages: 382-391
Magee J, Kramer J, Magee J, et al., 2005, Model-based design of concurrent programs, Symposium on 25 Years of Communicating Sequential Processes, Publisher: SPRINGER-VERLAG BERLIN, Pages: 211-219, ISSN: 0302-9743
A model is a simplified representation of the real world and, as such, includes only those aspects of the real-world system relevant to the problem at hand. The paper reviews a modelling approach to the design of concurrent programs in which models represent the behaviour of concurrent Java programs. A notation based on CSP is used to model behaviour. Tool support enables both interactive model exploration and the mechanical verification of required safety and liveness properties. Models are systematically translated into Java programs. The approach, supported by a textbook, forms the basis of a course at the authors' institution and has also been widely adopted elsewhere. With the benefit of five years hindsight, we examine the strengths and weaknesses of the approach and look at some of the subsequent remedies and directions. © Springer-Verlag Berlin Heidelberg 2005.
Uchitel S, Chatley RB, Kramer J, et al., 2005, Fluent-based animation: exploiting the relation between goals and scenarios for requirements validation, Requirements Engineering Journal, Vol: 10, ISSN: 0947-3602
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.