Wyniki wyszukiwania - BazTech

1

A UML 2.0 activity diagrams/csp integrated approach for modeling and verification of software systems

Elmansouri Raida, Meghzili Said, Chaoui Allaoua

Computer Science

|

2021

|

T. 22 (2)

209–233

EN

This paper proposes an approach that integrates UML 2.0 Activity Diagrams (UML2-ADs) and the communicating sequential process (CSP) for modeling and verifying software systems. A UML2-AD is used for modeling a software system, while a CSP is used for verification purposes. The proposed approach consists of another way of transforming UML2-AD models to CSP models. It also focuses on checking the correctness of some properties of the transformation itself. These properties are specified using linear temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on model -driven engineering (MDE). The meta-modeling is realized using the AToMPM tool, while the model transformation and the correctness of its properties are realized using the GROOVE tool. Finally, we illustrated this approach through a case study.

2

Review of The Data Modeling Standards and Data Model Transformation Techniques

Jaskierny Leszek

Applied Computer Science

|

2018

|

Vol. 14, no 4

93--108

EN

Manual data transformations that result in high error rates are a big problem in complex integration and data warehouse projects, resulting in poor quality of data and delays in deployment to production. Automation of data trans-formations can be easily verified by humans; the ability to learn from past decisions allows the creation of metadata that can be leveraged in future mappings. Significant improvement of the quality of data transformations can be achieved, when at least one of the models used in transformation is already analyzed and understood. Over recent decades, particular industries have defined data models that are widely adopted in commercial and open source solutions. Those models (often industry standards, accepted by ISO or other organizations) can be leveraged to increase reuse in integration projects resulting in a) lower project costs and b) faster delivery to production. The goal of this article is to provide a comprehensive review of the practical applications of standardization of data formats. Using use cases from the Financial Services Industry as examples, the author tries to identify the motivations and common elements of particular data formats, and how they can be leveraged in order to automate process of data transformations between the models.

3

Pattern-based Rewriting through Abstraction

Bottoni P., Guerra E., de Lara J.

Fundamenta Informaticae

|

2016

|

Vol. 144, nr 2

109--160

EN

Model-based development relies on models in different phases for different purposes, with modelling patterns being used to document and gather knowledge about good practices in specific domains, to analyse the quality of existing designs, and to guide the construction and refactoring of models. Providing a formal basis for the use of patterns would also support their integration with existing approaches to model transformation. To this end, we turn to the commonly used, in this context, machinery of graph transformations and provide an algebraic-categorical formalization of modelling patterns, which can express variability and required/forbidden application contexts. This allows the definition of transformation rules having patterns in left and right-hand sides, which can be used to express refactorings towards patterns, change the use of one pattern by a different one, or switch between pattern variants. A key element in our proposal is the use of operations to abstract models into patterns, so that they can be manipulated by pattern rules, thus leading to a rewriting mechanism for classes of graphs described by patterns and not just individual graphs. The proposal is illustrated with examples in object-oriented software design patterns and enterprise architecture patterns, but can be applied to any other domain where patterns are used for modelling.

4

Transformation of Typed Composite Graphs with Inheritance and Containment Structures

Jurack S., Taentzer G.

Fundamenta Informaticae

|

2012

|

Vol. 118, nr 1-2

97-134

EN

Model-driven development (MDD) has become a promising trend in software engineering. The model-driven development of highly complex software systems may lead to large models which deserve a modularization concept to enable their structured development in larger teams. Graphs are a natural way to represent the underlying structure of visual models. Typed graphs with inheritance and containment structures are well suited to describe the essentials of models based on the Eclipse Modeling Framework (EMF). Composite graphs can specify the logical distribution of EMF models and therefore, can form the conceptual basis for composite modeling in modeldriven development. This is done based on the formal foundation of distributed graphs. Moreover, this category-theoretical foundation allows for the precise definition of consistent composite graph transformations satisfying all inheritance and containment conditions.

