With the growing adoption of AI-based systems, effective risk management is more important than ever. Obstacle analysis is a requirements engineering technique introduced three decades ago for designing dependable software systems despite failures, exceptions, and unforeseen behaviors in both the software and its environment. An obstacle is an undesirable situation that violates a stakeholder goal, an environment assumption, or a software requirement. Obstacles include safety hazards, security threats, user errors, and other adverse situations. Obstacle analysis provides a structured, systematic approach for identifying, analyzing, and resolving obstacles at the requirements level. In this retrospective paper, we summarize the original technique and discuss its impacts on research and practice. We also propose a research agenda to extend obstacle analysis to address emerging challenges in AI systems engineering.

The engineering of high-quality software requirements generally relies on properties and assumptions about the environment in which the software-to-be has to operate. Such properties and assumptions, referred to as environment conditions in this paper, are highly subject to change over time or from one software variant to another. As a consequence, the requirements engineered for a specific set of environment conditions may no longer be adequate, complete and consistent for another set.

Software systems are deployed in environments that keep changing over time. They should therefore adapt to changing conditions to meet their requirements. The satisfaction rate of these requirements depends on the rate at which adverse conditions prevent their satisfaction. Obstacle analysis is a goal-oriented form of risk analysis for requirements engineering (RE), whereby obstacles to system goals are identified, assessed, and resolved through countermeasures. The selection of effective countermeasures relies on environment assumptions and on the assessed likelihood and criticality of the corresponding obstacles. Those various factors estimated at RE time may, however, evolve at system runtime. To meet the system’s goals under changing conditions, this article proposes to defer obstacle resolution to system runtime. Techniques are presented for monitoring obstacle satisfaction rates; deciding when adaptation should be triggered; and adapting the system on-the-fly to countermeasures that are more effective. The approach relies on a model where goals and obstacles are refined and specified in a probabilistic linear temporal logic. The techniques allow for monitoring the satisfaction rate of probabilistic leaf obstacles; determining the severity of obstacle consequences on goal satisfaction rates computed from the monitored obstacle satisfaction rates; and shifting to countermeasures that better meet the required goal satisfaction rates. Our approach is evaluated on fragments of an ambulance dispatching system.

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.

Requirements engineers are faced with multiple sources of uncertainty. In particular, the extent to which the identified software requirements and environment assumptions are adequate and sufficiently complete is uncertain; the extent to which they will be satisfied in the system-to-be is uncertain; and the extent to which obstacles to their satisfaction will occur is uncertain. The resolution of such domain-level uncertainty requires estimations of the likelihood that those different types of situations may or may not occur. However, the extent to which the resulting estimates are accurate is uncertain as well. This meta-level uncertainty limits current risk-based methods for requirements engineering. The paper introduces a quantitative approach for managing it. An earlier formal framework for probabilistic goals and obstacles is extended to explicitly cope with uncertainties about estimates of likelihoods of fine-grained obstacles to goal satisfaction. Such estimates are elicited from multiple sources and combined in order to reduce their uncertainty margins. The combined estimates and their uncertainties are up-propagated through obstacle refinement trees and then through the system's goal model. Two metrics are introduced for measuring problematic uncertainties. When applied to the probability distributions obtained by up-propagation to the top-level goals, the metrics allow critical leaf obstacles with most problematic uncertainty margins to be highlighted. The proposed approach is evaluated on excerpts from a real ambulance dispatching system.

