Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Decidable Race Condition and Open Coregions in HMSC
Get PDFMessage Sequence Charts (MSCs) is a visual formalism for the description of
communication behaviour of distributed systems. An MSC specifies relations
between communication events with partial orders. A situation when two
visually ordered events may occur in any order during an execution of an MSC
is called a race and is usually considered as a design error. While there
is a quadratic time algorithm detecting races in a finite communication
behaviours called Basic Message Sequence Charts (BMSCs), the race detection
problem is undecidable for High-level Message Sequence Charts (HMSCs), an
MSC formalism describing potentially infinite sets of potentially unbounded
behaviours. To improve this negative situation for HMSCs, we introduce two
new notions: a new concept of race called trace-race and an extension of the
HMSC formalism with open coregions, i.e. coregions that can extend over more
than one BMSC. We present three arguments showing benefits of our notions
over the standard notions of race and HMSC. First, every trace-race-free
HMSC is also race-free. Second, every race-free HMSC can be equivalently
expressed as a trace-race-free HMSC with open coregions. Last, the
trace-race detection problem for HMSC with open coregions is decidable and
PSPACE-complete. Finally, the proposed extension of coregions allows to
represent in a visual fashion whether an arbitrary number of racing events
in the usual MSC formalism are concurrent or not
Graph Algebras for Bigraphs
Get PDFBinding bigraphs are a graphical formalism intended to be a meta-model for mobile, concurrent and communicating systems. In this paper we present an algebra of typed graph terms which correspond precisely to binding bigraphs over a given signature. As particular cases, pure bigraphs and local bigraphs are described by two sublanguages which can be given a simple syntactic characterization.
Moreover, we give a formal connection between these languages and Synchronized Hyperedge Replacement algebras and the hierarchical graphs used in Architectural Design Rewriting. This allows to transfer results and constructions among formalisms which have been developed independently, e.g., the systematic definition of congruent bisimulations for SHR graphs via the IPO construction
From Petri Nets to Graph Transformation Systems
Get PDFHans-Joerg Kreowski was among the first researchers to point out that Place/Transition Petri nets can be interpreted as instances of Graph Transformation Systems, a fact now considered folklore.
We elaborate on this observation, discussing how several different models of Petri nets can be encoded faithfully into Graph Transformation Systems. The key idea we pursue is that the net encoding is uniquely determined, and distinct net models are mapped to alternative approaches to graph transformation
Towards Generalizing Visual Process Patterns
Get PDFVisual Process Patterns (VPP) is a visual language to describe constraints on the behavior of UML Activities. They have been developed for the sake of formulating and verifying requirements on business process models in a visual, intuitive way (with UML Activities being one possible description language). In the VPP approach, a visual process pattern is translated into an LTL formula, which can then be verified against a transition system describing the behavior of the Activity under consideration.
In this paper, we aim at generalizing VPP. We show how to formulate patterns more generally, using an enhanced version of the concrete syntax of the behavioral model under consideration. Additionally, we describe how these more general patterns can be verified against a modelâs behavior
Specifying OCL Constraints on Process Instantiations
Get PDFDue to the variety of concerns affecting software development in large organisations, processes have to be adapted to project specific needs to be effectively applicable in individual projects. We describe a project aiming to provide tool support for this individualised instantiation of reference processes, based on an OCL-based specification of instantiation operations. The aim is not only to execute instantiation decisions made by humans but to automatically ensure correctness of the resulting process, potentially resulting in followup actions being executed or suggested
Generation of Formal Model Metrics for MOF based Domain Specific Languages
Get PDFThe assessment of quality in a software development process is vital for the quality of the final system. A number of approaches exist, which can be used to determine such quality properties. In a model-driven development process models are the primary artifacts. Novel technologies are needed in order to assess the quality of those artifacts. Often, the Object Constraint Language is used to formulate model metrics and to compute them automatically afterwards. This paper describes an approach for the generation of model metrics expressed as OCL statements based on a set of generic rules. These rules can be applied on any domain specific modeling languages for creating a basic set of metrics which can be tailored for the specific needs of a development process. The paper also briefly describes a prototype of a tool for the generation, computation, and management of these model metrics by using the Software Metrics Meta-model - SMM
Assessment – Ein Ansatz zur Evaluierung selbstorganisierender Systeme
Get PDFSelbstorganisierende Systeme werden in der Kommunikationstechnik als Möglichkeit gesehen, die Dienstqualität zu verbessern und gleichzeitig den Administrationsaufwand zu senken. Die eingesetzten selbstanpassenden Algorithmen führen zu völlig neuen Systemeigenschaften, die beim Testen und der Evaluation der Leistungsfähigkeit dieser Systeme berücksichtigt werden müssen. Ausgehend von Definitionen zu kontextsensitiven Systemen und Überlegungen zu Schnittstellen zwischen der Testumgebung und dem zu testenden System wird das neuartige, als Assessment bezeichnete Evaluationsverfahren vorgestellt. Abschließend werden Probleme bei der Generierung von Testfällen diskutiert und dabei neue, anstehende Forschungsaufgaben skizziert. Der Ansatz soll zur Diskussion einer Systemtheorie dieser neuartigen Systeme beitragen und ganz praktisch das Vertrauen in die Arbeit derartiger, hochgradig flexibler Systeme stärken sowie deren zukünftigen Einsatz fördern
Efficient Analysis of Permutation Equivalence of Graph Derivations Based on Petri Nets
Get PDFIn the framework of graph transformation systems with Negative Application Conditions (NACs) the classical notion of switch equivalence of derivations is extended to permutation equivalence, because there are intuitively equivalent derivations which are not switch-equivalent if NACs are considered. By definition, two derivations are permutation-equivalent, if they respect the NACs and disregarding the NACs they are switch equivalent. A direct analysis of permutation
equivalence is very complex in general, thus we propose a much more efficient analysis technique. For this purpose, we construct a Place/Transition Petri net, called dependency net, which encodes the dependencies among rule applications of the
derivation, including the inhibiting effects of the NACs.
The analysis of permutation equivalence is important for analysing simulation runs within development environments for systems modelled by graph transformation. The application of the technique is demonstrated by a graph transformation system within the context of workflow modelling. We show the effectiveness of the approach by comparing the minimal costs of a direct analysis with the costs of the efficient analysis applied to a derivation of our example system
Second-Order Value Numbering
Get PDFWe present second-order value numbering, a new optimization method for suppressing redundancy, in a version tailored to the application for optimizing the decision procedure of jMosel, a verification tool set for monadic second-order logic on strings (M2L(Str)). The method extends the well-known concept of value
numbering to consider not merely values, but semantics transformers that can be efficiently pre-computed and help to avoid redundancy at the 2nd-order level. Since decision procedures for M2L are non-elementary, an optimization method like this can have a great impact on the execution time, even though our decision procedure comprises the analysis and optimization time for second-order value numbering.
This is illustrated considering a parametric family of hardware circuits, where we observed a performance gain by a factor of 3. This result is surprising, as the design of these circuits exploits already structural similarity