Incremental execution of rule-based model transformation

When model transformations are used to implement consistency relations between very large models, incrementality plays a cornerstone role in detecting and resolving inconsistencies efficiently when models are updated. Given a directed consistency relation between two models, the problem studied in this work consists in propagating model changes from a source model to a target model in order to ensure consistency while minimizing computational costs. The mechanism that enforces such consistency is called consistency maintainer and, in this context, its scalability is a required non-functional requirement. State-of-the-art model transformation engines with support for incrementality normally rely on an observer pattern for linking model changes, also known as deltas, to the application of model transformation rules, in so-called dependencies, at run time. These model changes can then be propagated along an already executed model transformation. Only a few approaches to model transformation provide domain-specific languages for representing and storing model changes in order to enable their use in asynchronous, event-based execution environments. The principal contribution of this work is the design of a forward change propagation mechanism for incremental execution of model transformations, which decouples dependency tracking from change propagation using two innovations. First, the observer pattern-based model is replaced with dependency injection, decoupling domain models from consistency maintainers. Second, a standardized representation of model changes is reused, enabling interoperability with EMF-compliant tools, both for defining model changes and for processing them asynchronously. This procedure has been implemented in a model transformation engine, whose performance has been evaluated experimentally using the VIATRA CPS benchmark. In the experiments performed, the new transformation engine shows gains in the form of several orders of magnitude in the initial phase of the incremental execution of the benchmark model transformation and change propagation is performed in real time for those model sizes that are processable by other tools and, in addition, is able to process much larger models.

     

A case study on consistency management of business and IT process models in banking

Organizations that adopt process modeling often maintain several co-existing models of the same business process. These models target different abstraction levels and stakeholder perspectives. Maintaining consistency among these models has become a major challenge for such organizations. Although several academic works have discussed this challenge, little empirical investigation exists on how people perform process model consistency management in practice. This paper aims to address this lack by presenting an in-depth empirical study of a business-driven engineering process deployed at a large company in the banking sector. We analyzed more than 70 business process models developed by the company, including their change history, with over 1,000 change requests. We also interviewed 9 business and IT practitioners and surveyed 23 such practitioners to understand concrete difficulties in consistency management, the rationales for the specification-to-implementation refinements found in the models, strategies that the practitioners use to detect and fix inconsistencies, and how tools could help with these tasks. Our contribution is a set of eight empirical findings, some of which confirm or contradict previous works on process model consistency management found in the literature. The findings provide empirical evidence of (1) how business process models are created and maintained, including a set of recurrent patterns used to refine business-level process specifications into IT-level models; (2) what types of inconsistencies occur; how they are introduced; and what problems they cause; and (3) what stakeholders expect from tools to support consistency management.     

Predicate diagrams for the verification of real-time systems

This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems that are defined as extended timed graphs, a format that combines timed automata and constructs for modelling data, possibly over infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean abstractions. They also represent an interface between deductive tools used to establish the correctness of an abstraction, and model checking tools that can verify behavioral properties of finite-state models. The contribution of this article is to extend the format of predicate diagrams to timed systems. We establish a set of verification conditions that are sufficient to prove that a given predicate diagram is a correct abstraction of an extended timed graph; these verification conditions can often be discharged with SMT solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer’s real-time mutual-exclusion protocol.     

基于锁增广分段图的多线程程序死锁检测

死锁是并行程序常见的缺陷之一,动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而,锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行,扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息,分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关系.上述问题导致了多种死锁...     

Integration verteilter Produktmodelle durch Semantic-Web-Technologien

Product development is the most knowledge intensive business process in industry. Product models have a special role in supporting knowledge and information exchange. Interdisciplinary engineering processes and distributed tools generate distributed and heterogeneous product models with numerous internal dependencies and relationships. Neither Knowledge Management Systems nor Product Life Cycle Management Systems support the maintenance of these relationships sufficiently today. This paper suggests an approach to describe and manage internal relationships of the product model and to ensure its consistency by using Semantic Web technologies. Ontologies are applied to specify the relationships semantically.     

Using graph rewriting methods for the semi-automatic generation of parametric infrastructure models