Missing requirements are known to be among the major sources of software failure. Incompleteness often results from poor anticipation of what could go wrong with an over-ideal system. Obstacle analysis is a model-based, goal-anchored form of risk analysis aimed at identifying, assessing and resolving exceptional conditions that may obstruct the behavioral goals of the target system. The obstacle resolution step is obviously crucial as it should result in more adequate and more complete requirements. In contrast with obstacle identification and assessment, however, this step has little support beyond a palette of resolution operators encoding tactics for producing isolated countermeasures to single risks. In particular, there is no single clue to date as to where and how such countermeasures should be integrated within a more robust goal model. To address this problem, the paper describes a systematic technique for integrating obstacle resolutions as countermeasure goals into goal models. The technique is shown to guarantee progress towards a complete goal model; it preserves the correctness of refinements in the overall model; and keeps the original, ideal model visible to avoid cluttering the latter with a combinatorial blow-up of exceptional cases. To allow for this, the goal specification language is slightly extended in order to capture exceptions to goals seperately and distinguish normal situations from exceptional ones. The proposed technique is evaluated on a non-trivial ambulance dispatching system.

Decision-based processes are composed of tasks whose application may depend on explicit decisions relying on the state of the process environment. In specific domains such as healthcare, decision-based processes are often complex and critical in terms of timing and resources. The paper presents a variety of tool-supported techniques for analyzing models of such processes. The analyses allow a variety of errors to be detected early and incrementally on partial models, notably: inadequate decisions resulting from inaccurate or outdated information about the environment state; incomplete decisions; non-deterministic task selections; unreachable tasks along process paths; and violations of non-functional process requirements involving time, resources or costs. The proposed techniques are based on different instantiations of the same generic algorithm that propagates decorations iteratively through the process model. This algorithm in particular allows event-based models to be automatically decorated with state-based invariants. A formal language supporting both event-based and state-based specifications is introduced as a process modeling language to enable such analyses. This language mimics the informal flowcharts commonly used by process stakeholders. It extends High-Level Message Sequence Charts with guards on task-related and environment-related variables. The language provides constructs for specifying task compositions, task refinements, decision trees, multi-agent communication scenarios, and time and resource constraints. The proposed techniques are demonstrated on the incremental building and analysis of a complex model of a real protocol for cancer therapy.

The effectiveness of model-driven engineering relies on our ability to build high quality models. This task is intrinsically difficult. We need to produce sufficiently complete, adequate, consistent, and well-structured models from incomplete, imprecise, and sparse material originating from multiple, often conflicting sources. The systems we need to consider generally comprises software components, devices and people.

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.

Requirements completeness is among the most critical and difficult software engineering challenges. Missing requirements often result from poor risk analysis at requirements engineering time. Obstacle analysis is a goal-oriented form of risk analysis aimed at anticipating exceptional conditions in which the software should behave adequately. In the identify-assess-control cycles of such analysis, the assessment step is not well supported by current techniques. This step is concerned with evaluating how likely the obstacles to goals are and how likely and severe their consequences are. Those key factors drive the selection of most appropriate countermeasures to be integrated in the system goal model for increased completeness. Moreover, obstacles to probabilistic goals are currently not supported; such goals prescribe that some corresponding target property should be satisfied in at least X% of the cases. The paper presents a probabilistic framework for goal specification and obstacle assessment. The specification language for goals and obstacles is extended with a probabilistic layer where probabilities have a precise semantics grounded on system-specific phenomena. The probability of a root obstacle to a goal is thereby computed by up-propagation of probabilities of finer-grained obstacles through the obstacle refinement tree. The probability and severity of obstacle consequences is in turn computed by up-propagation from the obstructed leaf goals through the goal refinement graph. The paper shows how the computed information can be used to prioritize obstacles for countermeasure selection towards a more complete and robust goal model. The framework is evaluated on a non-trivial carpooling support system.

