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.

Models play a crucial role in the development and maintenance of software systems, but are often neglected during the development process due to the considerable manual effort required to produce them. In response to this problem, numerous techniques have been developed that seek to automate the model generation task with the aid of increasingly accurate algorithms from the domain of Machine Learning. From an empirical perspective, these are extremely challenging to compare; there are many factors that are difficult to control (e.g. the richness of the input and the complexity of subject systems), and numerous practical issues that are just as troublesome (e.g. tool availability). This paper describes the StaMinA ( Sta te M achine In ference A pproaches) competiton, that was designed to address these problems. The competition attracted numerous submissions, many of which were improved or adapted versions of techniques that had not been subjected to extensive empirical evaluations, and had not been evaluated with respect to their ability to infer models of software systems. This paper shows how many of these techniques substantially improve on the state of the art, providing insights into some of the factors that could underpin the success of the best techniques. In a more general sense it demonstrates the potential for competitions to act as a useful basis for empirical software engineering by (a) spurring the development of new techniques and (b) facilitating their comparative evaluation to an extent that would usually be prohibitively challenging without the active participation of the developers.

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.

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.

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.