This “interview” with Jeff Kramer offers an insight into his experiences and challenges as an Editor-in-Chief of IEEE TSE. It also provides some consideration of how the software engineering landscape was viewed during his tenure. Finally it offers some thoughts on the future of the journal and of the field of software engineering.

By invitation, we revisit our 1990 paper -The Evolving Philosophers: Dynamic Change Management.The paper addressed the problem of safely updating large complex distributed systems while permitting the system to continue running to provide at least a partial service. We outline the context in which we addressed this problem, the key ideas behind the proposed solution and then focus on the development and influence of these ideas in both our own subsequent research and that of others.

Automated detection of software failures is an important but challenging software engineering task. It involves finding in a vast search space the failure-inducing test cases that contain an input triggering the software fault and an oracle asserting the incorrect execution. We are motivated to study how far this outstanding challenge can be solved by recent advances in large language models (LLMs) such as ChatGPT. However, our study reveals that ChatGPT has a relatively low success rate (28.8%) in finding correct failure-inducing test cases for buggy programs. A possible conjecture is that finding failure-inducing test cases requires analyzing the subtle differences (nuances) between the tokens of a program's correct version and those for its buggy version. When these two versions have similar sets of tokens and attentions, ChatGPT is weak in distinguishing their differences. We find that ChatGPT can successfully generate failure-inducing test cases when it is guided to focus on the nuances. Our solution is inspired by an interesting observation that ChatGPT could infer the intended functionality of buggy code if it is similar to the correct version. Driven by the inspiration, we develop a novel technique, called Differential Prompting, to effectively find failure-inducing test cases with the help of the compilable code synthesized by the inferred intention. Prompts are constructed based on the nuances between the given version and the synthesized code. We evaluate Differential Prompting on Quixbugs (a popular benchmark of buggy programs) and recent programs published at Codeforces (a popular programming contest portal, which is also an official benchmark of ChatGPT). We compare Differential Prompting with two baselines constructed using conventional ChatGPT prompting and Pynguin (the state-of-the-art unit test generation tool for Python programs). Our evaluation results show that for programs of Quixbugs, Differential Prompting can achieve a success rate of 75.0% in finding failure-inducing test cases, outperforming the best baseline by 2.6X. For programs of Codeforces, Differential Prompting's success rate is 66.7%, outperforming the best baseline by 4.0X.

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.

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.

Providing rigorous techniques and tools to support RE so that it could potentially be performed online, at runtime, is certainly challenging. However the rewards could be great. Performing RE at runtime has the potential not only to enable software self-adaptation, but also to provide support for change in general by suggesting possible remedies to engineers. This talk will present our motivation and vision, and suggest possible approaches using techniques such as model checking, learning and synthesis to try to support RE change and adaptation.

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.

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.

In this paper we propose a modelling formalism, Probabilistic Component Automata (PCA), as a probabilistic extension to Interface Automata to represent the probabilistic behaviour of component-based systems. The aim is to support composition of component-based models for both behaviour and non-functional properties such as reliability. We show how additional primitives for modelling failure scenarios, failure handling and failure propagation, as well as other algebraic operators, can be combined with models of the system architecture to automatically construct a system model by composing models of its subcomponents. The approach is supported by the tool LTSA-PCA, an extension of LTSA, which generates a composite DTMC model. The reliability of a particular system configuration can then be automatically analysed based on the corresponding composite model using the PRISM model checker. This approach facilitates configurability and adaptation in which the software configuration of components and the associated composition of component models are changed at run time.

Self-managed systems need to adapt to changes in requirements and in operational conditions. New components or services may become available, others may become unreliable or fail. Non-functional aspects, such as reliability or other quality-of-service parameters usually drive the selection of new architectural configurations. However, in existing approaches, the link between non-functional aspects and software models is established through manual annotations that require human intervention on each re-configuration and adaptation is enacted through fixed rules that require anticipation of all possible changes. We propose here a methodology to automatically re-assemble services and component-based applications to preserve their reliability. To achieve this we define architectural and behavioural models that are composable, account for non-functional aspects and correspond closely to the implementation. Our approach enables autonomous components to locally adapt and control their internal configuration whilst exposing interface models to upstream components.

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.

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.

The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system.

Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration.

Missing requirements are known to be among the major causes of software failure. They often result from a natural inclination to conceive over-ideal systems where the software-to-be and its environment always behave as expected. Obstacle analysis is a goal-anchored form of risk analysis whereby exceptional conditions that may obstruct system goals are identified, assessed and resolved to produce complete requirements. Various techniques have been proposed for identifying obstacle conditions systematically. Among these, the formal ones have limited applicability or are costly to automate. This paper describes a tool-supported technique for generating a set of obstacle conditions guaranteed to be complete and consistent with respect to the known domain properties. The approach relies on a novel combination of model checking and learning technologies. Obstacles are iteratively learned from counterexample and witness traces produced by model checking against a goal and converted into positive and negative examples, respectively. A comparative evaluation is provided with respect to published results on the manual derivation of obstacles in a real safety-critical system for which failures have been reported.

Summary form only given. Social media has revolutionized how humans create and curate knowledge artifacts [1]. It has increased individual engagement, broadened community participation and led to the formation of new social networks. This paradigm shift is particularly evident in software engineering in three distinct ways: firstly, in how software stakeholders co-develop and form communities of practice; secondly, in the complex and distributed software ecosystems that are enabled through insourcing, outsourcing, open sourcing and crowdsourcing of components and related artifacts; and thirdly, by the emergence of socially-enabled software repositories and collaborative development environments [2].