Many of us lost a close colleague on November 28, 2010.More than that: we lost a friend.One that we used to meet regularly, all over the world, always listening to us, making interesting comments and suggestions on our work, joking on every occasion and making us discover how much fun our business is.Rather than reviewing his work in detail, this note puts more focus on Michel's rich personality, with the hope that it will bring back fond memories among those who were lucky enough to share some good times with him.The style is intended to be personal and informal.Michel would have hated anything different, to be sure.Born in 1938 in Brussels, Michel completed his master's degree in Mathematics at the Université catholique de Louvain (UCL) in 1962.After 2 years of civil service as a maths teacher in Katanga (Congo), he entered the MBLE Research Laboratory in Brussels in 1964 (MBLE stands for "Manufacture Belge de Lampes et matériel Electrique").This was a branch of Philips Research Labs specifically dedicated to background research in applied mathematics and computing science.After 18 years of research in programming languages, formal semantics, program analysis and concurrency at MBLE, he joined the newly founded department of Computing Science at UCL in 1982 with new interests in diverse areas such as proof systems, control theory and dynamical systems.Michel contributed to the PhD work of dozens of people in Belgium and France, as supervisor or contributor, without ever having been interested in getting a PhD himself.He received a Doctorate Honoris Causa from the Université Joseph Fourier in Grenoble (France) and was a member of the Informatics section of the Academy of Europe.Michel was an Emeritus Professor at UCL since 2003.The two of us were face to face in the same office at MBLE Research for 10 years (1970)(1971)(1972)(1973)(1974)(1975)(1976)(1977)(1978)(1979)(1980), and had adjacent rooms at UCL for another decade (1993)(1994)(1995)(1996)(1997)(1998)(1999)(2000)(2001)(2002)(2003).Programs, 1972) as the precursor paper on abstract interpretation.This paper and others he wrote around that time on program verification and type discovery are heavily cited in the paper generally considered to have opened the field (Cousot and Cousot, 1977).The technique described in his 1972 paper was simultaneously implemented in Paul Branquart's optimizing compiler for Algol68, confirming how powerful it was. Many consider Michel's paper Calculating Properties of Programs by Valuations on Specific Models (Proc. ACM Conference on Proving Assertions about

The effectiveness of MDE relies on our ability to build high-quality models. This task is intrinsically difficult. We need to produce sufficiently complete, adequate, consistent, and well-structured models from incomplete, imprecise, and sparse material originating from multiple, often conflicting sources. The system we need to consider in the early stages comprises software and environment components including people and devices.

Process models capture tasks performed by agents together with their control flow. Building and analyzing such models is important but difficult in certain areas such as safety-critical healthcare processes. Tool-supported techniques are needed to find and correct flaws in such processes. On another hand, event-based formalisms such as Labeled Transition Systems (LTS) prove effective for analyzing agent behaviors. The paper describes a blend of state-based and event-based techniques for analyzing task models involving decisions. The input models are specified as guarded high-level message sequence charts, a language allowing us to integrate material provided by stakeholders such as multi-agent scenarios, decision trees, and flowchart fragments. The input models are compiled into guarded LTS, where transition guards on fluents support the integration of state-based and event-based analysis. The techniques supported by our tool include model checking against process-specific properties, invariant generation, and the detection of incompleteness, unreachability, and undesirable non-determinism in process decisions. They are based on a trace semantics of process models, defined in terms of guarded LTS, which are in turn defined in terms of pure LTS. The techniques complement our previous palette for synthesizing behavior models from scenarios and goals. The paper also describes our preliminary experience in analyzing cancer treatment processes using these techniques.

This mini-tutorial overviews a blend of complementary techniques for constructing multi-view models for RE. Requirements engineering techniques are faced with a recurring problem of focus and structure. Elicitation techniques raise the problem of focussing and structuring elicitation sessions and artefacts. Evaluation techniques raise the problem of identifying and comparing items at a common level of abstraction and granularity for risk analysis, conflict management, option selection, or prioritization. Specification techniques offer mechanisms for structuring specifications but do not tell us much on how a complex structure should be built through such mechanisms. For quality assurance, inspection techniques are more effective if inspections can be focussed on structured specifications. Validation and verification techniques require the availability of structured specifications as well. Likewise, evolution techniques are more effective when a rich structure is available for defining change units, granularities of traceable items, built-in derivation links, and satisfaction arguments to be replayed in case of change.

Getting the right software requirements under the right environment assumptions is a critical precondition for developing the right software. This task is intrinsically difficult. We need to produce a complete, adequate, consistent, and well-structured set of measurable requirements and assumptions from incomplete, imprecise, and sparse material originating from multiple, often conflicting sources. The system we need to consider comprises software and environment components including people and devices.

Models are increasingly recognized as an effective means for elaborating requirements and exploring designs. For complex systems, model building is far from an easy task. Efforts were therefore recently made to automate parts of this process, notably, by synthesizing behavior models from scenarios of interactions between the software-to-be and its environment. In particular, our previous interactive synthesizer generates labelled transition systems (LTS) from simple message sequence charts (MSC) provided by end-users. Compared with others, the synthesizer requires no additional input such as state or flowcharting information. User interactions consist in simple scenarios generated by the synthesizer that the user has to classify as example or counterexample of desired behavior.Experience with this approach showed that the number of such scenario questions may become fairly large in interaction-intensive applications such as web applications. In this paper, we extend our model synthesis technique by injecting additional information into the synthesizer, when available, in order to constrain induction and prune the inductive search space. Additional information may include global definitions of fluents that link interaction events and atomic assertions; declarative properties of the domain; behavior models of external components; and goals that the software system is expected to satisfy. We provide comparative data on increasingly complex examples to show how effective such constraints are in reducing the number of scenario questions and in increasing the adequacy of the synthesized model. As goals and domain properties might not be easily provided by users, the paper also shows how our synthesizer generates a significant class of them automatically from the available scenarios. As a side-effect, our work provides additional evidence on the synergistic links between scenarios, goals, and state machines for model-driven engineering of requirements and designs.

Growing attention is being paid to application security at requirements engineering time. Confidentiality is a particular subclass of security concerns that requires sensitive information to never be disclosed to unauthorized agents. Disclosure refers to undesired knowledge states of such agents. In previous work we have extended our requirements specification framework with epistemic constructs for capturing what agents may or may not know about the application. Roughly, an agent knows some property if the latter is found in the agent's memory.This paper makes the semantics of such constructs further precise through a formal model of how sensitive information may appear or disappear in an agent's memory. Based on this extended framework, a catalog of specification patterns is proposed to codify families of confidentiality requirements. A proof-of-concept tool is presented for early checking of requirements models against such confidentiality patterns. In case of violation, the counterexample scenarios generated by the tool show how an unauthorized agent may acquire confidential knowledge. Counter-measures should then be devised to produce further confidentiality requirements.

Requirements-related scenarios capture typical examples of system behaviors through sequences of desired interactions between the software-to-be and its environment. Their concrete, narrative style of expression makes them very effective for eliciting software requirements and for validating behavior models. However, scenarios raise coverage problems as they only capture partial histories of interaction among-system component instances. Moreover, they often leave the actual requirements implicit. Numerous efforts have therefore been made recently to synthesize requirements or behavior models inductively from scenarios. Two problems arise from those efforts. On the one hand, the, scenarios must be complemented with additional input such as state assertions along episodes or flowcharts on such episodes. This makes such techniques difficult to use by the nonexpert end-users who provide the scenarios. On the other hand, the generated state machines may be hard to understand as their nodes generally convey no domain- specific properties. Their validation by analysts, complementary to model checking and animation by may therefore be quite difficult. This paper describes tool-supported techniques that overcome those two problems. Our tool generates a labeled transition system (LTS) for each system component from simple forms of message sequence charts (MSC) taken as examples or counterexamples of desired behavior. No additional input is required. A global LTS for the entire system is synthesized first. This LTS covers all scenario examples and excludes all counterexamples. It is inductively generated through an interactive procedure that extends known learning techniques for grammar induction. The procedure is incremental on training examples. It interactively produces additional scenarios that the end-user has to classify as examples or counterexamples of desired behavior. The LTS synthesis procedure may thus also be used independently for requirements elicitation through scenario questions generated by the tool. The synthesized system LTS is then projected on local LTS for each system component. For model validation by analysts, the tool generates state invariants that decorate the nodes of the local LTS.

Caring for security at requirements engineering time is a message that has finally received some attention recently. However, it is not yet very clear how to achieve this systematically through the various stages of the requirements engineering process. The paper presents a constructive approach to the modeling, specification and analysis of application-specific security requirements. The method is based on a goal-oriented framework for generating and resolving obstacles to goal satisfaction. The extended framework addresses malicious obstacles (called anti-goals) set up by attackers to threaten security goals. Threat trees are built systematically through anti-goal refinement until leaf nodes are derived that are either software vulnerabilities observable by the attacker or anti-requirements implementable by this attacker. New security requirements are then obtained as countermeasures by application of threat resolution operators to the specification of the anti-requirements and vulnerabilities revealed by the analysis. The paper also introduces formal epistemic specification constructs and patterns that may be used to support a formal derivation and analysis process. The method is illustrated on a Web-based banking system for which subtle attacks have been reported recently.

Exploring alternative options is at the heart of the requirements and design processes. Different alternatives contribute to different degrees of achievement of non-functional goals about system safety, security, performance, usability, and so forth. Such goals in general cannot be satisfied in an absolute, clear-cut sense. Various qualitative and quantitative frameworks have been proposed to support the assessment of alternatives for design decision making. In general they lead to limited conclusions due to the lack of accuracy and measurability of goal formulations and the lack of impact propagation rules along goal contribution links.

This tutorial presents a comprehensive overview of state-of-the-art techniques for eliciting, modeling, specifying, analyzing and documenting high-quality system requirements.

Goal-oriented methods are increasingly popular for elaborating software requirements. They provide systematic support for incrementally building intentional, structural and operational models of the software and its environment together with various techniques for early analysis, e.g., to manage conflicting goals or anticipate abnormal environment behaviors that prevent goals from being achieved. On the other hand, tabular event-based methods are well-established for specifying operational requirements for control software. They provide sophisticated techniques and tools for late analysis of software behavior models through, e.g., simulation, model checking or table exhaustiveness checks. We propose to take the best out of these two worlds to engineer requirements for control software. It presents a technique for deriving event-based specifications, written in the SCR tabular language, from operational specifications built according to the KAOS goal-oriented method. The technique consists in a series of transformation steps each of which resolves semantic, structural or syntactic differences between the KAOS source language and the SCR target language. Some of these steps need human intervention and illustrate the kind of semantic subtleties that need to be taken into account when integrating multiple formalisms. As a result of our technique SCR specifiers may use upstream goal-based processes a la KAOS for the incremental elaboration, early analysis, organization and documentation of their tables while KAOS modelers may use downstream tables a la SCR for later analysis of the behavior models derived from goal specifications.

Developing high quality requirements specifications is a necessity for a number of critical industrial systems. An integrated toolset, called FAUST, is proposed to assist in the production of such specifications based on the KAOS goal-driven methodology. The tool suite is designed to naturally extend the existing semiformal modeling framework and to allow formalizing only the relevant critical parts. Two tools from the toolset are presented. The requirements checker performs KAOS goal-level checks using existing model checking technology. The requirements animator produces domain-level animations hiding formality even further.

Goal orientation is an increasingly recognized paradigm for eliciting, structuring, analyzing and documenting system requirements. Goals are statements of intent ranging from high-level, strategic concerns to low-level, technical requirements on the software-to-be and assumptions on its environment. Achieving goals require the cooperation of agents such as software components, input/output devices and human agents. The assignment of responsibilities for goals to agents is a critical decision in the requirements engineering process as alternative agent assignments define alternative system proposals.The paper describes a systematic technique to support the process of refining goals, identifying agents, and exploring alternative responsibility assignments. The underlying principles are to refine goals until they are assignable to single agents, and to assign a goal to an agent only if the agent can realize the goal.There are various reasons why a goal may not be realizable by an agent, e.g., the goal may refer to variables that are not monitorable or controllable by the agent. The notion of goal realizability is first defined on formal grounds; it provides a basis for identifying a complete taxonomy of realizability problems. From this taxonomy we systematically derive a catalog of tactics for refining goals and identifying agents so as to resolve realizability problems. Each tactics corresponds to the application of a formal refinement pattern that relieves the specifier from verifying the correctness of refinements in temporal logic.Our techniques have been used in two case studies of significant size; excerpts are shown to illustrate the main ideas.

Goal orientation is an increasingly recognized paradigm for eliciting, modeling, specifying and analyzing software requirements. Goals are statements of intent organized in AND/OR refinement structures; they range from high-level, strategic concerns to low-level, technical requirements on the software-to-be and assumptions on its environment. The operationalization of system goals into specifications of software services is a core aspect of the requirements elaboration process for which little systematic and constructive support is available. In particular, most formal methods assume such operational specifications to be given and focus on their a posteriori analysis.The paper considers a formal, constructive approach in which operational software specifications are built incrementally from higher-level goal formulations in a way that guarantees their correctness by construction. The operationalization process is based on formal derivation rules that map goal specifications to specifications of software operations; more specifically, these rules map real-time temporal logic specifications to sets of pre-, post- and trigger conditions. The rules define operationalization patterns that may be used for guiding and documenting the operationalization process while hiding all formal reasoning details; the patterns are formally proved correct once and for all. The catalog of operationalization patterns is structured according to a rich taxonomy of goal specification patterns.

Goals capture, at different levels of abstraction, the various objectives the system under consideration should achieve. Goal-oriented requirements engineering is concerned with the use of goals for eliciting, elaborating, structuring, specifying, analyzing, negotiating, documenting, and modifying requirements. This area has received increasing attention. The paper reviews various research efforts undertaken along this line of research. The arguments in favor of goal orientation are first briefly discussed. The paper then compares the main approaches to goal modeling, goal specification and goal-based reasoning in the many activities of the requirements engineering process. To make the discussion more concrete, a real case study is used to suggest what a goal-oriented requirements engineering method may look like. Experience, with such approaches and tool support are briefly discussed as well.

Requirements engineering (RE) is concerned with the identification of the goals to be achieved by the envisioned system, the operationalization of such goals into services and constraints, and the assignment of responsibilities for the resulting requirements to agents such as humans, devices, and software. The processes involved in RE include domain analysis, elicitation, specification, assessment, negotiation, documentation, and evolution. Getting high-quality requirements is difficult and critical. Recent surveys have confirmed the growing recognition of RE as an area of utmost importance in software engineering research and practice.

Requirements engineering is concerned with the elicitation of high-level goals to be achieved by the envisioned system, the refinement of such goals and their operationalization into specifications of services and constraints and the assignment of responsibilities for the resulting requirements to agents such as humans, devices and software. Requirements engineering processes often result in goals, requirements, and assumptions about agent behavior that are too ideal; some of them are likely not to be satisfied from time to time in the running system due to unexpected agent behavior. The lack of anticipation of exceptional behaviors results in unrealistic, unachievable, and/or incomplete requirements. As a consequence, the software developed from those requirements will not be robust enough and will inevitably result in poor performance or failures, sometimes with critical consequences on the environment. This paper presents formal techniques for reasoning about obstacles to the satisfaction of goals, requirements, and assumptions elaborated in the requirements engineering process. The techniques are based on a temporal logic formalization of goals and domain properties; they are integrated into an existing method for goal-oriented requirements elaboration with the aim of deriving more realistic, complete, and robust requirements specifications. A key principle is to handle exceptions at requirements engineering time and at the goal level, so that more freedom is left for resolving them in a satisfactory way. The various techniques proposed are illustrated and assessed in the context of a real safety-critical system.

Requirements engineering is concerned with the elicitation of high-level goals to be achieved by the system envisioned, the refinement of such goals and their operationalization into services and constraints, and the assignment of responsibilities for the resulting requirements to agents such as humans, devices and software. Requirements engineering processes may often result in requirements and assumptions about agent behaviour that are too ideal; some of them are likely to be violated from time to time in the running system due to unexpected agent behaviour. The lack of anticipation of exceptional behaviors results in unrealistic, unachievable and/or incomplete requirements. As a consequence, the software developed from those requirements will inevitably result in poor performance, sometimes with critical consequences on the environment. This paper proposes systematic techniques for reasoning about obstacles to the satisfaction of goals, requirements, and assumptions elaborated in the requirements engineering process. These techniques are integrated into an existing method for goal-driven requirements elaboration with the aim of deriving more complete and realistic requirements. The concept of obstacle is first defined precisely. Formal techniques and domain-independent heuristics are then proposed for identifying obstacles from goal/assumption formulations and domain properties. The paper then discusses techniques for resolving obstacles by transformation of the goals, requirements and assumptions elaborated so far in the process, or by introduction of new ones. Numerous examples are given throughout the paper to suggest how the techniques can be usefully applied in practice.

A wide range of inconsistencies can arise during requirements engineering as goals and requirements are elicited from multiple stakeholders. Resolving such inconsistencies sooner or later in the process is a necessary condition for successful development of the software implementing those requirements. The paper first reviews the main types of inconsistency that can arise during requirements elaboration, defining them in an integrated framework and exploring their interrelationships. It then concentrates on the specific case of conflicting formulations of goals and requirements among different stakeholder viewpoints or within a single viewpoint. A frequent, weaker form of conflict called divergence is introduced and studied in depth. Formal techniques and heuristics are proposed for detecting conflicts and divergences from specifications of goals/requirements and of domain properties. Various techniques are then discussed for resolving conflicts and divergences systematically by the introduction of new goals or by transforming the specifications of goals/objects toward conflict-free versions. Numerous examples are given throughout the paper to illustrate the practical relevance of the concepts and techniques presented. The latter are discussed in the framework of the KAOS methodology for goal-driven requirements engineering.

Scenarios are increasingly recognized as an effective means for eliciting, validating, and documenting software requirements. The paper focuses on the use of scenarios for requirements elicitation and explores the process of inferring formal specifications of goals and requirements from scenario descriptions. Scenarios are considered as typical examples of system usage; they are provided in terms of sequences of interaction steps between the intended software and its environment. Such scenarios are in general partial, procedural, and leave required properties about the intended system implicit. In the end such properties need to be stated in explicit, declarative terms for consistency/completeness analysis to be carried out. A formal method is proposed for supporting the process of inferring specifications of system goals and requirements inductively from interaction scenarios provided by stakeholders. The method is based on a learning algorithm that takes scenarios as examples/counterexamples and generates a set of goal specifications in temporal logic that covers all positive scenarios while excluding all negative ones. The output language in which goals and requirements are specified is the KAOS goal based specification language. The paper also discusses how the scenario based inference of goal specifications is integrated in the KAOS methodology for goal based requirements engineering. In particular, the benefits of inferring declarative specifications of goals from operational scenarios are demonstrated by examples of formal analysis at the goal level, including conflict analysis, obstacle analysis, the inference of higher level goals, and the derivation of alternative scenarios that better achieve the underlying goals.

No abstract available.

The KAOS methodology provides a language, a method, and meta-level knowledge for goal-driven requirements elaboration. The language provides a rich ontology for capturing requirements in terms of goals, constraints, objects, actions, agents etc. Links between requirements are represented its well to capture refinements, conflicts, operationalizations, responsibility assignments, etc. The KAOS specification language is a multi-paradigm language with a two-level structure: an outer semantic net layer for declaring concepts, their attributes and links to other concepts, and an inner formal assertion layer for formally defining the concept. The latter combines a real-time temporal logic for the specification of goals, constraints, and objects, and standard pre-/postconditions for the specification of actions and their strengthening to ensure the constraints.

Reusing similar requirements fragments is one of the most promising ways to reduce the elaboration time and increase the requirements' quality. This paper investigates the application of analogical reasoning techniques to complete partial requirement specifications. A case base is assumed to be available; it contains requirements frameworks involving goals, constraints, objects, actions and agents from systems which have already been specified. We show how a rich requirements meta-model, coupled with an expressive formal assertion language, may increase the effectiveness of analogical reuse. An acquisition problem is first specified by a requirements engineer as a query formulated in the vocabulary of the specification fragments built so far. Source cases and partial mappings are found by query generalization followed by a search through the case base. Once analogies have been confirmed, mappings are completed by the use of relevance rules that distinguish, in the formal assertions, what is relevant to the analogy from what is irrelevant. The best analogies are then selected and extended in such a way that the logical properties of the answers to the query may be verified, thus increasing confidence in the analogy. The approach is illustrated by analogical acquisition of specifications of a meeting scheduler in the KAOS goal-oriented specification language.

Requirements engineering is concerned with the identification of high-level goals to be achieved by the system envisioned, the refinement of such goals, the operationalization of goals into services and constraints, and the assignment of responsibilities for the resulting requirements to agents such as humans, devices and programs. Goal refinement and operationalization is a complex process which is not well supported by current requirements engineering technology. Ideally some form of formal support should be provided, but formal methods are difficult and costly to apply at this stage.This paper presents an approach to goal refinement and operationalization which is aimed at providing constructive formal support while hiding the underlying mathematics. The principle is to reuse generic refinement patterns from a library structured according to strengthening/weakening relationships among patterns. The patterns are once for all proved correct and complete. They can be used for guiding the refinement process or for pointing out missing elements in a refinement. The cost inherent to the use of a formal method is thus reduced significantly. Tactics are proposed to the requirements engineer for grounding pattern selection on semantic criteria.The approach is discussed in the context of the multi-paradigm language used in the KAOS method; this language has an external semantic net layer for capturing goals, constraints, agents, objects and actions together with their links, and an inner formal assertion layer that includes a real-time temporal logic for the specification of goals and constraints. Some frequent refinement patterns are high-lighted and illustrated through a variety of examples.The general principle is somewhat similar in spirit to the increasingly popular idea of design patterns, although it is grounded on a formal framework here.

Recently a number of requirements engineering languages and methods have flourished that not only address 'what' questions but also 'why', 'who' and 'when' questions. The objective of the paper is twofold: to assess the strengths and weaknesses of one of these methodologies on a nontrivial benchmark; and to illustrate and discuss a number of challenging issues that need to be addressed for such methodologies to become effective in supporting real, complex requirements engineering tasks. The problem considered here is that of a distributed meeting scheduler system; the methodology considered is the KAOS goal directed language and method. The issues raised from this case study include goal identification, the "deidelization" of unachievable goals, the handling of interfering goals, the impact of early formal reasoning, the merits of early reuse of abstract descriptions and categories, requirements traceability and the need to link requirements to retractable assumptions, and the potential benefits of hybrid acquisition strategies.

ALMA is an environment kernel supporting the elaboration, analysis, documentation, and maintenance of the various products developed during an entire software lifecycle. Its central component is an environment database in which properties about software objects and relations are collected. Two kinds of tools are provided: high-level tools and syntax-directed tools. A basic feature of the ALMA kernel is its genericity. Tools of the first kind are parameterized on software lifecycle models while tools of the second kind are parameterized on formalisms. Versions of specific models and formalisms are generated by a meta-environment, which also generates the environment database structure tailored to the desired lifecycle model. The database support meta-system and the instatiated database support systems it generates are emphasized, including the architectural design decisions made and the mechanisms introduced for achieving parameterization on lifecycle models.>