For the design of large infrastructure projects such as inner-city subway tracks, it proves necessary to consider differing model scales, ranging from the scale of several kilometers down to a few millimeters. This challenge can be addressed by using multi-scale product models comprising multiple levels of detail (LoD). Ensuring consistency across the different LoDs can be achieved by applying procedural and parametric modeling techniques while creating the model. This results in a flexible multi-scale model that can be easily modified on one scale while other scales are automatically updated. However, the correct application of parametric constraints and procedural dependencies has shown to be a very complex and time-consuming process. To address this issue, this papers presents a semi-automated detailing mechanism, which is based on formal procedures based on graphs and graph transformations. This paper discusses how procedural parametric models based on two-dimensional sketches can be represented by graphs and how detailing steps in the form of parametric modeling operations can be formalized by using rule-based graph rewriting.     

一种并发程序依赖性分析方法

并发程序的依赖性分析是并发程序分析，理解，调试，测试和维护的重要手段，由于并发程序执行的不确定性，目前，尚有很多难点有待解决，针对Ada任务机制，首先提出了一种简洁，有效的并发程序表示方法－并发程序流图，然后讨论了由任务间同步引起的同步依赖和由访问共享变量引起的任务数据依赖，建立了并发程序依赖图，并在此基础上给出了一种有效的并发程序依赖性分析算法，得到一个比较精确的依赖性，较好地解决了并发程序依赖关系不可传递性问题。     

CODE: a unified approach to parallel programming

The authors describe CODE (computation-oriented display environment), which can be used to develop modular parallel programs graphically in an environment built around fill-in templates. It also lets programs written in any sequential language be incorporated into parallel programs targeted for any parallel architecture. Broad expressive power was obtained in CODE by including abstractions of all the dependency types that occur in the widely used parallel-computation models and by keeping the form used to specify firing rules general. The CODE programming language is a version of generalized dependency graphs designed to encode the unified parallel-computation model. A simple example is used to illustrate the abstraction level in specifying dependencies and how they are separated from the computation-unit specification. The most important CODE concepts are described by developing a declarative, hierarchical program with complex firing rules and multiple dependency types     

Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars

Building verified compilers is difficult, especially when complex analyses such as type checking or data-flow analysis must be performed. Both the type checking and program optimization communities have developed methods for proving the correctness of these processes and developed tools for using, respectively, verified type systems and verified optimizations. However, it is difficult to use both of these analyses in a single declarative framework since these processes work on different program representations: type checking on abstract syntax trees and data-flow analysis-based optimization on control flow or program dependency graphs.We present an attribute grammar specification language that has been extended with constructs for specifying attribute-labelled control flow graphs and both CTL and LTL-FV formulas that specify data-flow analyses. These formulas are model-checked on these graphs to perform the specified analyses. Thus, verified type rules and verified data-flow analyses (verified either by hand or with automated proof tools) can both be transcribed into a single declarative framework based on attribute grammars to build a high-confidence language implementations. Also, the attribute grammar specification language is extensible so that it is relatively straight-forward to add new constructs for different temporal logics so that alternative logics and model checkers can be used to specify data-flow analyses in this framework.     

TracED: A tool for capturing and tracing engineering design processes

The design of products or production processes in many engineering disciplines such as chemical, or software engineering, involves many creative and sometimes unstructured activities, with an opportunistic control flow. During these design processes, several models are generated, which have different levels of abstraction of the object being designed. Given the difficulties in dealing with this complexity using an improvised way, there is an urgent need for tools that support the capture and tracing of this process. In this proposal, TracED, a computational environment to support the capture and tracing of engineering design process is presented. It allows defining a particular engineering design domain and supporting the capture of how products under development are transformed along an engineering design process. Particularly, in this work, we consider software architectures design domain. As in any complex process, the support of computational tools is required for enabling its capture.     

图依赖研究与应用综述

图依赖是用于解决图数据的数据一致性问题的数据质量规则。基于图依赖提升数据一致性的过程通常分为图依赖定义与形式化、图依赖自动挖掘、基于图依赖的数据一致性提升三步。介绍了针对数据一致性的图依赖理论,并根据拓展类型将图依赖分为基于结构约束拓展、基于语义约束拓展和基于外部约束拓展的图依赖;综述并对比了从图数据中自动挖掘图依赖及其拓展的算法;分析了应用图依赖提高数据一致性的研究现状;总结了当前研究中仍存在的问题,并依据问题展望了图依赖在数据质量领域的应用前景。     