The necessity of accurate localization in mobile robotics is obvious—if a robot does not know where it is, it cannot navigate accurately and reach goal locations. Robots learn about their environment via sensors. Small robots require small, efficient, and, if they are to be deployed in large numbers, inexpensive sensors. The sensors used by robots to perceive the world are inherently inaccurate, providing noisy, erroneous data, or even no data at all. Combined with estimation error due to imperfect modeling of the robot, there are many obstacles to successfully localizing in the world. Sensor fusion is used to overcome these difficulties—combining the available sensor data to derive a more accurate pose estimation for the robot. A feeling of “ready-fire-aim'' pervades the discipline—filters are chosen on little to no information, and new filters are simply tested against a few peers and claimed as superior to all others. This is folly—the most appropriate filter is seldom the newest. This article provides an overview and in-depth tutorial of all modern robot localization methods and thoroughly discusses their strengths and weaknesses to assist a robot researcher in the task of choosing the most appropriate filter for their task. © 2012 Wiley Periodicals, Inc.

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.

Localization is arguably the most important goal for a robot to solve-without knowledge of its place in the world, a robot cannot do useful work. The current best practice for providing accurate localization given uncertain sensors involves the use of sensor fusion, or combining sensor data in order to derive a better pose estimation for the robot. Small robots add another problem that needs to be solved-limited power, computational ability, and weight/space constrain both the sensors available and the filters that can be used. This paper provides a detailed example in simulation of four filter types: the extended Kalman filter, the Fuzzy EKF, the sigma-point KF (SPKF), and the double fuzzy SPKF, while discussing the strengths and weaknesses of all current state of the art sensor methods. While the field is relatively mature, there has been little to no comparative analysis of different filters performed-what roles do they best serve, how to select the “best” filter, and what tradeoffs must be made for each type. This paper analyzes the current state of the art filters of all categories and determines their applicability to the small robot problem.

Abstract One of the difficulties in goal-oriented requirements engineering (GORE) is the construction of behaviour models from declarative goal specifications. This paper addresses this problem using a combination of model checking and machine learning. First, a goal model is transformed into a (potentially Zeno) behaviour model. Then, via an iterative process, Zeno traces are identified by model checking the behaviour model against a time progress property, and inductive logic programming (ILP) is used to learn operational requirements ( pre-conditions ) that eliminate these traces. The process terminates giving a non-Zeno behaviour model produced from the learned pre-conditions and the given goal model.

Abstract 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 L tsa , a graphical and user-friendly tool. Language of temporal ordering specification (L otos ) is the only process calculus that has led to an international standard, and is supported by the C adp verification toolbox. We propose a translation of FSP sequential processes into L otos . Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in L otos , they are translated into networks of automata which are another input language accepted by C adp . Hence, it is possible to use jointly L tsa and C adp to validate FSP specifications. Our approach is completely automated by a translator tool.

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.

Time for change ... Alas, my term of office from January 2006 to December 2009 as the Editor in Chief of the IEEE Transactions on Software Engineering has ended. It has been a great honor to serve and I have very much enjoyed it. It provided me with an interesting overview of the field and an opportunity to make contact with the many researchers and practitioners who contribute to TSE. Despite the onerous responsibility—and it is hard work—I shall miss it. It is my great pleasure to introduce the new Editor in Chief, Professor Bashar Nuseibeh, who takes over from 1 January 2010. Bashar is a professor in computing at the Open University in the United Kingdom and Chief Scientist at Lero—the Irish Software Engineering Research Centre. He is a gifted researcher with an extensive portfolio of major research contributions. Bashar is a very active member of the software engineering community and a loyal supporter of the IEEE Transactions on Software Engineering, having served as an associate editor on the Editorial Board for the last four years. The journal is in excellent hands, and I am delighted that Bashar agreed to undertake this responsibility. State of the journal During my term of office, I have endeavored to attract more submissions, to improve the quality of the published papers, to widen their relevance and appeal, and to strengthen the archival nature of the journal. I am pleased to report that the journal is in a very healthy state, and the excellent reputation of TSE has continued to strengthen, in terms of both submissions and citations/impact. There has been a steady increase in submissions, starting from 302 papers in 2006, 356 in 2007, 412 in 2008, and finally 418 in 2009. This annual increase in submissions reflects an encouraging interest by authors in the selection of TSE as their journal of choice for publication. As a complement to the submissions figures, those for impact and citations reflect the growing reputation of TSE among readers as a good source of relevant results. Thomson reports that citations have risen dramatically from 3,165 in 2005, 3,203 in 2006, and 3,672 in 2007 to the latest figure of 5,449 for 2008. Impact factor is a measure of the frequency with which the “average article” in a journal has been cited in a particular year. The results for TSE impact have similarly risen from 1.967 in 2005, 2.132 in 2006, and 2.105 in 2007 to the latest figure of 3.569 for 2008. Thanks to the hard work and expertise of our Associate Editors and reviewers, the reviewing process remains efficient yet rigorous. The current acceptance rate for the journal is around 12 percent. The average time from submission to first decision is around three and half months, from submission to final decision is about seven and half months, from acceptance to electronic publication (Rapid Posting) just over a month, and from submission to paper publication is around 14 months. For a particular paper, the time from submission to a decision varies because of many factors, including the length of the manuscript, the workload of the editors involved, and the workloads of the various reviewers. Editorial Board On behalf of the software engineering community, I would like to express my sincere thanks to all of the Associate Editors who served as members of the Board during my term of office. The Editorial Board is the foundation upon which TSE is built. Board membership is both an honor and a duty. Despite many other commitments, these colleagues of international repute voluntarily give of their time and effort, taking responsibility for selecting reviewers, overseeing the reviewing process, and making the final recommendations regarding acceptability. They are instrumental in maintaining the reputation of the IEEE Transactions on Software Engineering as a first-class journal. I am very grateful for their unstinting support and expert advice; it has been a privilege to work with them. Like me, a number of Associate Editors reached the end of their terms of office in December 2009: my sincere thanks to Jo Atlee, Shing-Chi Cheung, Rance Cleaveland, Prem Devanbu, Susanna Donatelli, Matt Dwyer, Wolfgang Emmerich, Mark Harman, Audris Mockus, Hausi Muller, Bashar Nuseibeh, Wilhelm Schaefer, Neeraj Suri, Dick Taylor, Sebastian Uchitel, and AlexWolf.

