Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
eSOA - SOA für eingebettete Netze
No full textEingebettete Netze, bestehend aus einer Vielzahl von vernetzten Knoten mit unterschiedlichen Mess-, Steuer- und Rechenfähigkeiten, werden zunehmend in Bereichen wie der Heim- und Industrieautomatisierung, modernen Kraftfahrzeugen
oder großflächigen Infrastrukturen z.B. in Energienetzen oder Verkehrsleitsystemen eingesetzt. Die Komplexität der Netze, die Heterogenität der enthaltenen Knoten und Infrastrukturänderungen durch mobile Knoten oder Knotenausfälle stellen besondere Herausforderungen während der Anwendungsentwicklung dar. Viele dieser Anforderungen können durch die aus dem Software-Bereich wohlbekannten Service orientierten Architekturen (SOAs) erfüllt werden. Um die besonderen Rahmenbedingungen von eingebetteten Netzen (Ressourcenbeschränkungen, Echtzeitanforderungen,
etc) berücksichtigen zu können, sind einige Anpassungen des traditionellen SOA Paradigmas aus dem Web Service Kontext nötig. Ziel des eSOA-Projekts ist die Definition eines embedded-SOA-(eSOA)-Konzepts, das diesen Anforderungen
genügt, und die Entwicklung einer Middleware für eingebettete Netze und den dazugehörigen Entwicklungswerkzeugen, welche eine effiziente Anwendungsentwicklung ermöglichen
Permutation Equivalence of DPO Derivations with Negative Application Conditions based on Subobject Transformation Systems
Get PDFSwitch equivalence for transformation systems has been successfully used in many domains for the analysis of concurrent behaviour. When using graph transformation as modelling framework for these systems, the concept of negative application conditions (NACs) is widely used - in particular for the specification of operational semantics.
In this paper we show that switch equivalence can be improved essentially for the analysis of systems with NACs by our new concept of permutation equivalence.
Two derivations respecting all NACs are called permutation-equivalent, if they are switch-equivalent disregarding the NACs. In fact, there are permutation-equivalent derivations which are not switch-equivalent with NACs.
As main result of the paper, we solve the following problem:
Given a derivation with NACs, we can efficiently derive all permutation-equivalent derivations to the given one by static analysis. The results are based on extended techniques for subobject transformation systems, which have been introduced recently
An Extension of the Inverse Method to Probabilistic Timed Automata
Get PDFProbabilistic timed automata can be used to model systems in which probabilistic and timing behavior coexist.
Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation of the timing parameters.
Given such a parameter valuation, we present a method for obtaining automatically a constraint on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation.
The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the "inverse method'".
Our approach is useful for avoiding repeated executions of probabilistic model checking analyses for the same model with different parameter valuations.
We provide examples of the application of our technique to models of randomized protocols
Automatically Finding Bugs in Open Source Programs
Get PDFWe consider properties desirable for static analysis tools targeted at finding bugs in the real open source code, and review tools based on various approaches to defect detection. A static analysis tool is described, that includes a framework for flow-sensitive interprocedural dataflow analysis and scales to analysis of large
programs. The framework enables implementation of multiple checkers searching for specific bugs, such as null pointer dereference and buffer overflow, abstracting from the checkers details such as alias analysis
Repotting the Geraniums: On Nested Graph Transformation Rules
Get PDFWe propose a scheme for rule amalgamation based on nested graph predicates. Essentially, we extend all the graphs in such a predicate with right hand sides. Whenever such an enriched nested predicate matches (i.e., is satisfied by) a given
host graph, this results in many individual match morphisms, and thus many âsmallâ rule applications. The total effect is described by the amalgamated rule. This makes for a smooth, uniform and very powerful amalgamation scheme, which we demonstrate
on a number of examples. Among the examples is the following, which we believe to be inexpressible in very few other parallel rule formalism proposed in the literature: repot all flowering geraniums whose pots have cracked
A Pattern-Based Approach to Manage Model References
Get PDFModel references play an important role in model integration, especially when models belonging to different domains are to be integrated. They are also needed in various model transformation tasks. In some cases, they need to be instantiated systematically, following certain rules. This calls for an instantiation specification of model references.
In this paper we propose a pattern-based approach for modeling, specifying, and finally applying model references. We represent model references as so-called collaboration patterns,
modeled as UML collaborations. We further describe the instantiation rules of collaboration patterns. A tool has been implemented for establishing the model references according to the specification, allowing the designer to assist in the process of semi-automated model reference instantiation. We demonstrate the usefulness of the approach and tools by applying them in designing Web service orchestrations
A coinductive approach to verified exact real number computation
Get PDFWe present an approach to verified programs for
exact real number computation that is based on inductive and
coinductive definitions and program extraction from proofs.
We informally discuss the theoretical background of this method
and give examples of extracted programs implementing
the translation between the representation by fast converging
rational Cauchy sequences and the signed binary
digit representations of real numbers
Toward Automated Verification of Model Transformations: A Case Study of Analysis of Refactoring Business Process Models
Get PDFVerification of the transformations is a fundamental issue for applying them in real world solutions. We have previously proposed a formalization to declaratively describe model transformations and proposed an approach for the verification. Our approach consists of a reasoning system that works on the formal transformation description and deduction rules for the system. The reasoning system can automatically generate the proof of some properties. In this paper, we present a case study, to demonstrate our approach of automated verification of model transformations in a multi-paradigm environment
Flexible Modeling of Emergency Scenarios using Reconfigurable Systems
Get PDFIn emergency scenarios we can obtain a more effective coordination among team members constituting a mobile ad hoc network (MANET) through the use of reconfigurable systems. This means that cooperative work can be adequately modeled by low level and high level Petri nets with initial markings and the net structure can be adapted to new requirements of the environment during run time by a set of rules. In this paper we give main requirements for flexible processes in MANETs and show how to realize them using the formal notions of reconfigurable systems. The main part presents a case study in the area of emergency management and demonstrates the advantages of our approach which allows the dynamic adaption of processes in mobile environments. In this context we also discuss the main results achieved for reconfigurable systems and outline some interesting aspects of future work
A Novel Opportunistic Spectrum Sharing Scheme for Cognitive Ad Hoc Networks
Get PDFNowadays, wireless ad hoc networks are using a static spectrum allocation which leads to congestion in this spectrum parts as the number of devices increases. On the contrary, a significant portion of the spectrum in licensed band (e.g. TV band) is not utilized. Cognitive radio (CR) is a promising technology to solve the spectrum inefficiency problem in ad hoc networks. Based on CR, the unlicensed (secondary) users will utilize the unused spectrum of the licensed (primary) users in an opportunistic manner. As a result, the average spectrum usage will be increased. However, the sudden appearance of primary users will have a negative impact on the performance of secondary users, since secondary users must evacuate the occupied channel and handoff to another unutilized one. This process continues till an unlicensed user finishes his transmission. We will name this process consecutive spectrum handoff (CSH). In order to increase the performance of CR, the number of consecutive spectrum handoffs should be reduced. In this paper, a novel opportunistic spectrum sharing scheme under a heterogeneous spectrum environment of licensed and unlicensed bands is introduced. In this scheme, the licensed channels will be used as operating channels and the unlicensed channels will be used as backup channels when the primary user appears. Since the unlicensed channels are not interrupted by primary users, no more spectrum handoff is needed