Coupling Use Cases and Class Models as a Means for Validation and Verification of Requirements Specifications

In many applications, especially from the business domain, the requirements specification mainly deals with use cases and class models. Unfortunately, these models are based on different modelling techniques and aim at different levels of abstraction, such that serious consistency and completeness problems are induced. To overcome these deficiencies, we refine activity graphs to meet the needs for a suitable modelling element for use case behaviour. The refinement in particular supports the proper coupling of use cases via activity graphs and the class model. The granularity and semantics of our approach allow for a seamless, traceable transition of use cases to the class model and for the verification of the class model against the use case model. The validation of the use case model and parts of the class model is supported as well. Experience from several applications has shown that the investment in specification, validation and verification not only pays off during system and acceptance testing but also significantly improves the quality of the final product.       

Design for service compatibility

Service composition is a recent field that has seen a flurry of different approaches proposed towards the goal of flexible distributed heterogeneous interoperation of software systems, usually based on the expectation that such systems must be derived from higher-level models rather than be coded at low level. In practice, achieving service interoperability nonetheless continues to require significant modelling approach at multiple abstraction levels, and existing formal approaches typically require the analysis of the global space of joint executions of interacting services. Based on our earlier work on providing locally checkable consistency rules for guaranteeing the behavioural consistency of inheritance hierarchies, a model-driven approach for creating consistent service orchestrations is proposed. Service execution and interaction is represented with a high-level model in terms of extended Petri net notation; formal criteria are provided for service consistency that can be checked in terms of local model properties, and give a multi-step design approach for developing services that are guaranteed to be interoperable. Finally, it is outlined how the presented results can be carried over and applied to modelling processes using the Business Process Modelling Notation (BPMN).     

Verification of workflow nets with transition conditions

Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.     

Anytime search in dynamic graphs

Agents operating in the real world often have limited time available for planning their next actions. Producing optimal plans is infeasible in these scenarios. Instead, agents must be satisfied with the best plans they can generate within the time available. One class of planners well-suited to this task are anytime planners, which quickly find an initial, highly suboptimal plan, and then improve this plan until time runs out.A second challenge associated with planning in the real world is that models are usually imperfect and environments are often dynamic. Thus, agents need to update their models and consequently plans over time. Incremental planners, which make use of the results of previous planning efforts to generate a new plan, can substantially speed up each planning episode in such cases.In this paper, we present an A^∗-based anytime search algorithm that produces significantly better solutions than current approaches, while also providing suboptimality bounds on the quality of the solution at any point in time. We also present an extension of this algorithm that is both anytime and incremental. This extension improves its current solution while deliberation time allows and is able to incrementally repair its solution when changes to the world model occur. We provide a number of theoretical and experimental results and demonstrate the effectiveness of the approaches in a robot navigation domain involving two physical systems. We believe that the simplicity, theoretical properties, and generality of the presented methods make them well suited to a range of search problems involving dynamic graphs.     

一种并行化的启发式流程挖掘算法

启发式流程挖掘算法在日志噪音与不完备日志的处理方面优势显著,但是现有算法对长距离依赖关系以及2-循环特殊结构的处理存在不足,而且算法未进行并行化处理.针对上述问题,基于执行任务集将流程模型划分为多个案例模型,结合改进的启发式算法并行挖掘各个案例模型所对应的C-net模型;再将上述模型集成得到完整流程对应的C-net.同时,将长距离依赖关系扩展为决策点处两个任务子集之间的非局部依赖关系,给出了更为准确的长距离依赖关系度量指标和挖掘算法.上述改进措施使得该算法更为精确、高效.     

Response to Jiau et al.'s comments

The consistency problems in UML models and related software processes can be very complex. First, although UML supports a modeling process that should yield inter and intraconsistent models, the meaning of the UML dependencies and their specializations is not precisely defined and, for this reason, many inconsistencies may appear in their models and processes. Precise definitions would form a basis for methods to detect and analyze consistency problems related to UML dependencies and relationships, as well as problems related to software processes described in UML. In addition, we are using the UML object constraint language (OCL) to describe constraints related to the framework instantiation process. OCL is recognized as a limited language in some aspects for expressing well-formedness rules. We have presented a method (T.C. Oliveira et al., 2004) that works in the case of consistent rules and consistent instantiation processes.