Biomedical scientists generate, access, validate and interpret multiple distributed and heterogeneous data sets. Semantic annotations for these data sets are paramount for exchanging and using the data, and take the form of concepts from a domain ontology. ONIX is a platform that facilitates the access to cancer research data resources and one of its goals is to interoperate with caGrid — a grid computing infrastructure for data sharing. In this paper, we present the ONIX approach to building a semantic layer with support for concept-based queries, which exploit semantic annotations of resources, focusing on caGrid resources. The main contributions of this work are: the automatic generation of OWL ontologies from resources' metadata; concept-based query construction and validation; rewriting and translation from concept-based queries to the caGrid query language.

Goal-oriented methods have increasingly been recognised as an effective means for eliciting, elaborating, analysing and specifying software requirements. A key activity in these approaches is the elaboration of a correct and complete set of opertional requirements, in the form of pre- and trigger-conditions, that guarantee the system goals. Few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. In this paper we propose a tool-based framework that combines model checking, inductive learning and scenarios for elaborating operational requirements from goal models. This is an iterative process that requires the engineer to identify positive and negative scenarios from counterexamples to the goals, generated using model checking, and to select operational requirements from suggestions computed by inductive learning.

Probabilistic models are useful in the analysis of system behaviour and non-functional properties. Reliable estimates and measurements of probabilities are needed to annotate behaviour models in order to generate accurate predictions. However, this may not be sufficient, and may still lead to inaccurate results when the system model does not properly reflect the probabilistic choices made by the environment. Thus, not only should the probabilities be accurate in properly reflecting reality, but also the model that is being used. In this paper we identify and illustrate this problem showing that it can lead to inaccuracies and both false positive and false negative property checks. We propose state refinement as a technique to mitigate this problem, and present a framework for iteratively improving the accuracy of a probabilistically annotated behaviour model.

When enacting a web service orchestration defined using the Business Process Execution Language (BPEL) we observed various safety property violations. This surprised us considerably as we had previously established that the orchestration was free of such property violations using existing BPEL model checking techniques. In this paper, we describe the origins of these violations. They result from a combination of design and deployment decisions, which include the distribution of services across hosts, the choice of synchronisation primitives in the process and the threading configuration of the servlet container that hosts the orchestrated web services. This leads us to conclude that model checking approaches that ignore resource constraints of the deployment environment are insufficient to establish safety and liveness properties of service orchestrations specifically, and distributed systems more generally. We show how model checking can take execution resource constraints into account. We evaluate the approach by applying it to the above application and are able to demonstrate that a change in allocation of services to hosts is indeed safe, a result that we are able to confirm experimentally in the deployed system. The approach is supported by a tool suite, known as WS-Engineer, providing automated process translation, architecture and model-checking views.

In this paper we describe a tool 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) process 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 approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.

This workshop explores the concept of abstraction in software engineering at the individual, team and organization level. The aim is to explore the role of abstraction in dealing with complexity in the software engineering process, to discuss how the use of different levels of abstraction may facilitate performance of different activities, and to examine whether or not abstraction skills can be taught.

T IEEE Transactions on Software Engineering is one of the foremost journals in software engineering, with a long and prestigious history of publishing high quality archival papers. It has been in publication for more than 30 years and has served the community well. I am honored and proud to have been appointed as the new editor-in-chief. On behalf of all our readers, I would like to thank the previous editor-in-chief, John Knight, the associate editors, reviewers, authors, and support staff from the IEEE Computer Society Publications Offi ce for their hard work and outstanding efforts. TSE received more than 300 submissions last year and yet managed an average review time of around four months. It is essential that TSE maintain its reputation for quality, its appeal to both researchers and practitioners, and its relevance in an environment which has changed radically over the years.

