Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Functorial Analysis of Algebraic Higher-Order Net Systems with Applications to Mobile Ad-Hoc Networks
Get PDFAlgebraic higher-order (AHO) net systems are Petri nets with place/
transition systems, i.e. place/transition nets with initial markings, and rules as tokens.
In several applications, however, there is the need for explicit data modeling.
The main idea of this paper is to introduce AHO net systems with high-level net
systems and corresponding rules as tokens. We relate them to AHO net systems
with low-level net systems as tokens and analyze the firing and transformation properties
of the corresponding net class transformation defined as functors between the
corresponding categories of AHO net systems.
All concepts and results are explained with an example in the application area of
mobile ad-hoc networks. From an abstract point of view, mobile ad-hoc networks
consist of mobile nodes which communicate with each other independent of a stable
infrastructure, while the topology of the network constantly changes depending on
the current position of the nodes and their availability. To ensure satisfactory team
cooperation in workflows of mobile ad-hoc networks we use the modeling technique
of AHO net systems
Towards Guided Trajectory Exploration of Graph Transformation Systems
Get PDFGraph transformation systems (GTS) are often used for modeling the behavior of complex systems. A common GTS analysis scenario is the exploration of its state space from an initial state to a state adhering to given goals through a proper
trajectory. Guided trajectory exploration uses information from some more abstract analysis of the system as hints to reduce the traversed state space. These hints are used to order possible further transitions from a given state (selection) and detect violations early (cut-off), thus pruning unpromising trajectories from the state space.
In the current paper, we define cut-off and selection criteria for guiding the trajectory exploration, and use Petri Net analysis results and the dependency relations between rules as hints in our criteria calculation algorithm. The criteria definitions include navigation along dependency relations, various types of ordering for selection and quantifiers for cut-off criteria. Our approach is exemplified on a cloud infrastructure configuration problem
Combination of Different Layout Approaches
Get PDFIn an interactive environment such as a visual language editor, it is not sufficient to apply the same layout algorithm in every situation. Instead, the user often wants to select the layout behavior at runtime. With the approach presented, the user can control the layout behavior by choosing different layout patterns for different parts of a diagram, e.g., a graph drawing algorithm may be applied to some selected components while others are aligned vertically or horizontally.
To enable the specification of layout behavior, we introduced the concept of layout patterns in previous work. Each layout pattern encapsulates certain layout behavior, and hence enables modularization and reuse.
To specify user-controlled layout behavior, a flexible combination of arbitrary layout patterns needs to be enabled. Therefore, we introduce an approach that is capable of combining diverse layout approaches, such as standard graph drawing algorithms, constraint-based algorithms, or rule-based layout algorithms. More specifically, an algorithm is presented that automatically computes the complete layout in a straightforward way
UML is still inconsistent! How to improve OCL Constraints in the UML 2.3 Superstructure
Get PDFSince the first OMG specification of the Unified Modeling Language (UML), the Object Constraint Language (OCL) has been used for the definition of well-formedness rules in the UML specification. These rules have been specified within the early OCL years, when no appropriate tooling existed. Thus, they could not be checked for syntactical and static semantics correctness. In this paper we present an analysis of the static correctness of all OCL rules specified in the UML 2.3 superstructure document. We categorise found errors and propose changes for both the UML specification process and the OCL language to improve the UML specification’s correctness in future versions
Distributed Graph-Based State Space Generation
Get PDFLTSMIN provides a framework in which state space generation can be distributed easily over many cores on a single compute node, as well as over multiple compute nodes. The tool works on the basis of a vector representation of the states; the individual cores are assigned the task of computing all successors of states that are sent to them. In this paper we show how this framework can be applied in the case where states are essentially graphs interpreted up to isomorphism, such as the ones we have been studying for GROOVE. This involves developing a suitable vector representation for a canonical form of those graphs. The canonical forms are computed using a third tool called BLISS. We combined the three tools to form a system for distributed state space generation based on graph grammars.
We show that the time performance of the resulting system scales well (i.e., close to linear) with the number of cores. We also report surprising statistics on the memory consumption, which imply that the vector representation used to store graphs in LTSMIN is more compact than the representation used in GROOVE
Towards a Maude Tool for Model Checking Temporal Graph Properties
Get PDFWe present our prototypical tool for the verification of graph transformation systems. The major novelty of our tool is that it provides a model checker for temporal graph properties based on counterpart semantics for quantified mu-calculi. Our tool can be considered as an instantiation of our approach to counterpart semantics which allows for a neat handling of creation, deletion and merging in systems with dynamic structure. Our implementation is based on the object-based machinery of Maude, which provides the basics to deal with attributed graphs. Graph transformation systems are specified with term rewrite rules. The model checker evaluates logical formulae of second-order modal mu-calculus in the automatically generated Counterpart Model (a sort of unfolded graph transition system) of the graph transformation system under study. The result of evaluating a formula is a set of assignments for each state, associating node variables to actual nodes
Application Conditions for Reactive Systems with Applications to Bisimulation Theory
Get PDFThis paper presents generalized application conditions (GACs), a new
formalism for nested application conditions. GACs are not only suitable for DPO
rewriting, but for rewriting in reactive systems as well. The main theorem states that
it is possible to construct an equivalent reactive system rule with a GAC for a DPO
rule with application conditions under very mild conditions. The resulting reactive
system rules live in the cospan category of the category C, in which the DPO rules
live.
It turns out that these GACs for reactive systems provide a slightly more powerful
way to control the application of a rewriting rule, than it is possible in the original
DPO setting.
At the end, we give a short outlook on the applications of this formalism to the field
of bisimulation theory, sketch our latest results and discuss future work
New Media in Teaching UML in the Large — an Experience Report
Get PDFHuge classes with more than 800 students pose a major challenge to lecturers as well as to students, especially when a practical part is included. In order to successfully master lectures of this size, novel kinds of teaching media provide a
multitude of enhanced opportunities.
In this paper, we present our experiences with the application of new media in our undergraduate course Introduction to Object-Oriented Modeling (OOM). In this course, we teach approximately 800-1000 students per year the principles and techniques of UML 2.0. New media, i.e., technologies other than the traditional blackboard presentation like a document camera, web-based self assessments, or lecture recordings, are applied to support both, students and lecturers when learning and teaching, respectively. We empirically underline the acceptance of our concept with the feedback of our students concerning the newly used technologies gained through an extensive survey
From the Behavior Model of an Animated Visual Language to its Editing Environment Based on Graph Transformation
Get PDFAnimated visual models are a reasonable means for illustrating system behavior. However, implementing animated visual languages and their editing environments is difficult. Therefore, guidelines, specification methods, and tool support are necessary. A flexible approach for specifying model states and behavior is to use graphs and graph transformations. Thereby, a graph can also represent dynamic aspects of a model, like animations, and graph transformations are triggered over time to control the behavior, like starting, modifying, and stopping animations or adding and removing elements. These concepts had already been added to Dia-Meta, a framework for generating editing environments, but they provide only low-level support for specifying and implementing animated visual languages; specifying complex dynamic languages was still a challenging task. This paper proposes the Animation Modeling Language (AML), which allows to model behavior and animations on a higher level of abstraction. AML models are then translated into low-level specifications based on graph transformations. The approach is demonstrated using a traffic simulation
Role Allocation and Scheme in Software Engineering Course Projects
Get PDFRole is a set of behavioural actions and responsibilities one takes in a specific situation. We play different roles with our family, at work as well as in other environments. Differences among the role definitions reach mainly from the different emphasis of the software development method itself. Agile software development methods define roles to enhance communication and to produce a better product. In this paper, we describe a role allocation and scheme method whose data were gathered in student’s projects in software engineering course in the university