Skip to main content
main-content

Über dieses Buch

This book is dedicated to Professor Martin Wirsing on the occasion of his emeritation from Ludwig-Maximilians-Universität in Munich, Germany. The volume is a reflection, with gratitude and admiration, on Professor Wirsing’s life highly creative, remarkably fruitful and intellectually generous life. It also gives a snapshot of the research ideas that in many cases have been deeply influenced by Professor Wirsing’s work.

The book consists of six sections. The first section contains personal remembrances and expressions of gratitude from friends of Professor Wirsing. The remaining five sections consist of groups of scientific papers written by colleagues and collaborators of Professor Wirsing, which have been grouped and ordered according to his scientific evolution. More specifically, the papers are concerned with logical and algebraic foundations; algebraic specifications, institutions and rewriting; foundations of software engineering; service oriented systems; and adaptive and autonomic systems.

Inhaltsverzeichnis

Frontmatter

A Homage to Martin Wirsing

Martin Wirsing was born on Christmas Eve, December 24th, 1948, in Bayreuth, a Bavarian town which is famous for the annually celebrated Richard Wagner Festival. There he visited the Lerchenbühl School and the High-School “Christian Ernestinum” where he followed the humanistic branch focusing on Latin and Ancient Greek. After that, from 1968 to 1974, Martin studied Mathematics at University Paris 7 and at Ludwig-Maximilians-Universität in Munich. In 1971 he became Maitrise-en-Sciences Mathematiques at the University Paris 7 and, in 1974, he got the Diploma in Mathematics at LMU Munich.

Rocco De Nicola, Rolf Hennicker

Homage from Friends

Ode to the PST

1992! Internet in Germany was in its infancy, object oriented programming wasn’t well-known yet, and even the European Union, which has funded so many of our research efforts lately, had not been formed.

Computing was certainly not mainstream when Martin Wirsing took the post of full professor at the Ludwig-Maximilians-Universität München in that year. The chair for Programming & Software Engineering (

Lehrstuhl für Programmierung und Softwaretechnik, PST

) was created along with his appointment. Indeed, the first

Diplom

course of studies in Computer Science (

Informatik

) at LMU had been created only the year before. The institute was still situated in the Leopoldstraße in Schwabing, only moving to the

Institute am Englischen Garten

in the Oettingenstraße in 1996 (Figure 1) — a beautiful location set right in the English Garden in Munich, five minutes away from one of the main tourist spots, the

Biergarten am Chinesischen Turm

. And with a history — the building was the site of the former

Radio Free Europe

[28], a radio station funded by the U.S. Government with its own history (including a bomb attack in 1981 on the very building where PST is now located).

Matthias Hölzl, Nora Koch, Philip Mayer, Andreas Schroeder, Lenz Belzner, Marianne Busch, Anton Fasching, Annabelle Klarl, Christian Kroiss, Laith Raed

From Formal Logic through Program Transformations to System Dynamics: 40 Years of Meeting Points with Martin Wirsing

My first meeting with Martin Wirsing is of rather virtual nature: We both have the same academic background and got our diplomas from the same institution, the Institute of Mathematical Logic of LMU Munich directed by Kurt Sch”utte. But we did not (yet) meet personally: While I worked on my diploma thesis on

μ

-recursive functions and the non-eliminability of some ugly functionals in intricate number theory, Martin entered the institute as a student and left it some years later having completed two theses (diploma and Ph.D.) on similarly mystical problems such as (un-)decidability of (sub-)classes of formulae in first-order predicate logic.

Wolfgang Hesse

The Broad View: How To Spawn a Radical Organizational Transformation ‘En Passant’

This short paper is a rather personal account on the process, which in the end led to the effect that the author moved from a scholar of an influential person to a colleague of him. It tries to tell the story how a new organizational backbone for the Institute of Informatics at LMU was created by predictive thinking, and it is a hommage to the ability to switch from technical detail to a very broad but nevertheless precise analysis of development opportunities for an organization.

Heinrich Hussmann

Logical and Algebraic Foundations

Modal Satisfiability via SMT Solving

Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions.

Carlos Areces, Pascal Fontaine, Stephan Merz

Division by Zero in Common Meadows

Common meadows are fields expanded with a total multiplicative inverse function. Division by zero produces an additional value denoted with “

${\textup{\textbf{a}}}$