5

Hoare-Style Verification of Graph Programs

Poskitt C. M., Plump D.

Fundamenta Informaticae

|

2012

|

Vol. 118, nr 1-2

135-175

EN

GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees programmers from dealing with low-level data structures. In this paper, we present a Hoare-style proof system for verifying the partial correctness of (a subset of) graph programs. The pre- and postconditions of the calculus are nested graph conditions with expressions, a formalism for specifying both structural graph properties and properties of labels. We show that our proof system is sound with respect to GP’s operational semantics and give examples of its use.

6

Counterpart Semantics for a Second-Order μ-Calculus

Gadducci F., Lafuente A. L., Vandin A.

Fundamenta Informaticae

|

2012

|

Vol. 118, nr 1-2

177-205

EN

Quantified &mi;-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behaviour of individual components within a software system. In this paper we introduce a novel approach to the semantics of such calculi: we consider a sort of labeled transition systems called counterpart models as semantic domain, where states are algebras and transitions are defined by counterpart relations (a family of partial homomorphisms) between states. Then, formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows us to model and reason about the creation and deletion of components, as well as the merging of components. Moreover, it avoids the limitations of existing approaches, usually enforcing restrictions of the transition relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of. The paper is rounded up with some considerations about expressiveness and decidability aspects.

7

Adhesivity with Partial Maps instead of Spans

Heindel T.

Fundamenta Informaticae

|

2012

|

Vol. 118, nr 1-2

1-33

EN

The introduction of adhesive categories revived interest in the study of properties of pushouts with respect to pullbacks that started over thirty years ago for the category of graphs. Adhesive categories - of which graphs are the 'archetypal' example - are defined by a single property of pushouts along monos that implies essential lemmas and central theorems of double pushout rewriting such as the local Church-Rosser Theorem. The present paper shows that a strictly weaker condition on pushouts suffices to obtain essentially the same results: it suffices to require pushouts to be hereditary, i.e. they have to remain pushouts when they are embedded into the associated category of partial maps. This fact however is not the only reason to introduce partial map adhesive categories as categories with pushouts along monos (of a certain stable class) that are hereditary. There are two equally important motivations: first, there is an application relevant example category that cannot be captured by the more established variations of adhesive categories; second, partial map adhesive categories are 'conceptually similar' to adhesive categories as the latter can be characterized as those categories with pushout along monos that remain bi-pushouts when they are embedded into the associated bi-category of spans. Thus, adhesivity with partial maps instead of spans appears to be a natural candidate for a general rewriting framework.

8

Formal Analysis of Service-oriented Architectures

Rafe V.

Przegląd Elektrotechniczny

|

2011

|

R. 87, nr 11

310-313

EN

Even though model checking is one of the most accurate analyses techniques to verify software systems, the problem of model checking is that it is not feasible for large and complex software systems, which their state spaces are too large. In these situations one can use scenariobased model checking techniques. In this paper, we present an approach to analyze large and complex systems specified by graph transformation systems. To do so, we propose the scenario-based model checking techniques. We explain how the approach will affect to the size of the state space by focusing on the most important occurring scenarios in a system.

PL

Problem sprawdzania modelu software jest istotny jeśli badamy duży i złożony system. W artykule zaprezentowano metodę umożliwiającą taką analizę systemu opisanego przez transformację grafu. Zaproponowano technikę sprawdzania opierającą się na modelu bazującym na scenariuszu.

9

GRADIS - środowisko dla Rozproszonych Transformacji Grafowych (z perspektywy pięciu lat badań)

Kotulski L.

Pomiary Automatyka Robotyka

|

2011

|

R. 15, nr 12

150-151

PL

W niniejszym artykule zaprezentowano historię prowadzonych w Katedrze Automatyki pod kierunkiem Autora badań w zakresie przetwarzania transformacji grafowych w środowisku rozproszonym.

EN