IT is my pleasure to introduce and welcome three new members of the Editorial Board, Antonia Bertolino, Ross Jeffery, and Patrick McDaniel. Dr. Bertolino will assist us in the areas of software testing and software dependability, as well as other nonfunctional properties, Professor Jeffery in the areas of software engineering process and product modeling and improvement, and in software quality, metrics, and management, and Professor McDaniel in various aspects of software security, such as in network and systems, programming languages, telecommunications, digital rights, and policies. The brief biographies of these new AEs can be found below. I look forward to working with our new AEs. I would also like to thank the following people who have retired from the Editorial Board so far this year: Tom Ball, Bill Frakes, Pankaj Jalote, Robyn Lutz, and Avi Rubin. These colleagues have voluntarily given their time and effort to the task of paper management and peer review, helping to maintain the reputation of the IEEE Transactions on Software Engineering as a fi rst-class journal. I am very grateful for their support. Finally, I would like to use this opportunity to give you news of some changes at TSE. It has been decided that, beginning in January 2008, TSE should go from 12 monthly issues per year to 6 bimonthly issues. The result will be fewer but healthier issues with more papers and content per issue, which will be easier for the IEEE CS to produce and which will help us to reduce our costs. Bimonthly issues will not penalize authors: We already have electronic publication (Rapid Posting) on acceptance and the maximum increase in paper publication delay will be a month. Readers will also not suffer as all subscriptions include both online access and printed copies of the journal. Although this will mean fewer issues per year, the intention is not to reduce the content. On the contrary, TSE has the capacity to publish more papers of the required quality. Despite receiving around one paper submission every day, we continue to provide rigorous review and relatively fast turnaround, with average times from submission to fi rst decision of 4 months and to publication of around 13 months. I encourage all authors in the software engineering fi eld to submit their best work to TSE.

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.

Scenarios are an effective means for eliciting, validating and documenting requirements. At the requirements level, scenarios describe sequences of interactions between the software-to-be and agents in the environment. Interactions correspond to the occurrence of an event that is controlled by one agent and monitored by another.This paper presents a technique to analyse requirements-level scenarios for unforeseen, potentially harmful, consequences. Our aim is to perform analysis early in system development, where it is highly cost-effective. The approach recognises the importance of monitoring and control issues and extends existing work on implied scenarios accordingly. These so-called input-output implied scenarios expose problematic behaviours in scenario descriptions that cannot be detected using standard implied scenarios. Validation of these implied scenarios supports requirements elaboration. We demonstrate the relevance of input-output implied scenarios using a number of examples.

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.

The role of structure in specifying, designing, analysing, constructing and evolving software has been the central theme of our research in Distributed Software Engineering. This structural discipline dictates formalisms and techniques that are compositional, components that are context independent and systems that can be constructed and evolved incrementally. This extended abstract overviews our development of a structural approach to engineering distributed software and gives indications of our future work which moves from explicit to implicit structural specification. With the benefit of hindsight we attempt to give a "rational history" to our research.

Fluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through "fluents" which are state predicates whose value are determined by the occurrences of initiating and terminating events that make the fluents values become true or false, respectively.The existing fluent temporal logic is convenient for reasoning about untimed event-based models but difficult to use for timed models. The paper extends fluent temporal logic with temporal operators for modelling timed properties of discrete-time event-based models. It presents two approaches that differ on whether the properties model the system state after the occurrence of each event or at a fixed time rate. Model checking of timed properties is made possible by translating them into the existing untimed framework.

No abstract available.

In this paper we discuss a model-based approach to verifying process interactions for coordinated Web service compositions. The approach uses finite state machine representations of Web service orchestrations and assigns semantics to the distributed process interactions. The move towards implementing Web service compositions by multiple interested parties as a form of distributed system architecture motivates the need for supporting compatibility verification of activities and transactions in all the processes. The described approach is supported by a suite of cooperating tools for specification, formal modeling and providing verification results from orchestrated Web service interactions.

Constructing rigorous models for analysing the behaviour of concurrent and distributed systems is a complex task. Our aim is to facilitate model construction. Scenarios provide simple, intuitive, example based descriptions of the behaviour of component instances in the context of a simplified architecture instance. The specific architecture instance is generally chosen to provide sufficient context to indicate the expected behaviour of particular instances of component types to be used in the real system. Existing synthesis techniques provide mechanisms for building behaviour models for these simplified and specific architectural settings. However, the behaviour models required are those for the full generality of the system architecture, and not the simplified architecture used for scenarios. In this paper we exploit architectural information in the context of behaviour model synthesis from scenarios. Software architecture descriptions give the necessary contextual information so that component instance behaviour can be generalised to component type behaviour. Furthermore, architecture description languages can be used to describe the complex architectures in which the generalised behaviours need to be instantiated. Thus, architectural information used in conjunction with scenario-based model synthesis can support both model construction and elaboration, where the behaviour derived from simple architecture fragments can be instantiated in more complex ones.

Behavior modeling has proved to be successful in helping uncover design flaws of concurrent and distributed systems. Nevertheless, it has not had a widespread impact on practitioners because model construction remains a difficult task and because the benefits of behavior analysis appear at the end of the model construction effort. In contrast, scenario-based specifications have a wide acceptance in industry and are well suited for developing first approximations of intended behavior; however, they are still maturing with respect to rigorous semantics and analysis tools.This article proposes a process for elaborating system behavior that exploits the potential benefits of behavior modeling and scenario-based specifications yet ameliorates their shortcomings. The concept that drives the elaboration process is that of implied scenarios . Implied scenarios identify gaps in scenario-based specifications that arise from specifying the global behavior of a system that will be implemented component-wise. They are the result of a mismatch between the behavioral and architectural aspects of scenario-based specifications. Due to the partial nature of scenario-based specifications, implied scenarios need to be validated as desired or undesired behavior. The scenario specifications are then updated accordingly with new positive or negative scenarios. By iteratively detecting and validating implied scenarios, it is possible to incrementally elaborate the behavior described both in the scenario-based specification and models. The proposed elaboration process starts with a message sequence chart (MSC) specification that includes basic, high-level and negative MSCs. Implied scenario detection is performed by synthesis and automated analysis of behavior models. The final outcome consists of four artifacts: (1) an MSC specification that has been evolved from its original form to cover important aspects of the concurrent nature of the system that were under-specified or absent in the original specification, (2) a behavior model that captures the component structure of the system that, combined with (3) a constraint model and (4) a property model that provides the basis for modeling and reasoning about system design.