” that propagates through all operations of the meadow signature (this additional value can be interpreted as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that admit a certain cancellation law.

Jan A. Bergstra, Alban Ponse

Logical Relations and Nondeterminism

The purpose of this article is to illustrate some technical difficulties encountered when trying to extend a logical relation to the Hoare powerdomain. We give a partial solution and some applications. Our vehicle is a simple call-by-value programming language with binary nondeterministic choice. We define both a big-step operational semantics and a denotational semantics using the Hoare powerdomain. Using our logical relation we then show equivalence of the two semantics in the sense of computational adequacy and some type-dependent program equivalences.

Martin Hofmann

Simplified Coalgebraic Trace Equivalence

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. labelled transition systems. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard and probabilistic labelled transition systems.

Alexander Kurz, Stefan Milius, Dirk Pattinson, Lutz Schröder

Localized Operational Termination in General Logics

Termination can be thought of as the property of programs ensuring that every input is given an answer in finite time. There are, however, many different (combinations of) programming paradigms and languages for these paradigms. Is a common

formal

definition of termination of programs in any (or most) of these programming languages possible? The notion of

operational termination

provides a general definition of termination which relies on the logic-based description of (the operational semantics of) a

programming language

. The key point is capturing termination as the

absence of infinite inference

, that is:

all

proof attempts must either successfully terminate, or they must fail in finite time. This

global notion

is well-suited for most

declarative

languages, where programs are

theories

in a logic whose inference system is

specialized

to each theory to characterize its computations. Other programming languages (e.g., imperative languages) and applications (e.g., the evaluation of specific expressions and goals in functional and logic programs) require a more specialized treatment which pays attention not just to theories, but to specific

formulas

to be proved within the given theory. For instance, the execution of an imperative program can be viewed as a proof of an specific

formula

(representing the program) within the computational logic describing the operational semantics of the programming language. In such cases, an appropriate definition of termination should focus on proving the absence of infinite proofs for computations

localized

to

specific goals

. In this paper we generalize the global notion of operational termination to this new setting and adapt the recently introduced OT-framework for mechanizing proofs of operational termination to support proofs of

localized

operational termination.

Salvador Lucas, José Meseguer

Partial Valuation Structures for Qualitative Soft Constraints

Soft constraints have proved to be a versatile tool for the specification and implementation of decision making in adaptive systems. A plethora of formalisms have been devised to capture different notions of preference. Wirsing et al. have proposed partial valuation structures as a unifying algebraic structure for several soft constraint formalisms, including quantitative and qualitative ones, which, in particular, supports lexicographic products in a broad range of cases. We demonstrate the versatility of partial valuation structures by integrating the qualitative formalism of constraint relationships as well as the hybrid concept of constraint hierarchies. The latter inherently relies on lexicographic combinations, but it turns out that not all can be covered directly by partial valuation structures. We therefore investigate a notion for simulating partial valuation structures not amenable to lexicographic combinations by better suited ones. The concepts are illustrated by a case study in decentralized energy management.

Alexander Schiendorfer, Alexander Knapp, Jan-Philipp Steghöfer, Gerrit Anders, Florian Siefert, Wolfgang Reif

Algebraic Specifications, Institutions, and Rewriting

An Institution for Object-Z with Inheritance and Polymorphism

Large software systems are best specified using a multi-paradigm approach. Depending on which aspects of a system one wants to model, some logic formalisms are better suited than others. The theory of institutions and (co)morphisms between institutions provides a general framework for describing logical systems and their connections. This is the foundation of multi-modelling languages allowing one to deal with heterogeneous specifications in a consistent way. To make Object-Z accessible as part of such a multi-modelling language, we define the institution OZS for Object-Z. We have chosen Object-Z in part because it is a prominent software modelling language and in part because it allows us to study the formalisation of object-oriented concepts, like object identity, object state, dynamic behaviour, polymorphic sorts and inheritance.

Hubert Baumeister, Mohamed Bettaz, Mourad Maouche, M’hamed Mosteghanemi

Abstract Constraint Data Types

Martin Wirsing is one of the earliest contributors to the area of Algebraic Specification (e.g., [2]), which he explored in a variety of domains over many years. Throughout his career, he has also inspired countless researchers in related areas. This paper is inspired by one of the domains that he explored thirty years or so after his first contributions when leading the FET Integrated Project SENSORIA [14]: the use of constraint systems to deal with non-functional requirements and preferences [13,8]. Following in his footsteps, we provide an extension of the traditional notion of algebraic data type specification to encompass soft-constraints as formalised in [1]. Finally, we relate this extension with institutions [6] and recent work on graded consequence in institutions [3].

José Luiz Fiadeiro, Fernando Orejas

Generate & Check Method for Verifying Transition Systems in CafeOBJ 

An interactive theorem proving method for the verification of infinite state transition systems is described.

The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a topmost sort

State

, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an invariant (i.e. a state predicate that is valid for all reachable states) or (2) a (

p leads-to q

) property for two state predicates

p

and

q

, where (

p leads-to q

) means that from any reachable state

s

with (

p(s)

=

true

) the system will get into a state

t

with (

q(t)

=

true

) no matter what transition sequence is taken.

Verification is achieved by developing proof scores in

CafeOBJ

. Sufficient verification conditions are formalized for verifying invariants and (

p leads-to q

) properties. For each verification condition, a proof score is constructed to (1) generate a finite set of state patterns that covers all possible infinite states and (2) check validity of the verification condition for all the covering state patterns by reductions.

The method achieves significant automation of proof score developments.

Kokichi Futatsugi

Institutions for OCL-Like Expression Languages

In 2008, Martin Wirsing initiated the project of conceiving the “Unified Modeling Language” (UML) as a heterogeneous modelling language. He proposed to use the theory of heterogeneous institutions for providing individual semantics to each sub-language, that can then be integrated using institution (co-)morphisms. In particular, the proposal allows for seamlessly capturing the notorious semantic variation points of UML with mathematical rigour. In this line of research, we contribute an institutional framework for the “Object Constraint Language” (OCL), UML’s language for expressing constraints.

Alexander Knapp, María Victoria Cengarle

Towards an Institutional Framework for Heterogeneous Formal Development in UML

— A Position Paper —

We present a framework for formal software development with UML. In contrast to previous approaches to equipping UML with a formal semantics, we propose an institution-based heterogeneous approach. This can express suitable formal semantics of the different UML diagram types directly, without the need to map everything to one specific formalism (let it be first-order logic or graph grammars). We provide ideas how different aspects of the formal development process can be coherently formalised, ranging from requirements over design and Hoare-style conditions on code to the implementation itself. The framework can be used to verify consistency of different UML diagrams both horizontally (e.g., consistency among various requirements) as well as vertically (e.g., correctness of design or implementation w.r.t. the requirements).

Alexander Knapp, Till Mossakowski, Markus Roggenbach

Formal Analysis of Leader Election in MANETs Using Real-Time Maude

The modeling and analysis of mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ways that are hard to model and analyze by automatic formal methods. In this work we use rewriting logic and Real-Time Maude to address this challenge. We propose a composable formal framework for MANET protocols and their mobility models that can take into account such complex interactions. We illustrate our framework by analyzing a well-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.

Si Liu, Peter Csaba Ölveczky, José Meseguer

The Foundational Legacy of ASL

We recall the kernel algebraic specification language ASL and outline its main features in the context of the state of research on algebraic specification at the time it was conceived in the early 1980s. We discuss the most significant new ideas in ASL and the influence they had on subsequent developments in the field and on our own work in particular.

Donald Sannella, Andrzej Tarlecki

Soft Agents: Exploring Soft Constraints to Model Robust Adaptive Distributed Cyber-Physical Agent Systems

We are interested in principles for designing and building open distributed systems consisting of multiple cyber-physical agents, specifically, where a coherent global view is unattainable and timely consensus is impossible. Such agents attempt to contribute to a system goal by making local decisions to sense and effect their environment based on local information. In this paper we propose a model, formalized in the Maude rewriting logic system, that allows experimenting with and reasoning about designs of such systems. Features of the model include communication via sharing of partially ordered knowledge, making explicit the physical state as well as the cyber perception of this state, and the use of a notion of soft constraints developed by Martin Wirsing and his team to specify agent behavior. The paper begins with a discussion of desiderata for such models and concludes with a small case study to illustrate the use of the modeling framework.

Carolyn Talcott, Farhad Arbab, Maneesh Yadav

Foundations of Software Engineering

Structured Document Algebra in Action

A

Structured Document Algebra (SDA)

defines modules with variation points and how such modules compose. The basic operations are module addition and replacement. Repeated addition can create nested module structures. SDA also allows the decomposition of modules into smaller parts. In this paper we show how SDA modules can be used to deal algebraically with

Software Product Lines (SPLs)

. In particular, we treat some fundamental concepts of SPLs, such as refinement and refactoring. This leads to mathematically precise formalization of fundamental concepts used in SPLs, which can be used for improved

Feature-Oriented Software Development

(FOSD) tooling.

Don Batory, Peter Höfner, Dominik Köppl, Bernhard Möller, Andreas Zelend

From EU Projects to a Family of Model Checkers

From Kandinsky to KandISTI

We describe the development of the KandISTI family of model checkers from its origins nearly two decades ago until its very recent latest addition. Most progress was made, however, during two integrated European projects, AGILE and SENSORIA, in which our FM&&T lab participated under the scientific coordination of Martin Wirsing. Moreover, the very name of the family of model checkers is partly due to Martin Wirsing’s passion for art and science.

Maurice H. ter Beek, Stefania Gnesi, Franco Mazzanti

Pragmatic Formal Specification of System Properties by Tables

We suggest tables as pragmatic tractable specification formalism for a precise as well as readable specification of systems, their interfaces, as well as their functional properties. Translating tables into logical formulae defines a precise semantics for them. Writing logical formulae in a structured way by tables makes them better usable for engineering purposes. Tables are considered better structured, easier to read, to comprehend, to analyze, or at least easier to communicate than large logical formulae. On the other hand logical formulae are better suited to derive properties by deduction steps applying logical calculi. By translating tables into formulae of predicate logic and vice versa, we provide a bridge between the conciseness of readable suggestive specifications and the preciseness of mathematical methods in software and systems engineering.

Manfred Broy

Formal Modelling for Cooking Assistance

Structured ontologies, with various facets of abstraction, are used to model food, ingredients, recipes, cookware and workflows. They form the uniform knowledge base for modular software assistants. Processes and monitors supervise the cooking process and advise the user.

Bernd Krieg-Brückner, Serge Autexier, Martin Rink, Sidoine Ghomsi Nokam

A Framework for Defining and Comparing Modelling Methods

There are a huge number of scientific papers and reports intended for practitioners, not forgetting whole books and websites, presenting modelling methods in the field of software development. Thus, many questions naturally arise concerning both the nature of method itself (say, e.g. its scope and intended use) and the relationships between different methods, to compare them and choosing the most appropriate for a specific application. Here we present a preliminary attempt at proposing a “modelling method framework” suitable for presenting the constituents, both technical and methodological, of a method in an organized and possibly precise way. The purpose of our framework is to provide a setting for answering the above mentioned questions in a systematic and well-founded way. We will illustrate our proposed framework using some existing methods for modelling service-based systems.

At the end of the paper we offer a short tribute to a long standing friendship with Martin.

Gianna Reggio, Egidio Astesiano, Christine Choppy

A Theory Agenda for Component-Based Design

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a semantically sound theoretical and general framework for modelling component-based systems and their properties both behavioural and architectural as well for achieving correctness by using scalable specific techniques.

We discuss the problem of composing components by proposing the concept of glue as a set of stateless composition operators defined by a certain type of operational semantics rules. We provide an overview of results about glue expressiveness and minimality. We show how interactions and associated transfer of data can be described by using connectors and in particular, how dynamic connectors can be defined as an extension of static connectors. We present two approaches for achieving correctness for component-based systems. One is by compositional inference of global properties of a composite component from properties of its constituents and interaction constraints implied by composition operators. The other is by using and composing architectures that enforce specific coordination properties. Finally, we discuss recent results on architecture specification by studying two types of logics: 1) interaction logics for the specification of sets of allowed interactions; 2) configuration logics for the characterisation of architecture styles.

