Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Checking Unsatisfiability for OCL Constraints
Get PDFIn this paper we propose a mapping from a subset of
OCL into first-order logic (FOL) and use this mapping for checking the
unsatisfiability of sets of OCL constraints. Although still
preliminary work, we argue in this paper that our mapping is both
simple, since the resulting FOL sentences closely mirror the
original OCL constraints, and practical, since we can use
automated reasoning tools, such as automated theorem provers and SMT
solvers to automatically check the unsatisfiability of
non-trivial sets of OCL constraints
Modelling Feedback Control Loops for Self-Adaptive Systems
Get PDFFeedback Control Loops (FCLs) are the heart of any self-adaptive sys- tem. Existing engineering approaches for building self-adaptive systems mask FCL by providing abstraction layers that hide the application complexity. In this paper, we investigate a model-driven approach for the engineering of FCLs whose archi- tecture is based on the Service Component Architecture (SCA) model. Our proposal consists in exploiting the data streaming model, to specify the characteristics of the control policies, and to generate FCLs of self-adaptive systems deployed in large- scale environment. We argue that the use of a data-oriented model for designing self-adaptive systems significantly increases FCL visibility
Modeling a Service and Session Calculus with Hierarchical Graph Transformation
Get PDFGraph transformation techniques have been applied successfully to the
modelling of process calculi, for example for equipping them with a
truly concurrent semantics. Recently, there has been an increasing
interest towards hierarchical structures both at the level of
graph-based models, in order to represent explicitly the interplay
between linking and containment (like in Milner's bigraphs), and at
the level of process calculi, in order to deal with several logical
notions of scoping (ambients, sessions and transactions, among
others). In this paper we show how to encode a sophisticated calculus
of services and nested sessions by exploiting a suitable flavour of
hierarchical graphs. For the encoding of the processes of this
calculus we benefit from a recently proposed algebra of graphs with
nesting
Massively Multiuser Virtual Environments using Object Based Sharing
Get PDFMassively multiuser virtual environments (MMVEs) are becoming increasingly
popular with millions of users. Commercial implementations typically
rely on a traditional client/server architecture controlling the virtual world state of
shared data at a central point. Message passing mechanisms are used to communicate
state changes to the clients. For scalability reasons our approach creates and
deploys MMVEs in a peer-to-peer (P2P) fashion. We use standard Java technology
implementing only a few basic data-centric operations for the management of our
distributed objects. Higher consistency models can easily be implemented using
these basic operations. Currently, we have implemented transactional consistency
offering convenient and consistent access to the shared scene graph. In this paper
we describe our basic object model and the prototype implementation TGOS (Typed
Grid Object Sharing). Furthermore, we discuss preliminary measurements with the
virtual world Wissenheim executed on top of TGOS
Improved Flexibility and Scalability by Interpreting Story Diagrams
Get PDFIn this paper, we present an interpreter for Story Diagrams working on Eclipse Modeling Framework (EMF) models. The interpreter provides a more flexible and, under certain circumstances, a more scalable solution than the compiled Java code generated from Story Diagrams by Fujaba. of Dynamic EMF even allows the evolution of meta models at runtime. Story Diagrams can now be modeled and executed within Eclipse. They can be modified and re-executed by the Story Diagram interpreter immediately without recompiling the source code and restarting the application. Our implementation also supports higher-order transformations by using Story Diagrams to modify other Story Diagrams. generation is not applicable, like running systems. While interpretation obviously results in performance drawbacks, we demonstrate that the Story Diagram interpreter is able to improve the performance in certain worst-case situations compared to the average generated code. This is achieved by a dynamic ordering of the matching process, which considers the actual number of elements in an association at runtime. Such a dynamic ordering can minimize the matching effort considerably. In contrast, Fujaba generated code uses a static matching strategy. Whereas the Fujaba Story Diagrams have potentially high performance fluctuations, the performance of the Story Diagram interpreter is steadier and more scalable compared to the generated Java code
A decidable class of verification conditions for programs with higher order store
Get PDFRecent years have seen a surge in techniques and tools for automatic and
semi-automatic static checking of imperative heap-manipulating programs. At the
heart of such tools are algorithms for automatic logical reasoning, using heap
description formalisms such as separation logic. In this paper we work towards
extending these static checking techniques to languages with procedures as first
class citizens. To do this, we first identify a class of entailment problems which arise naturally as verification conditions during the static checking of higher order heap-manipulating programs. We then present a decision procedure
for this class and prove its correctness. Entailments in our class combine
simple symbolic heaps, which are descriptions of the heap using a subset of
separation logic, with (limited use of) nested Hoare triples to specify
properties of higher order procedures
Integriertes Performance-Monitoring von SOA-Anwendungen
Get PDFDer Beitrag stellt einen Ansatz zur Integration von Performance-Monitoring-Aspekten in serviceorientierte Architekturen (SOAs) vor. Der Fokus liegt hierbei auf der konsistenten Instrumentierung bereits existierender SOA-Dienste. Hierfür wird ein im Rahmen des Projekts Performance Management of Enterprise Applications (PerManEntA) entwickeltesWerkzeug vorgestellt, das eine modellbasierte Instrumentierungsunterstützung mit Hilfe grafischer Marker vorsieht. Der Ansatz ermöglicht die Verwendung einheitlicher Monitoringschnittstellen und -funktionalität für alle in einer SOA kooperierenden Dienste und die konsistente Instrumentierung mit Hilfe teilautomatisierter, werkzeuggestützter Instrumentierung und Quellcodegenerierung. Im Ausblick werden Möglichkeiten zur Integration mit unterschiedlichen Ansätzen für das Service Level Management im SOA-Kontext aufgezeigt
Aspects for Graph Grammars
Get PDFAspect-oriented programming (AOP) is an extension to the object oriented paradigm that aims to provide better modularity for code that is usually scattered across an object-oriented system such as logging, authentication and distributed object handling. Aspect weaving is a novel way to compose systems, focusing on the integration of system-wide policies through pattern-action rules. While there are
several semantic proposals for representing aspects over source code and programs, aspect weaving for visual models such as graph rewriting systems is still not fully established. In this work, we propose the definition of aspect-oriented graph grammars, an extension to conventional graph grammar where aspects are modeled as transformation rules over the structure of a base graph grammar
Fighting Cheating in P2P-based MMVEs with Disjoint Path Routing
Get PDFIn a P2P-based Massively Multiuser Virtual Environment (MMVE) where
nodes cannot be trusted, replicating data on multiple nodes is a possibility to increase
the reliability to obtain correct data. Current structured P2P networks mostly
place replicas in such a way that queries for the replicas travel along similar paths.
A malicious node in the common part of all paths can nullify the security gain of
replicated data. We therefore propose to combine radix-based prefix routing with a
symmetric replication scheme to gain disjoint paths to each of the replicas