The development of complex systems invariably involves many stakeholders who have different perspectives on the problem they are addressing, the system being developed, and the process by which it is being developed. The ViewPoints framework was devised to provide an organisational framework in which these different. perspectives, and their relationships, could be explicitly represented and analysed The framework acknowledges the inevitability of multiple inconsistent views, promotes separation of concerns, and encourages decentralised specification while providing support for integration through relationships and composition. In this paper, we reflect on the ViewPoints framework, current work and future research directions.

In this paper, we discuss a model-based approach to verifying Web service compositions for Web service implementations. The approach supports verification against specification models and assigns semantics to the behavior of implementation model so as to confirm expected results for both the designer and implementer. Specifications of the design are modeled in UML (Unified Modeling Language), in the form of message sequence charts (MSC), and mechanically compiled into the finite state process notation (FSP) to concisely describe and reason about the concurrent programs. Implementations are mechanically translated to FSP to allow a trace equivalence verification process to be performed. By providing early design verification, the implementation, testing, and deployment of Web service compositions can be eased through the understanding of the differences, limitations and undesirable traces allowed by the composition. The approach is supported by a suite of cooperating tools for specification, formal modeling and trace animation of the composition workflow.

State machine based formalisms such as labelled transition systems (LTS) are generally assumed to be complete descriptions of system behaviour at some level of abstraction: if a labelled transition system cannot exhibit a certain sequence of actions, it is assumed that the system or component it models cannot or should not exhibit that sequence. This assumption is a valid one at the end of the modelling effort when reasoning about properties of the completed model. However, it is not a valid assumption when behaviour models are in the process of being developed. In this setting, the distinction between proscribed behaviour and behaviour that has not yet been defined is an important one. Knowing where the gaps are in a behaviour model permits the presentation of meaningful questions to stakeholders, which in turn can lead to model exploration and thus more comprehensive descriptions of the system behaviour. In this paper we propose using partial labelled transition systems (PLTS) to capture what remains to be defined of the system behaviour. In the context of scenario synthesis, we show that PLTSs can be used to support the iterative incremental elaboration of behaviour models.

Scenario-based specifications such as Message Sequence Charts (MSCs) are useful as part of a requirements specification. A scenario is a partial story, describing how system components, the environment, and users work concurrently and interact in order to provide system level functionality. Scenarios need to be combined to provide a more complete description of system behavior. Consequently, scenario synthesis is central to the effective use of scenario descriptions. How should a set of scenarios be interpreted? How do they relate to one another? What is the underlying semantics? What assumptions are made when synthesizing behavior models from multiple scenarios? In this paper, we present an approach to scenario synthesis based on a clear sound semantics, which can support and integrate many of the existing approaches to scenario synthesis. The contributions of the paper are threefold. We first define an MSC language with sound abstract semantics in terms of labeled transition systems and parallel composition. The language integrates existing approaches based on scenario composition by using high-level MSCs (hMSCs) and those based on state identification by introducing explicit component state labeling. This combination allows stakeholders to break up scenario specifications into manageable parts and reuse scenarios using hMCSs; it also allows them to introduce additional domain-specific information and general assumptions explicitly into the scenario specification using state labels. Second, we provide a sound synthesis algorithm which translates scenarios into a behavioral specification in the form of Finite Sequential Processes. This specification can be analyzed with the Labeled Transition System Analyzer using model checking and animation. Finally, we demonstrate how many of the assumptions embedded in existing synthesis approaches can be made explicit and modeled in our approach. Thus, we provide the basis for a common approach to scenario-based specification, synthesis, and analysis.

Scenario-based specifications such as Message Sequence Charts (MSCs) are popular for requirement elicitation and specification. MSCs describe two distinct aspects of a system: on the one hand they provide examples of intended system behaviour and on the other they outline the system architecture. A mismatch between architecture and behaviour may give rise to implied scenarios. Implied scenarios occur because a component's local view of the system state is insufficient to enforce specified system behaviour. An implied scenario indicates a gap in the MSC specification that needs to be clarified. It may simply mean that an acceptable scenario has been overlooked and should be added to the scenario specification. Alternatively, it may represent an unacceptable behaviour which should be documented and avoided in the final implementation. Thus implied scenarios can be used to iteratively drive requirements elicitation. However, in order to do so, tools for coping with rejected implied scenarios are needed. The contributions of this paper are twofold. Firstly, we define a language for describing negative scenarios. Secondly, we complement existing implied scenario detection methods with techniques for accommodating negative scenarios.

Scenario-based specifications such as Message Sequence Charts (MSCs) are becoming increasingly popular as part of a requirements specification. Our objective is to facilitate the development of behaviour models in conjunction with scenarios. In this paper, we first present an MSC language with semantics in terms of labelled transition systems and parallel composition. The language integrates existing languages based on the use of high-level MSCs (hMSCs) and on identifying component states. This integration allows stakeholders to break up scenario specifications into manageable parts using hMCSs and to explicitly introduce additional information and domain-specific or other assumptions using state labels. Secondly, we present an algorithm, implemented in Java, which translates scenarios into a specification in the form of Finite Sequential Processes. This can then be fed to the labelled transition system analyser for model checking and animation. Finally we show how many of the assumptions embedded in existing synthesis approaches can be translated into our approach. Thus we provide the basis of a common workbench for supporting MSC specifications, behaviour synthesis and analysis.