The article presents a brief history of investigation made in the area of the distributed graph transformation. Their effect is designing the multiagent GRADIS environment.

10

Matrix Graph Grammars with Application Conditions

Velasco P.P.P.

Fundamenta Informaticae

|

2010

|

Vol. 99, nr 1

29-62

EN

In the Matrix approach to graph transformation we represent simple digraphs and rules with Boolean matrices and vectors, and the rewriting is expressed using Boolean operators only. In previous works, we developed analysis techniques enabling the study of the applicability of rule sequences, their independence, state reachability and the minimal graph able to fire a sequence. In the present paper we improve our framework in two ways. First, we make explicit (in the form of a Boolean matrix) some negative implicit information in rules. This matrix (called nihilation matrix) contains the elements that, if present, forbid the application of the rule (i.e. potential dangling edges, or newly added edges, which cannot be already present in the simple digraph). Second, we introduce a novel notion of application condition, which combines graph diagrams together with monadic second order logic. This allows for more flexibility and expressivity than previous approaches, as well as more concise conditions in certain cases. We demonstrate that these application conditions can be embedded into rules (i.e. in the left hand side and the nihilation matrix), and show that the applicability of a rule with arbitrary application conditions is equivalent to the applicability of a sequence of plain rules without application conditions. Therefore, the analysis of the former is equivalent to the analysis of the latter, showing that in our framework no additional results are needed for the study of application conditions. Moreover, all analysis techniques of [21, 22] for the study of sequences can be applied to application conditions.

11

Autonomous Units to Model Interacting Sequential and Parallel Processes

Hölscher K., Kreowski H-J., Kuske S.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 3

233-257

EN

In this paper, we introduce the notion of a community of autonomous units as a rulebased and graph-transformational device to model processes that run interactively but independently of each other in a common environment. The main components of an autonomous unit are a set of rules, a control condition, and a goal. Every autonomous unit transforms graphs by applying its rules so that the control condition is satisfied. If the goal is reached the resulting transformation process is successful. A community contains a set of autonomous units, an initial environment specification, and an overall goal. In every transformation process of a community the autonomous units interact via their common environment. As an example, the game Ludo is modeled as a community of self-controlled players who interact on a common board. The emphasis of the presented approach is laid on the study of the formal semantics of a community as a whole and of each of its member units separately. In particular, a sequential as well as a parallel semantics is introduced, and communities with parallel semantics are compared with Petri nets, cellular automata, and multiagent systems.

12

Real-time ice visualisation on the GPU

Szajerman D., Pietruszka M.

Journal of Applied Computer Science

|

2008

|

Vol. 16, nr 2

89-106

EN

Today the most interactive graphics applications tend to render plausible realism using clever ideas of mapping subproblems of global illumination to Graphics Processing Units (GPU) or/and storing precomputed solutions in an appropriate manner. In this paper an empirical model of an ice-like material as an example of a multi-feature material is provided. Thanks to shaders whole presented rendering methods allow to work in interactive, on-line mode. A few datasets was used to check the performance of the rendering.

13

Parallel allocation of the distributed software using node label controlled graph grammars

Kotulski L.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2008

|

T. 12, z. 2

321-337

EN

Centralization of a graph's data is useful while we consider properties of some system specification but it seems to be not acceptable in the case of the support an efficient, high reliably system with a dynamic software allocation. In the paper, we introduce the aedNLC graph grammar, that has both polynomial computational complexity and enough descriptive power to coordinate parallel modification of a few local graphs (representing parts of the system), in such a way that the global consistency of the distributed system specification can be maintained.

PL

Rozważając własności specyfikacji systemów, utrzymujemy grafy w postaci scentralizowanej, ale dla efektywnego wspierania dynamicznej alokacji oprogramowania w środowisku rozproszonym, struktury grafowe powinny być również rozproszone. W artykule przedstawiamy gramatykę aedNLC, która zachowując wielomianową złożoność obliczeniową parsingu, ma wystarczającą moc opisową dla koordynacji równoległych modyfikacji lokalnych grafów (reprezentujących podsystemy) w taki sposób, że globalna spójność specyfikacji systemu rozproszonego będzie zachowana.

