共查询到20条相似文献,搜索用时 15 毫秒
1.
UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams. 相似文献
2.
The Unified Modeling Langugage (UML) offers different diagram types to model the behavior of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time in behavioral models since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain.We have proposed Dynamic Meta Modeling (DMM), an approach based on graph transformation, as a means for specifying operational semantics of dynamic UML diagrams. In this article, we extend this approach to also account for time by extending the semantic domain to timed graph transformation. This enables us to define the operational semantics of UML diagrams with time specifications. As an example, we provide semantics for special sequence diagrams from the domain of multimedia application modeling. 相似文献
3.
Fundamental properties of model transformations based on triple graph grammars (TGGs) have been studied extensively including syntactical correctness, completeness, termination and functional behavior. But up to now, it is an open problem how domain specific properties that are valid for a source model can be preserved along model transformations such that the transformed properties are valid for the derived target model. This question shows up in enterprise modeling. Here, modeling activities related to different domains are handled by different parties, and their models need to be consistent and integrated into one holistic enterprise model later on. So, support for decentralized modeling processes is needed. One technical aspect of the needed support in this case is the (bidirectional) propagation of constraints because that enables one party to understand and check the constraints of another party. Therefore, we analyze in the framework of TGGs how to propagate constraints from a source model to an integrated model and, afterwards, to a target model, such that, whenever the source model satisfies the source constraint, also the integrated and target model satisfy the corresponding integrated and target constraint. In our main new results we show under which conditions this is possible. 相似文献
4.
Transformations of graphlike expressions are called correct if they preserve a given functional semantics of the expressions. Combining the algebraic theories of graph grammars (cf. [10]) and programming language semantics (cf. [1]) it will be proved that the correctness of transformation rules carries over to the correctness of derivations via such rules. Applying this result to LISP we show that a LISP interpreter represented by a graph grammar is correct with respect to the functional semantics of graphlike LISP expressions. 相似文献
5.
Graph transformation systems are a well-founded and adequate technique to describe the syntax of visual modeling languages and to formalize their semantics. Moreover, graph transformation tools support visual model specification, simulation and analysis on the basis of the rich underlying theory.Despite the benefits of model validation by simulation, sometimes it is preferable for users to see the model's behavior not in the abstract layout of the formal model, but as scenarios presented in the layout of the specific application domain. Hence, we propose the integration of a domain-oriented animation view with the model transformation system. An animation view allows to define scenario animations in a systematic way based on the formal model. The specification of the well-known Dining Philosophers system as algebraic high-level Petri net serves as running example for the extension of the model by an animation view and the derivation of animation rules from the model transformation system. A scenario animation then is obtained as transformation by applying the animation rules to model states. This visualizes the behavior of the model in the layout of philosophers sitting around a table and eating with chopsticks. A prototypical implementation of the concepts in GenGED, a visual language environment, is presented. 相似文献
6.
This paper presents Model Algebra (MA), a formalism for representing SoC designs at system level. We define the objects and
composition rules of MA and show how system level models can be represented as expressions in this formalism. The formalism
is applied to a system level design methodology, where design decisions are used to gradually transform the functional specification
model of the system to a transaction level model with components and communication structure. Each transformation is represented
as a manipulation of a model algebraic expression, and proven for correctness using the laws of model algebra. These laws
are based on the well defined execution semantics and notion of functional equivalence for MA models. Our approach promises
significant savings in the verification of system level models because only the first model needs to be verified using conventional
techniques. All transformations of this model, derived using MA laws, are proven to be functionally equivalent. 相似文献
7.
The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches, it is usually not really clear under which constraints particular implementations really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. While the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static and runtime checks can be employed to guarantee these criteria. 相似文献
8.
In this paper, we use the UML MARTE profile to model high-performance embedded systems (HPES) in the G ASPARD2 framework. We address the design correctness issue on the UML model by using the formal validation tools associated with
synchronous languages, i.e., the S IGALI model checker, etc. This modeling and validation approach benefits from the advantages of UML as a standard, and from the
number of validation tools built around synchronous languages. In our context, model transformations act as a bridge between
UML and the chosen validation technologies. They are implemented according to a model-driven engineering approach. The modeling
and validation are illustrated using the multimedia functionality of a new-generation cellular phone. 相似文献
9.
A conceptual framework for the integration of data type and process modeling techniques, called integration paradigm, has been presented by the authors in previous papers already. The aim of this paper is to give a short review of this conceptual framework and to present a formal model for the integration paradigm. The formal model for the four layers, called data type, data states and transformations, processes and system architecture layers respectively, is based on an integration of abstract data types and structured transition systems. This formal model can be instantiated by all kinds of basic and integrated modeling techniques. Algebraic high-level nets, attributed graph transformation, an integration of Z with statecharts, and some diagram techniques of UML are discussed on the conceptual level. As instantiation of the formal model, a well-known CCS sender specification, place/transition nets, algebraic high-level nets and attributed graph transformation are presented in this paper, while instantiations of other modeling techniques will be discussed elsewhere. 相似文献
10.
In this paper, we investigate change-driven model transformations, a novel class of transformations, which are directly triggered by complex model changes carried out by arbitrary transactions on the model (e.g. editing operation, transformation, etc). After a classification of relevant change scenarios, we identify challenges for change-driven transformations. As the main technical contribution of the current paper, we define an expressive, high-level language for specifying change-driven transformations as an extension of graph patterns and graph transformation rules. This language generalizes previous results on live model transformations by offering trigger events for arbitrarily complex model changes, and dedicated reactions for specific kinds of changes, making this way the concept of change to be a first-class citizen of the transformation language. We discuss how the underlying transformation engine needs to be adapted in order to use the same language uniformly for different change scenarios. The technicalities of our approach will be discussed on a (1) model synchronization case study with non-materialized target models and (2) a case study on detecting the violation of evolutionary (temporal) constraints in the security requirements engineering domain. 相似文献
11.
In the framework of graph transformation, simulation rules define the operational behavior of visual models. Moreover, it has been shown already how to construct animation rules from simulation rules by so-called S2A-transformation. In contrast to simulation rules, animation rules use symbols representing entities from the application domain in a user-oriented visualization. Using animation views for model execution provides better insights of model behavior to users, leading to an earlier detection of model inconsistencies. Hence, an important requirement of the animation view construction is the preservation of the behavior of the original visual model. This means, we have to show on the one hand semantical correctness of the S2A-transformation, and, on the other hand, semantical correctness of a suitable backwards-transformation A2S. Semantical correctness of a model and rule transformation means that for each sequence of the source system we find a corresponding sequence in the target system. S2A-transformation has been considered in our contribution to GraMoT 2006. In this paper, we give a precise definition for animation-to-simulation ( A2S) backward transformation, and show under which conditions semantical correctness of an A2S backward transformation can be obtained. The main result states the conditions for S2A-transformations to be behavior-preserving. The result is applied to analyze the behavior of a Radio Clock model's S2A-transformation. 相似文献
12.
In this paper we study the problem of designing and specifying standard program components applicable to a wide variety of tasks; we choose for this study the specific problem domain of data structures for general searching problems. Within this domain Bentley and Saxe [1] have developed transformations for converting solutions of simple searching problems to solutions of more complex problems. We discuss one of those transformations, specify precisely the transformation and its conditions of applicability, and prove its correctness; we accomplish this by casting it in terms of abstract data types–specifically by using the Alphard form mechanism. The costs of the structures derived by this transformation are only slightly greater than the costs of the original structures, and the correctness of the transformation definition together with the correctness of the original structure assure the correctness of the derived structure. The transformation we describe has already been used to develop a number of new algorithms, and it represents a new level of generality in software engineering tools. 相似文献
14.
Graph transformation techniques, the Double-Pushout (DPO) approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we propose a theory of graph transformations for service programming with sophisticated features such as sessions and pipelines. Through graph representation of CaSPiS, a recently proposed process calculus, we show how graph transformations can cope with advanced features of service-oriented computing, such as several logical notions of scoping together with the interplay between linking and containment. We first exploit a graph algebra and set up a graph model that supports graph transformations in the DPO approach. Then, we show how to represent CaSPiS processes as hierarchical graphs in the graph model and their behaviors as graph transformation rules. Finally, we provide the soundness and completeness results of these rules with respect to the reduction semantics of CaSPiS. 相似文献
15.
Software engineering tools based on Graph Transformation techniques are becoming available, but their practical applicability is somewhat reduced by the lack of idioms and design patterns. Idioms and design patterns provide prototypical solutions for recurring design problems in software engineering, but their use can be easily extended into software development using graph transformation systems. In this paper we briefly present a simple graph transformation language: GReAT, and show how typical design problems that arise in the context of model transformations can be solved using its constructs. These solutions are similar to software design patterns, and intend to serve as the starting point for a more complete collection. 相似文献
16.
This paper takes first steps towards a formalization of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. Whereas graph rewriting is usually performed by mapping a pattern graph into a source graph by means of a graph morphism and then carrying out operations on the image node and edge set, this article generalises the notion of pattern graph to path expressions, which are formulae in a fragment of first-order logic. We examine the correspondence with traditional graph rewriting and show that this interpretation is beneficial when formally reasoning about model transformations with the aid of proof assistants. 相似文献
17.
Model-driven engineering (MDE) promotes the use of models throughout the software development cycle in order to increase abstraction and reduce software complexity. It favors the definition of domain-specific modeling languages (DSMLs) thanks to frameworks dedicated to meta-modeling and code generation like EMF (Eclipse Modeling Framework). The standard semantics of meta-models allows interoperability between tools such as language analysers (e.g., XText), code generators (e.g., Acceleo), and also model transformation tools (e.g., ATL). However, a major limitation of MDE is the lack of formal reasoning tools allowing to ensure the correctness of models. Indeed, most of the verification activities offered by MDE tools are based on the verification of OCL constraints on instances of meta-models. However, these constraints mainly deal with structural properties of the model and often miss out its behavioral semantics. In this work, we propose to bridge the gap between MDE and the rigorous world of formal methods in order to guarantee the correctness of both structural and behavioral properties of the model. Our approach translates EMF meta-models into an equivalent formal B specification and then injects models into this specification. The equivalence between the resulting B specification and the original EMF model is kept by proven design steps leading to a rigorous MDE technique. The AtelierB prover is used to guarantee the correctness of the model’s behavior with respect to its invariant properties, and the ProB model-checker is used to animate underlying execution scenarios which are translated back to the initial EMF model. Besides the use of these automatic reasoning tools in MDE, proved B refinements are also investigated in this paper in order to gradually translate abstract EMF models to concrete models which can then be automatically compiled into a programming language. 相似文献
18.
With model transformations becoming more widely used, there is an increasing need for approaches focussing on a systematic development of model transformations. Although a number of approaches for specifying model transformations exist, none of them focusses on systematically validating model transformations with respect to termination and confluence. Termination and confluence ensure that a model transformation always produces a unique result. Also called functionality, these properties are important requirements for practical applications of model transformations. In this paper, we introduce our approach to model transformation. Using and extending results from the theory of graph transformation, we investigate termination and confluence properties of model transformations specified in our approach. We establish a set of criteria for termination and confluence to be checked at design time by static analysis of the transformation rules and the underlying metamodels. Moreover, the criteria are formulated in such a way that they require less experience with the theory of graph transformation. Our concepts are illustrated by a running example of a model tranformation from statecharts to the process algebra Communicating Sequential Processes. 相似文献
19.
Algorithms designed for VLSI implementation are commonly described by directed graphs, in which the nodes represent functional units and the arcs indicate communication links. We give a denotational semantics for such a graph in terms of the least fixed point of a set of (mutually recursive) function definitions, describing the outputs produced at each node as a function of time. This semantics is consistent with the conventional clocked operational semantics of the system. A retiming is a systematic modification of the internode delays of a design, often used to convert an algorithm design into a systolic form. The utility of such retimings in optimizing the behavior of designs is well known. We use fixed-point semantics to provide simple proofs of the correctness of certain retiming transformations from the literature and to justify other design transformations such as pipelining. 相似文献
20.
In this paper we present case studies that describe how the graph transformation tool groove has been used to model problems from a wide variety of domains. These case studies highlight the wide applicability of groove in particular, and of graph transformation in general. They also give concrete templates for using groove in practice. Furthermore, we use the case studies to analyse the main strong and weak points of groove. 相似文献
|