We argue that the evolution of requirements specifications can be supported by a cycle composed of two phases: analysis and revision. We investigate an instance of such a cycle, which combines two techniques of logical abduction and inductive learning to analyze and revise specifications respectively.

Scenario-based specifications such as Message Sequence Charts (MSCs) are becoming increasingly popular as part of a requirements specification. Scenario describe how system components, the environment and users work concurrently and interact in order to provide system level functionality. Each scenario is a partial story which, when combined with other scenarios, should conform to provide a complete system description. However, although it is possible to build a set of components such that each component behaves in accordance with the set of scenarios, their composition may not provide the required system behaviour. Implied scenarios may appear as a result of unexpected component interaction. In this paper, we present an algorithm that builds a labelled transition system (LTS) behaviour model that describes the closest possible implementation for a specification based on basic and high-level MSCs. We also present a technique for detecting and providing feedback on the existence of implied scenarios. We have integrated these procedures into the Labelled Transition System Analyser (LTSA), which allows for model checking and animation of the behaviour model.

Graphical animation is a way of visualizing the behavior of design models. This visualization is of use in validating a design model against informally specified requirements and in interpreting the meaning and significance of analysis results in relation to the problem domain. In this paper we describe how behavior models specified by Labeled Transition Systems (LTS) can drive graphical animations. The semantic framework for the approach is based on Timed Automata. Animations are described by an XML document that is used to generate a set of JavaBeans. The elaborated JavaBeans perform the animation actions as directed by the LTS model.

Software vendors rarely acknowledge their debt to research, indeed often are unaware of it, and rarely even appreciate the importance of such acknowledgement. The long lead times, and tortuous adoption paths, for software engineering research contributions also cloud perception of the actual source of popularly adopted software engineering technologies.

The purpose of this panel is to introduce the Impact Project to the community, and to engage the community in a broad ranging discussion of the project's goals, approaches, and methods. Some of the project's early findings and directions will be presented.

Effective analysis and evolution of existing distributed software systems rely to great an extent on the ability to recognise implemented executable components, particularly their constituent modules. Traditionally, this information is obtained via manual examination of configuration files and the source code directory hierarchy. However both types of artifact are limited in distinguishing which modules are used exclusively by each executable component. This exclusivity distinction is important in that it helps to understand the components' unique functionalities and their potential runtime behaviour. This paper presents a module classification technique that can facilitate automatic recognition of executable component modules in a distributed system. In contrast to existing approaches, the technique explicitly distinguishes component exclusive modules from modules shared by multiple components. The paper illustrates the benefits of the technique by reporting on the results of a case study where it has been useful to (a) revealing component exclusive modules in the source code for the field distributed programming environment; and (b) investigating some aspects of an implicit-invocation model of field described elsewhere. Applications of the technique to other software engineering tasks, such as change impact analysis, reuse and restructuring, are also discussed.

The software architecture of a distributed program can be represented by a hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compositional reachability analysis (CRA) is a promising state reduction technique which can be automated and used in stages to derive the overall behavior of a distributed program based on its architecture. CRA is particularly suitable for the analysis of programs that are subject to evolutionary change. When a program evolves, only the behaviors of those subsystems affected by the change need be reevaluated. The technique however has a limitation. The properties available for analysis are constrained by the set of actions that remain globally observable. Properties involving actions encapsulated by subsystems may therefore not be analyzed. In this article, we enhance the CRA technique to check safety properties which may contain actions that are not globally observable. To achieve this, the state machine model is augmented with a special trap state labeled as π. We propose a scheme to transform, in stages, a property that involves hidden actions to one that involves only globally observable actions. The enhanced technique also includes a mechanism aiming at reducing the debugging effort. The technique is illustrated using a gas station system example.

No abstract available.

The paper addresses the problem of structuring and managing large distributed systems constructed from many distributed objects. Specifically, the paper proposes a component model which can be used to compose objects into manageable entities. Components are specified using Darwin, an architecture description language developed by the authors. A mapping of distributed objects into Darwin components is described together with an outline of how Darwin and its associated tools are implemented in a CORBA compliant environment.

Much of the recent work on Architecture Description Languages (ADL) has concentrated on specifying organisations of components and connectors which are static. When the ADL specification is used to drive system construction, then the structure of the resulting system in terms of its component instances and their interconnection is fixed. This paper examines ADL features which permit the description of dynamic software architectures in which the organisation of components and connectors may change during system execution.The paper outlines examples of language features which support dynamic structure. These examples are taken from Darwin, a language used to describe distributed system structure. An operational semantics for these features is presented in the π-calculus, together with a discussion of their advantages and limitations. The paper discusses some general approaches to dynamic architecture description suggested by these examples.