14

Locally Derivable Graphs

Mazurkiewicz A.

Fundamenta Informaticae

|

2007

|

Vol. 75, nr 1-4

335-355

EN

In the paper a class of locally derivable graphs is defined and discussed. Well known particular cases of derivable graphs are (among others) trees, complete, and triangular graphs; in the paper a broader class of locally derivable graphs, called closed graphs, is defined. Nodes and edges of closed graphs can be partitioned into external and internal ones; the main property of such graphs their local reducibility: successive removing its external nodes leads eventually to a singleton, and removing its external edges leads to an a spanning tree of the graph. The class of closed graphs is then a class enabling structural reducing. This property can be applied in processor networks to design some local procedures leading to global results.

15

On the support UML diagrams understanding during the software maintenance

Kotulski L., Basiura A.

Computer Methods in Materials Science

|

2007

|

Vol. 7, No. 3

366-375

EN

NOTE It was previously reviewed as :On the support image understanding during the software maintenance. Abstract. UML diagrams are generally accepted technique of supporting computing modeling and maintenance systems that are independent from the domain supported by the created system. Final model describes the system with help of object oriented techniques such as class inheritance, packages or the final software deployment diagrams. The mentioned techniques introduce some hierarchy of the developed concepts. An UML model describing all aspects of a system is hard to fully visualized. Usually they contain thousands of elements and relations which are difficult to present in form that can be easy to understand. Unfortunately, we are not able to represent such structures with help of the 2-dimensions manner (monitor screens or paper sheets) so we present only some "flat" aspects of these structures; it is desirable that we should be able move from one "flat" visualization of the hierarchical structure to another one. In this paper, we formalize the term "a flat visualization of the hierarchical graph", and specify the synthesis and analysis operations, that allow us to move between different flat forms. Practical aspect of this proposition is discussed for UML deployment and class diagrams.

PL

Diagramy UML są powszechnie stosowaną techniką wspomagającą modelowanie systemów obiektowych; stają się również wysoce użyteczne podczas modyfikacji systemu spowodowanej zmianami wymagań użytkowników. Pełny model systemu ilustruje jednak wielowymiarowe relacje pomiędzy setkami (tysiącami) składników, często opisywanych w różnych kontekstach (typach diagramów) i poziomach szczegółowości. Takie nasycenie elementów i relacji pomiędzy nimi powoduje bardzo często że model systemu przekracza możliwości percepcyjne człowieka i często jest on pomijany podczas procesu rozwoju. W artykule podejmujemy próbę czytelnego przedstawienia tych powiązań na dwuwymiarowym ekranie komputera. Proponujemy wyświetlanie informacji przedstawiającą tylko jedną perspektywę (tzw. płaską wizualizację grafu) zawierającą przefiltrowany zbiór informacji dotyczących danej części systemu (logicznej lub fizycznej). Udostępniamy użytkownikowi możliwość iteratywnej zmiany tej prospektywny na inną, która z nią jest powiązana. Proces ten opieramy na bazie grafów hierarchicznych, podajemy formalną specyfikację pojęcia płaskiej wizualizacji grafu, oraz definiujemy operacje analizy i syntezy pozwalające zmienić analizowaną perspektywę na inną bardziej (mniej) szczegółową. Wykorzystanie wprowadzonego aparatu formalnego, przedstawione jest na przykładzie analizy diagramów klas i diagramów wdrożenia.

16

Theory of Constraints and Application Conditions: From Graphs to High-Level Structures

Ehrig H., Ehrig K., Habel A., Pennemann K-H.

Fundamenta Informaticae

|

2006

|

Vol. 74, nr 1

135-166

EN

