Towards an Integrated Graph Based Semantics for UML

Recently, we proposed an integrated formal semantics based on graph transformation for central aspects of UML class, object and state diagrams. In this paper, we explain the basic ideas of that approach and show how two more UML diagram types, sequence and collaboration diagrams, can be captured. For UML models consisting of a class diagram and particular state diagrams, a graph transformation system can be defined. Its graphs are associated with system states and its rules with operations in the class diagram and transitions in the state diagrams. Sequence and collaboration diagrams then characterize sequences of operation applications and therefore sequences of transformation rule applications. Thus valid sequence and collaboration diagrams correspond to derivations induced by the graph transformation system. Proceeding this way, it can be checked for example whether such an operation application sequence may be applied in a specific system state.     

Dynamic Meta Modeling with time: Specifying the semantics of multimedia sequence diagrams

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.     

Specifying behavioral semantics of UML diagrams through graph transformations

The Unified Modeling Language (UML) has been widely accepted as a standard for modeling software systems from various perspectives. The intuitive notations of UML diagrams greatly improve the communication among developers. However, the lack of a formal semantics makes it difficult to automate analysis and verification. This paper offers a graphical yet formal approach to specifying the behavioral semantics of statechart diagrams using graph transformation techniques. It supports many advanced features of statecharts, such as composite states, firing priority, history, junction, and choice. In our approach, a graph grammar is derived automatically from a state machine to summarize the hierarchy of states. Based on the graph grammar, the execution of a set of non-conflict state transitions is interpreted by a sequence of graph transformations. This facilitates verifying a design model against system requirements. To demonstrate our approach, we present a case study on a toll-gate system.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

Dynamic Meta Modeling with Time: Specifying the Semantics of Multimedia Sequence Diagrams

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.     

A UML/OCL framework for the analysis of graph transformation rules

In this paper we present an approach for the analysis of graph transformation rules based on an intermediate OCL representation. We translate different rule semantics into OCL, together with the properties of interest (like rule applicability, conflicts or independence). The intermediate representation serves three purposes: (1) it allows the seamless integration of graph transformation rules with the MOF and OCL standards, and enables taking the meta-model and its OCL constraints (i.e. well-formedness rules) into account when verifying the correctness of the rules; (2) it permits the interoperability of graph transformation concepts with a number of standards-based model-driven development tools; and (3) it makes available a plethora of OCL tools to actually perform the rule analysis. This approach is especially useful to analyse the operational semantics of Domain Specific Visual Languages. We have automated these ideas by providing designers with tools for the graphical specification and analysis of graph transformation rules, including a back-annotation mechanism that presents the analysis results in terms of the original language notation.     

将UML模型转换成SDL模型的方法

提出了一种将UML模型转换成SDL模型的方法.UML是一种优秀的建模语言,使用UML可以为协议建立模型带来很多方便.但是,UML缺乏形式化语义,因此不能满足协议精确性的要求.SDL是一种用于通信软件规格的标准语言,它拥有形式化语义,而且有很多商业软件都支持它.在协议设计和开发中,将UML模型转换成SDL模型可以克服这样的缺点.通过为UML制作适当的profile,并制定严格的转换规则可以实现模型的转换.     

VPM: A visual,precise and multilevel metamodeling framework for describing mathematical domains and UML (The Mathematics of Metamodeling is Metamodeling Mathematics)

As UML 2.0 is evolving into a family of languages with individually specified semantics, there is an increasing need for automated and provenly correct model transformations that (i) assure the integration of local views (different diagrams) of the system into a consistent global view, and, (ii) provide a well-founded mapping from UML models to different semantic domains (Petri nets, Kripke automaton, process algebras, etc.) for formal analysis purposes as foreseen, for instance, in submissions for the OMG RFP for Schedulability, Performance and Time. However, such transformations into different semantic domains typically require the deep understanding of the underlying mathematics, which hinders the use of formal specification techniques in industrial applications. In the paper, we propose a multilevel metamodeling technique with precise static and dynamic semantics (based on a refinement calculus and graph transformation) where the structure and operational semantics of mathematical models can be defined in a UML notation without cumbersome mathematical formulae.     

UML Statecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.     

Extending C for Checking Shape Safety

The project Safe Pointers by Graph Transformation at the University of York has developed a method for specifying the shape of pointer-data structures by graph reduction, and a static checking algorithm for proving the shape safety of graph transformation rules modelling operations on pointer structures. In this paper, we outline how to apply this approach to the C programming language. We extend ANSI C with so-called transformers which model graph transformation rules, and with shape specifications for pointer structures. For the resulting language C-GRS, we present both a translation to C and and an abstraction to graph transformation. Our main result is that the abstraction of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation.     

Domain-specific discrete event modelling and simulation using graph transformation

Graph transformation is being increasingly used to express the semantics of domain-specific visual languages since its graphical nature makes rules intuitive. However, many application domains require an explicit handling of time to accurately represent the behaviour of a real system and to obtain useful simulation metrics to measure throughputs, utilization times and average delays. Inspired by the vast knowledge and experience accumulated by the discrete event simulation community, we propose a novel way of adding explicit time to graph transformation rules. In particular, we take the event scheduling discrete simulation world view and provide rules with the ability to schedule the occurrence of other rules in the future. Hence, our work combines standard, efficient techniques for discrete event simulation (based on the handling of a future event set) and the intuitive, visual nature of graph transformation. Moreover, we show how our formalism can be used to give semantics to other timed approaches and provide an implementation on top of the rewriting logic system Maude.     