Behavior analysis of complex distributed systems has led to the search for enhanced reachability analysis techniques which support modularity and which control the state explosion problem. While modularity has been achieved, state explosion in still a problem. Indeed, this problem may even be exacerbated, as a locally minimized subsystem may contain many states and transitions forbidden by its environment or context. Context constraints, specified as interface processes, are restrictions imposed by the environment on subsystem behavior. Recent research has suggested that the state explosion problem can be effectively controlled if context constraints are incorporated in compositional reachability analysis (CRA). Although theoretically very promising, the approach has rarely been used in practice because it generally requires a more complex computational model and does not contain a mechanism to derive context constraints automatically. This article presents a technique to automate the approach while using a similar computational model to that of CRA. Context constraints are derived automatically, based on a set of sufficient conditions for these constraints to be transparently included when building reachability graphs. As a result, the global reachability graph generated using the derived constraints is shown to be observationally equivalent to that generated by CRA without the inclusion of context constraints. Constraints can also be specified explicitly by users, based on their application knowledge. Erroneous constraints which contravene transparency can be identified together with an indication of the error sources. User-specified constraints can be combined with those generated automatically. The technique is illustrated using a clients/server system and other examples.

The ViewPoints framework for distributed and concurrent software engineering provides an alternative approach to traditional centralised software development environments.WJe investigate the use of decentralised process models to drive consistency checking and conflict resolution in this framework.Our process models use pattern matching on local development histories to determine the particular situation (state) of the development process, and employ rules to trigger situationdependent assistance to the user.We describe how communication between such process models facilitates the decentralised management of explicitly defined consistency constraints in the ViewPoints framework.

The software architecture of a distributed system can be described as a hierarchical composition of subsystems, with SIGSOFT '95 Washington, D. C.. USA

Distributed applications spanning multiple nodes should he capable of providing fast response. Computation servers equipped with powerful processors and large memories can improve performance by better utilising system resources such as offloading overloaded nodes. A computation service may comprise all the nodes of the system (in case all are equipped with the required resources) or a small subset such as provided by a pool of computation servers (as in Amoeba). In both cases there can be a large number of service providers (compute servers). A server selection service is required to choose the most suitable server to provide the service. This paper is concerned with the design of adaptive computation server selection with scale recognised as a primary design and implementation factor. Adaptive system partitioning into domains is advocated as a key design principle for scalability. The model is demonstrated with compute-server selection using adaptive partitioning compared to the same service using random selection and probing.>

Automated behavior analysis is a valuable technique in the development and maintenance of distributed systems. In this paper, we present a tractable dataflow analysis technique for the detection of unreachable states and actions in distributed systems. The technique follows an approximate approach described by Reif and Smolka, but delivers a more accurate result in assessing unreachable states and actions. The higher accuracy is achieved by the use of two concepts: action dependency and history sets. Although the technique does not exhaustively detect all possible errors, it detects nontrivial errors with a worst-case complexity quadratic to the system size. It can be automated and applied to systems with arbitrary loops and nondeterministic structures. The technique thus provides practical and tractable behavior analysis for preliminary designs of distributed systems. This makes it an ideal candidate for an interactive checker in software development tools. The technique is illustrated with case studies of a pump control system and an erroneous distributed program. Results from a prototype implementation are presented.>

The development of most large and complex systems necessarily involves many people-each with their own perspectives on the system defined by their knowledge, responsibilities, and commitments. To address this we have advocated distributed development of specifications from multiple perspectives. However, this leads to problems of identifying and handling inconsistencies between such perspectives. Maintaining absolute consistency is not always possible. Often this is not even desirable since this can unnecessarily constrain the development process, and can lead to the loss of important information. Indeed since the real-world forces us to work with inconsistencies, we should formalize some of the usually informal or extra-logical ways of responding to them. This is not necessarily done by eradicating inconsistencies but rather by supplying logical rules specifying how we should act on them. To achieve this, we combine two lines of existing research: the ViewPoints framework for perspective development, interaction and organization, and a logic-based approach to inconsistency handling. This paper presents our technique for inconsistency handling in the ViewPoints framework by using simple examples.>

Composite systems are generally comprised of heterogeneous components whose specifications are developed by many development participants. The requirements of such systems are invariably elicited from multiple perspectives that overlap, complement, and contradict each other. Furthermore, these requirements are generally developed and specified using multiple methods and notations, respectively. It is therefore necessary to express and check the relationships between the resultant specification fragments. We deploy multiple ViewPoints that hold partial requirements specifications, described and developed using different representation schemes and development strategies. We discuss the notion of inter-ViewPoint communication in the context of this ViewPoints framework, and propose a general model for ViewPoint interaction and integration. We elaborate on some of the requirements for expressing and enacting inter-ViewPoint relationships-the vehicles for consistency checking and inconsistency management. Finally, though we use simple fragments of the requirements specification method CORE to illustrate various components of our work, we also outline a number of larger case studies that we have used to validate our framework. Our computer-based ViewPoints support environment, The Viewer, is also briefly described.>

The question of specifying systems or domains is addressed. Among the issues discussed are: the requirements of first-class connectors for domain specifications; the use of application frameworks as domain specifications; the role of connectors in domain specifications; domain model specification; the question of what precisely is meant by a domain of the question of reuse; and the difficulty in producing sound domain specifications.>

Compositional techniques have been proposed for traditional reachability analysis in order to introduce modularity and to control the state explosion problem. While modularity has been achived, state explosion is still a problem. Indeed, this problem may even be exacerbated as a locally minimised subsystem may contain many states and transitions forbidden by its context or environments. This paper presents a method to alleviate this problem effectively by including context constraints in local subsystem minimisation. The global behaviour generated using the method is observationally equivalent to that generated by compositional reachability analysis without the inclusion of context constraints.Context constraints, specified as interface processes, are restrictions imposed by the environment on subsystem behaviour. The minimisation produces a simplified machine that describes the behaviour of the subsystem constrained by its context. This machine can also be used as a substitute for the original subsystem in the subsequent steps of the compositional reachability analysis. Interface processes capturing context constraints can be specified by users or automatically constructd using a simple algorithm. The concepts in the paper are illustrated with a clients/server system.