Joseph Sifakis, Saddek Bensalem, Simon Bliudze, Marius Bozga

Effective and Efficient Model Clone Detection

Code clones are a major source of software defects. Thus, it is likely that model clones (i.e., duplicate fragments of models) have a significant negative impact on model quality, and thus, on any software created based on those models, irrespective of whether the software is generated fully automatically (“MDD-style”) or hand-crafted following the blueprint defined by the model (“MBSD-style”). Unfortunately, however, model clones are much less well studied than code clones. In this paper, we present a clone detection algorithm for UML domain models. Our approach covers a much greater variety of model types than existing approaches while providing high clone detection rates at high speed.

Harald Störrle

Living Modeling of IT Architectures: Challenges and Solutions

Enterprise Architecture Models (EA Models) are documentations capturing the elements of an enterprise’s IT infrastructure, setting these elements in relation to each other and setting them into the context of the business. EA Models are a crucial backbone for any IT management process and activities like analysing IT related risks and planning investments. The more companies depend on reliable IT services and use IT as innovation driver, the more high quality EA Models provide competitive advantage. In this paper we describe core challenges to the maintenance of EA Models based on previously conducted surveys and our longstanding experience in industrial collaborations. This is followed by a sketch of an innovative solution to solve these challenges.

Thomas Trojer, Matthias Farwick, Martin Häusler, Ruth Breu