一种基于规则的模型转换方法*

尽管模型驱动开发(MDD)代表软件工程的发展方向,但是目前MDD还缺乏一套完整的转换规则描述方法和相应的实现机制,难以实现模型的自动转换。为此定义了一个平台独立模型到平台相关模型的转换框架,采用UML活动图说明模型转换的实现机制;基于OCL定义了转换规则的表示法,并结合UML模型到Java模型的转换给出了转换规则的定义。最后在一个具体的实例中验证了此方法的合理性和易用性。     

Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification

UML 2.X sequence diagrams(SD)are among privileged scenarios-based approaches dealing with the complexity of modeling the behaviors of some current systems.However,there are several issues related to the standard semantics of UML 2.X SD proposed by the Object Management Group(OMG).They mainly concern ambiguities of the interpretation of SDs,and the computation of causal relations between events which is not specifically laid out.Moreover,SD is a semi-formal language,and it does not support the verification of the modeled system.This justifies the considerable number of research studies intending to define formal semantics of UML SDs.We proposed in our previous work semantics covering the most popular combined fragments(CF)of control-flow ALT,OPT,LOOP and SEQ,allowing to model alternative,optional,iterative and sequential behaviors respectively.The proposed semantics is based on partial order theory relations that permit the computation of the precedence relations between the events of an SD with nested CFs.We also addressed the issue of the evaluation of the interaction constraint(guard)for guarded CFs,and the related synchronization issue.In this paper,we first extend our semantics,proposed in our previous work;indeed,we propose new rules for the computation of causal relations for SD with PAR and STRICT CFs(dedicated to modeling concurrent and strict behaviors respectively)as well as their nesting.Then,we propose a transformational semantics in Event-B.Our modeling approach emphasizes computation of causal relations,guard handling and transformational semantics into Event-B.The transformation of UML 2.X SD into the formal method Event-B allows us to perform several kinds of verification including simulation,trace acceptance,verification of properties,and verification of refinement relation between SDs.     

A component framework for system modeling based on high-level replacement systems

The aim of this paper is to present a generic component framework for system modeling that satisfies main requirements for component-based development in software engineering. In this sense, we have defined a framework that can be used, by providing an adequate instantiation, in connection with a large class of semi-formal and formal modeling techniques. Moreover, the framework is also flexible with respect to the connection of components, providing a compositional semantics of components. This means more precisely that the semantics of a system can be inferred from the semantics of its components. In contrast to other component concepts for data type specification techniques, our component framework is based on a generic notion of transformations. In particular, refinements and transformations are used to express intradependencies, between the export interface and the body of a component, and interdependencies, between the import and the export interfaces of different components. The generic component framework generalizes module concepts for different kinds of Petri nets and graph transformation systems proposed in the literature, and seems to be also suitable for visual modeling techniques, including parts of the UML, if these techniques provide a suitable refinement or transformation concept. In this paper the generic approach is instantiated in two steps. First to high-level replacement systems generalizing the transformation concept of graph transformations. In a second step it is further instantiated to low-level and high-level Petri nets. To show applicability we present sample components from a case study in the domain of production automation as proposed in a priority program of the German Research Council (DFG).     

基于上下文的异构文档类型定义匹配

XML文档的模式匹配是许多应用中的重要步骤．提出一种匹配算法来发现不同DTD中对应的元素和属性，通过转化规则将DTD转化成一个有向图模型，先给出了两个DTD树之间的匹配算法，然后将其推广一般的DTD图匹配的情形．匹配算法中在考察DTD节点的相似性时，除考虑标签语义和基数约束之外，研究了上下文语义对节点相似性的影响．     

A sound and complete theory of graph transformations for service programming with sessions and pipelines

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.     

UML活动图的操作语义

越来越多的系统采用UML（unified model language,统一建模语言）作为建模语言来进行系统分析和设计.UML活动图是UML语言中描述系统动态行为的一种方法,它广泛地运用于业务建模.由于UML活动图缺乏精确的动态语义,所以不利于对其所描述的系统进行形式化的分析、验证和确认.为解决这一问题,根据UML1.5语义文档,给出UML活动图的形式化操作语义.首先给出UML活动图的形式化的语法,然后详细地定义了活动图的格局和变迁,最后基于LTS给出了活动图的演绎规则.主要工作是：引入状态包的概念,使得描述更加清楚、完善;通过LTS定义活动图的操作语义,并详细阐述演绎规则,从而获得活动图的全局状态转移图,使定义的操作语义很容易地应用到形式化验证中.该语义覆盖了UML活动图的绝大部分特征,为对UML活动图进行模型检验奠定了基础.     

一种基于UML关系的Java代码库构造方法

关系信息是体现代码结构和语义的最重要的一类信息,如继承、聚合、组合、依赖、调用和创建实例等。为了更好地支持开源代码的理解与复用,提出了一种基于UML2关系的代码库构造方法。它以图数据库为实现平台,采用语言工程中经典的抽象语法树作为基础,并针对Java语言的特性和机制,设计富语义的Java代码属性图数据模型,在此基础上使得Java代码的图结构持久化。同时,为了屏蔽各种编程语言社区对代码中关系信息理解的差异性,采用UML2.4国际标准版本中定义的关系类型及语义解释,设计相应的代码关系抽取算法,为图节点添加对应的关系边。针对代码图化后的膨胀及代码库的空间存储消耗情况,选取9个常见的开源项目进行了实验评估。最后,给出了基于此代码库的查询应用实例。