This paper describes the integrated engineering study scheme, based around a set of 4 year MEng programmes of study, established by Imperial College. The paper outlines the rationale for the scheme and gives an account of its constituent programmes of study and the curriculum. The organisation and pattern of teaching, student workload and assessment methods are discussed. A detailed comparison of the scheme with the proposals and recommendations of the important model curricula are given.

This paper outlines a framework which supports the use of multiple perspectives in system development, and provides a means for developing and applying systems design methods. The framework uses "viewpoints" to partition the system specification, the development method and the formal representations used to express the system specifications. This VOSE (viewpoint-oriented systems engineering) framework can be used to support the design of heterogeneous and composite systems. We illustrate the use of the framework with a small example drawn from composite system development and give an account of prototype automated tools based on the framework.

A method for qualitative and quantitative analysis of load sharing algorithms is presented, using a number of well known examples as illustration. Algorithm design choice are considered with respect to the main activities of information dissemination and allocation decision making. It is argued that nodes must be capable of making local decisions, and for this efficient state, dissemination techniques are necessary. Activities related to remote execution should be bounded and restricted to a small proportion of the activity of the system. The quantitative analysis provides both performance and efficiency measures, including consideration of the load and delay characteristics of the environment. To assess stability, which is also a precondition for scalability, the authors introduce and measure the load-sharing hit-ratio, the ratio of remote execution requests concluded successfully. Using their analysis method, they are able to suggest improvements to some published algorithms.>

A constructive design approach to distributed systems is described. The approach is illustrated by a model airport shuttle system, which is implemented in an environment for distributed programming called Conic. The main principles on which the constructive approach is based are those of explicit system structure and context-independent components. Structure is explicitly described and preserved during the software development process, from initial design to actual system construction and evolution. Thus the main structural design information is retained in the constructed system itself. The second principle that of context independence of components, reduces the design and implementation effort by facilitating early identification of component types and component interface specifications.>

A model for dynamic change management which separates structural concerns from component application concerns is presented. This separation of concerns permits the formulation of general structural rules for change at the configuration level without the need to consider application state, and the specification of application component actions without prior knowledge of the actual structural changes which may be introduced. In addition, the changes can be applied in such a way so as to leave the modified system in a consistent state, and cause no disturbance to the unaffected part of the operational system. The model is applied to an example problem, 'evolving philosophers'. The principles of this model have been implemented and tested in the Conic environment for distributed systems.>

The Conic environment provides a language-based approach to the building of distributed systems which combines the simplicity and safety of a language approach with the flexibility and accessibility of an operating systems approach. It provides a comprehensive set of tools for program compilation, configuration, debugging, and execution in a distributed environment. A separate configuration language is used to specify the configuration of software components into logical nodes. This provides a concise configuration description and facilitates the reuse of program components in different configurations. Applications are constructed as sets of one or more interconnected logical nodes. Arbitrary, incremental change is supported by dynamic configuration. In addition, the system provides user-transparent datatype transformation between heterogeneous processors. Applications may be run on a mixed set of interconnected computers running the Unix operating system and on base target machines with no resident operating system. The basic principles adopted in the construction of the Conic environment are outlined and the configuration and run-time facilities provided are described.>

Abstract Requirements analysis has been recognized as one of the most critical and difficult tasks in software engineering. The need for tool support is essential. This paper reports some work done to provide such support for interpretation and validation of requirements specifications by animation. The Animator provides facilities for the selection and execution of a transaction to reflect the specified behaviour of a particular scenario specified in the requirements specification. Actions are described in terms of input‐output mappings and or functions with pattern matching. Simple rules can be specified to control the triggering of actions. In addition, facilities are provided to replay and interact with transactions. User interaction during animation includes the ability to change data values or role play selected actions as desired. A full graphical interface is supported. The approach has been tested by the provision of an Animator for the requirements analysis method CORE and an associated ‘Analyst Workstation’. Animation has been tested on a number of small examples and a major case study. This paper describes the Animator, justifies the approach taken and discusses experience and future work.

Dynamic system configuration is the ability to modify and extend a system while it is running. The facility is a requirement in large distributed systems where it may not be possible or economic to stop the entire system to allow modification to part of its hardware or software. It is also useful during production of the system to aid incremental integration of component parts, and during operation to aid system evolution. The paper introduces a model of the configuration process which permits dynamic incremental modification and extension. Using this model we determine the properties required by languages and their execution environments to support dynamic configuration. CONIC, the distributed system which has been developed at Imperial College with the specific objective of supporting dynamic configuration, is described to illustrate the feasibility of the model.

Abstract The concept of an invariant assertion has been shown by Hoare to be central to the problem of proving correctness of data representation in a program. A consequent approach for program design is to establish the parts of an overall invariant which characterize the components of the design. In this way it is feasible to synthesize a verified program. There is a gulf between verification theory and practical reality in this area, but the SIMULA class concept is close to the data representation technique required for such an approach. Some of the benefits and problems of this approach to design have been explored by the development of a SIMULA program to simulate a bounded delay resource allocation strategy in a job scheduling environment.