Service-Oriented Systems

A Flow Analysis Approach for Service-Oriented Architectures

The discipline of SOA (Service-oriented Architecture) provides concepts for designing the structural and behavioral aspects of application landscapes that rely on the interaction of self-contained services. To assess an architecture’s quality and validate its conformance to behavioral requirements, those models must be subjected to sophisticated static analyses. We propose a comprehensive methodology that relies on data flow analysis for a context-sensitive evaluation of service-oriented system designs. The approach employs a model-based format for SOA artifacts which acts as a uniform basis for the specification and execution of various analyses. Using this methodology, we implement two analyses which reveal blocking calls and assess performance metrics. These applications are evaluated in the context of two case studies that have been developed in the SENSORIA and the ENVIROFI projects.

Bernhard Bauer, Melanie Langermeier, Christian Saad

Service Composition for Collective Adaptive Systems

Collective adaptive systems are large-scale resource-sharing systems which adapt to the demands of their users by redistributing resources to balance load or provide alternative services where the current provision is perceived to be insufficient. Smart transport systems are a primary example where real-time location tracking systems record the location availability of assets such as cycles for hire, or fleet vehicles such as buses, trains and trams. We consider the problem of an informed user optimising his journey using a composition of services offered by different service providers.

Stephen Gilmore, Jane Hillston, Mirco Tribastone

