From scenarios to components

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)

691 Downloads (Pure)

Abstract

Scenario-based modeling has evolved as an accepted paradigm for developing complex systems of various kinds. Its main purpose is to ensure that a system provides desired behavior to its users. A scenario is generally understood as a behavioral requirement, denoting a course of actions that shall occur in the system. A typical notation of a scenario is a Message Sequence Chart or, more general, a finite partial order of actions. A specification is a set of scenarios. Intuitively, a system implements a specification if all scenarios of the specification can occur in the system. The main challenge in this approach is to systematically synthesize from a given scenario-based specification state-based components which together implement the specification; preferably to be achieved automatically. A further challenge is to analyze scenarios to avoid erroneous specifications. Existing scenario-based techniques exhibit a conceptual and formal gap between a scenariobased specification on the one hand and a state-based implementation on the other hand. This gap often renders synthesis surprisingly complex, and obscures the relationship between a specification and its implementation. Additionally, existing techniques for analyzing implementations cannot immediately be re-used for analyzing specifications, and vice versa. In this thesis, we introduce a semantic model for scenarios that seamlessly integrates scenario-based specifications and state-based implementations. We focus on modeling and analyzing the control-flow of systems. Technically, we use Petri nets together with the well established notion of distributed runs for (a) describing the semantics of scenarios, for (b) systematically constructing and analyzing a specification, and for (c) synthesizing an implementation from a given specification. Our first contribution is to identify a minimal set of notions to specify the behavior of distributed systems with scenarios. We formalize these notions in a novel semantic model for scenarios, called oclets. Oclets combine formal notions from Petri net theory with formal notions from scenario-based techniques in a unified way. We define a classical declarative semantics for scenario-based specifications which defines when a given set of runs satisfies a given specification. These semantics are compositional : a set of runs satisfies a composition of two specifications iff it satisfies each of the specifications. We then provide composition and decomposition operators on oclets and relations for comparing oclets. Using these notions, we systematically derive for each scenario-based specification S the behavior exhibited by a minimal implementation of S. The second contribution of this thesis aims at closing the conceptual and methodological gap between scenario-based specifications and state-based system models. In our approach, the semantics of scenarios and the semantics of systems both employ the same notions from Petri nets. We provide operational semantics for scenario-based specifications. On the basis of these operational semantics, we consider the problems of analyzing behavioral properties of specifications and of synthesizing components that implement the specification. We show that these problems are undecidable in general and we present a sufficient property for the decidable case. We then present algorithms for analysis and synthesis. We derive these results by generalizing existing techniques from Petri nets to the domain of scenario-based specifications. We implemented our algorithms for simulating, analyzing, and synthesizing from scenariobased specifications in our tool Greta. We report on an industrial case study that shows the feasibility of our techniques.
Original languageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • Mathematics and Computer Science
Supervisors/Advisors
  • van der Aalst, Wil, Promotor
  • Reisig, Wolfgang, Promotor, External person
  • Wolf, K., Copromotor, External person
Award date27 Sept 2010
Place of PublicationEindhoven
Publisher
Print ISBNs978-90-386-2319-1
DOIs
Publication statusPublished - 2010

Fingerprint

Dive into the research topics of 'From scenarios to components'. Together they form a unique fingerprint.

Cite this