Graph constraints and application conditions are most important for graph grammars and transformation systems in a large variety of application areas. Although different approaches have been presented in the literature already there is no adequate theory up to now which can be applied to different kinds of graphs and high-level structures. In this paper, we introduce a general notion of graph constraints and application conditions and show under what conditions the basic results can be extended from graph transformation to high-level replacement systems. In fact, we use the new framework of adhesive HLR categories recently introduced as combination of HLR systems and adhesive categories. Our main results are the transformation of graph constraints into right application conditions and the transformation from right to left application conditions in this new framework. The transformations are illustrated by a railroad control system with rail net constraints and application conditions.

17

Adhesive High-Level Replacement Systems: A New Categorical Framework for Graph Transformation

Ehrig H., Padberg J., Prange U.

Fundamenta Informaticae

|

2006

|

Vol. 74, nr 1

1-29

EN

Adhesive high-level replacement (HLR) systems are introduced as a new categorical framework for graph transformation in the double pushout (DPO) approach, which combines the well-known concept of HLR systems with the new concept of adhesive categories introduced by Lack and Sobociński. In this paper we show that most of the HLR properties, which had been introduced to generalize some basic results from the category of graphs to high-level structures, are valid already in adhesive HLR categories. This leads to a smooth categorical theory of HLR systems which can be applied to a large variety of graphs and other visual models. As a main new result in a categorical framework we show the Critical Pair Lemma for the local confluence of transformations. Moreover we present a new version of embeddings and extensions for transformations in our framework of adhesive HLR systems.

18

Diagrammatic spreadsheet

Le T. L., Kulpa Z.

Machine Graphics and Vision

|

2003

|

Vol. 12, No. 1

133-146

EN

The diagramatic spreadsheet concept to develop a fully interactive animated diagrammatic system in which the transformation and animation of the diagram is interactively avaible to the user in a click-and-drag mode, and the description of what elements can move, and in what way (according to the required constraints between their components) can be also easily and interactively defined by the user. A constraint is used here like a formula in a spreadsheet, which is employed to automatically recompute the value of a cell whenever any other cells bound to it by the constraint undergo change. The graphical elements of the diagram play the role of spreadsheet cells, and their various attributes constitute the cell contents. The system may be used by human users for interactive exploration of diagrammatic representation and reasoning problems, or as a front-end to a more automatic diagrammatic inference system. In the paper, an overview of this concept and general construction principles of the system are described.

19

Context-exploiting shapes for diagram transformation

Drewes F., Hoffmann B., Minas M.

Machine Graphics and Vision

|

2003

|

Vol. 12, No. 1

117-132

EN

DIA PLAN is a language for programming with graphs representing diagram that is currently being developed. The computational model of the language - nested graph transformation - suports nested structuring of graphs and graph variables, but is still intuitive. This paper discusses structural typing of nested graphs and nested graph transformation systems by shape rules. We extend the context-free shape rules proposed in earlier work to contexy-exploiting shape rules with which many relevant graph structures can be specifed. The conformance of a nested graph to the shape rules is decidable. If a trabsformation system conforms to shape rules as well. it can be shown to preserve shape conformance of the graphs it is applied to. This sets up a static type discipline for nested graph transformation.

20

Graph Transformation with Time

Gyapay S., Varró D., Heckel R.

Fundamenta Informaticae

|

2003

|

Vol. 58, nr 1

1--22

EN

Following TER nets, an approach to the modeling of time in high-level Petri nets, we propose a model of time within (attributed) graph transformation systems where logical clocks are represented as distinguished node attributes. Corresponding axioms for the time model in TER nets are generalized to graph transformation systems and semantic variations are discussed. They are summarized by a general theorem ensuring the consistency of temporal order and casual dependencies. The resulting notions of typed graph transformation with time specialize the algebraic double-pushout (DPO) approach to typed graph transformation. In particular, the concurrency theory of the DPO approach can be used in the transfer of the basic theory of TER nets.