The Evolution of Jolie

From Orchestrations to Adaptable Choreographies

Jolie is an orchestration language conceived during

Sensoria

, an FP7 European project led by Martin Wirsing in the time frame 2005–2010. Jolie was designed having in mind both the novel –at project time– concepts related to Service-Oriented Computing and the traditional approach to the modelling of concurrency typical of process calculi. The foundational work done around Jolie during

Sensoria

has subsequently produced many concrete results. In this paper we focus on two distinct advancements, one aiming at the development of dynamically adaptable orchestrated systems and one focusing on global choreographic specifications. These works, more recently, contributed to the realisation of a framework for programming dynamically evolvable distributed Service-Oriented applications that are correct-by-construction.

Ivan Lanese, Fabrizio Montesi, Gianluigi Zavattaro

Stochastic Model Checking of the Stochastic Quality Calculus

The Quality Calculus uses quality binders for input to express strategies for continuing the computation even when the desired input has not been received. The Stochastic Quality Calculus adds generally distributed delays for output actions and real-time constraints on the quality binders for input. This gives rise to Generalised Semi-Markov Decision Processes for which few analytical techniques are available.

We restrict delays on output actions to be exponentially distributed while still admitting real-time constraints on the quality binders. This facilitates developing analytical techniques based on stochastic model checking and we compute closed form solutions for a number of interesting scenarios. The analyses are applied to the design of an intelligent smart electrical meter of the kind to be installed in European households by 2020.

Flemming Nielson, Hanne Riis Nielson, Kebin Zeng

Adaptive and Autonomic Systems

Software-Intensive Systems for Smart Cities: From Ensembles to Superorganisms

Smart cities infrastructures can be considered as large-scale, software-intensive systems exhibiting close sinergies among ICT devices and humans. However, current deployments of smart city technologies rely on rather traditional technologies. This chapter introduces a novel perspective in which large-scale ensembles of software components, ICT devices, and humans, can be made working together in an orchestrated and self-organized way to achieve urban-level goals as if they were part of a single large-scale organism, i.e., a superorganism. Accordingly, we delineate our vision of urban superorganisms and overview related application areas. Finally, we identify the key challenges in engineering self-organizing systems that can work as a superorganism, and we introduce the reference architecture for an infrastructure capable of supporting our vision.

Nicola Bicocchi, Letizia Leonardi, Franco Zambonelii

A White Box Perspective on Behavioural Adaptation

We present a white-box conceptual framework for adaptation developed in the context of the EU Project ASCENS coordinated by Martin Wirsing. We called it CoDa, for Control Data Adaptation, since it is based on the notion of

control data

. CoDa promotes a neat separation between application and adaptation logic through a clear identification of the set of data that is relevant for the latter. The framework provides an original perspective from which we survey a representative set of approaches to adaptation, ranging from programming languages and paradigms to computational models and architectural solutions.

Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin

Rule-Based Modeling and Static Analysis of Self-adaptive Systems by Graph Transformation

Software systems nowadays require continuous operation despite changes both in user needs and in their operational environments. Self-adaptive systems are typically instrumented with tools to autonomously perform adaptation to these changes while maintaining some desired properties. In this paper we model and analyze self-adaptive systems by means of typed, attributed graph grammars. The interplay of different grammars representing the application and the adaptation logic is realized by an adaption manager. Within this formal framework we define consistency and operational properties that are maintained despite adaptations and we give static conditions for their verification. The overall approach is supported by the AGG tool for modeling, simulating, and analyzing graph transformation systems. A case study modeling a business process that adapts to changing environment conditions is used to demonstrate and validate the formal framework.

Antonio Bucchiarone, Hartmut Ehrig, Claudia Ermel, Patrizio Pelliccione, Olga Runge

Formalization of Invariant Patterns for the Invariant Refinement Method

Refining high-level system invariants into lower-level software obligations has been successfully employed in the design of ensemble-based systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathematical analysis. This paper provides such a formalization and demonstrates it in the context of the Invariant Refinement Method. The formalization is used to formally define invariant patterns at different levels of abstraction and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns.

Tomáš Bureš, Ilias Gerostathopoulos, Jaroslav Keznikl, František Plášil, Petr Tůma

On StocS: A Stochastic Extension of SCEL

Predicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension allows for quantitative modelling and analysis of system behaviour (e.g. performance) but rises a number of non-trivial design and formal semantics issues with different options as possible solutions at different levels of abstraction.

Diego Latella, Michele Loreti, Mieke Massink, Valerio Senni

Programming Autonomic Systems with Multiple Constraint Stores

Developing autonomic systems is a major challenge due to their distributed nature, large dimension, high dynamism, open-endedness, and need of adaptation. In this paper, we tackle this challenge by proposing a language, called

cc

SCEL, that combines abstractions and primitives specifically devised for programming autonomic systems by also using constraints and operations on them. We show that constraints permit addressing issues related to the programming of autonomic systems, since they are suitable means to deal with, e.g., partial knowledge, multi-criteria optimisation, preferences, uncertainty. We also present an advanced form of interaction that is particularly convenient in this setting. It allows a component of a system to access the constraint-based knowledge of all components checking its consistency and implications.

Ugo Montanari, Rosario Pugliese, Francesco Tiezzi

Adaptive and Autonomous Systems and Their Impact on Us

With technology becoming increasingly ubiquitous and through a wide use of interconnected “smart devices”, the impacts these advanced products have on us is gaining in significance. As technology providers, we are very proud to share the tribute for creating new infrastructures that bring benefits to individuals and society and make life easier. But we may also be held responsible for the possible detrimental impacts that new technology brought about. Especially, if we ignore the threatening consequences and fail to offer some protective solutions. Up to now, there has been some attention paid to privacy issues and security of commercial transactions, but the negative influence of “smart” technology on human behavior has been widely neglected. This paper considers the effects that adaptive and autonomous technologies have on their users. As the impacts can best be observed in practice, a number of application scenarios are taken into account, illustrating both the technical aspects and their possible effects on us.

Nikola Šerbedžija

The KnowLang Approach to Self-adaptation

Self-adaptive systems autonomously monitor their behavior and eventually modify that behavior according to changes in the operational environment or in the system itself. In this entry, we present an approach to implementing self-adaptation capabilities with KnowLang, a special framework for knowledge representation and reasoning. KnowLang provides for a special knowledge context and a special reasoner operating in that context. The approach is formal and demonstrates how knowledge representation and reasoning help to establish the vital connection between knowledge, perception, and actions that realize self-adaptive behavior. Knowledge is used against the perception of the world to generate appropriate actions in compliance with some set of goals and beliefs.

Emil Vassev, Mike Hinchey

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise