基于过程模型的工作流执行语义研究

针对现有工作流建模语言难以兼顾语言的可理解性、执行语义的形式化和描述维度的单一性等问题,提出利用可视化的过程模型作为工作流建模语言。过程模型能从过程、数据、资源、组织等多个角度描述企事业的业务工作流程。根据过程模型的语法和工作流系统的特点,定义形式化执行语义,为过程模型的分析、验证和执行提供理论依据。     

Clafer: unifying class and feature modeling

We present Clafer (class, feature, reference), a class modeling language with first-class support for feature modeling. We designed Clafer as a concise notation for meta-models, feature models, mixtures of meta- and feature models (such as components with options), and models that couple feature models and meta-models via constraints (such as mapping feature configurations to component configurations or model templates). Clafer allows arranging models into multiple specialization and extension layers via constraints and inheritance. We identify several key mechanisms allowing a meta-modeling language to express feature models concisely. Clafer unifies basic modeling constructs, such as class, association, and property, into a single construct, called clafer. We provide the language with a formal semantics built in a structurally explicit way. The resulting semantics explains the meaning of hierarchical models whereby properties can be arbitrarily nested in the presence of inheritance and feature modeling constructs. The semantics also enables building consistent automated reasoning support for the language: To date, we implemented three reasoners for Clafer based on Alloy, Z3 SMT, and Choco3 CSP solvers. We show that Clafer meets its design objectives using examples and by comparing to other languages.     

Semantische Prozessmodellierung – Konzeption und informationstechnische Unterstützung einer ontologiebasierten Repräsentation von Geschäftsprozessen

An extension of process modeling languages is designed which allows representing the semantics of model element labels which are formulated in natural language by using concepts of a formal ontology. This combination of semiformal models with formal ontologies will be characterized as semantic process modeling. The approach is exemplarily applied to the languages EPC (Event-driven Process Chain), BPMN (Business Process Modeling Notation) and OWL (Web Ontology Language) and is generalized by means of an information model. The proposed formalization of the semantics of individual model elements in conjunction with the usage of inference engines allows the improvement of query functionalities in modeling tools and enables new possibilities of model validation. The integration of the approach in the IT-based work environments of modelers is demonstrated by a system architecture and a prototypical implementation. Evidently, advantages in the areas of modeling, model management, business/IT alignment, and compliance can be achieved by the application of modeling tools augmented with semantic technologies.     

PSL: A semantic domain for flow models

Flow models underlie popular programming languages and many graphical behavior specification tools. However, their semantics is typically ambiguous, causing miscommunication between modelers and unexpected implementation results. This article introduces a way to disambiguate common flow modeling constructs, by expressing their semantics as constraints on runtime sequences of behavior execution. It also shows that reduced ambiguity enables more powerful modeling abstractions, such as partial behavior specifications. The runtime representation considered in this paper uses the Process Specification Language (PSL), which is defined in first-order logic, making it amenable to automated reasoning. The activity diagrams of the Unified Modeling Language are used for example flow models.     

A formal framework for software product lines

ContextA Software Product Line is a set of software systems that are built from a common set of features. These systems are developed in a prescribed way and they can be adapted to fit the needs of customers. Feature models specify the properties of the systems that are meaningful to customers. A semantics that models the feature level has the potential to support the automatic analysis of entire software product lines.ObjectiveThe objective of this paper is to define a formal framework for Software Product Lines. This framework needs to be general enough to provide a formal semantics for existing frameworks like FODA (Feature Oriented Domain Analysis), but also to be easily adaptable to new problems.MethodWe define an algebraic language, called SPLA, to describe Software Product Lines. We provide the semantics for the algebra in three different ways. The approach followed to give the semantics is inspired by the semantics of process algebras. First we define an operational semantics, next a denotational semantics, and finally an axiomatic semantics. We also have defined a representation of the algebra into propositional logic.ResultsWe prove that the three semantics are equivalent. We also show how FODA diagrams can be automatically translated into SPLA. Furthermore, we have developed our tool, called AT, that implements the formal framework presented in this paper. This tool uses a SAT-solver to check the satisfiability of an SPL.ConclusionThis paper defines a general formal framework for software product lines. We have defined three different semantics that are equivalent; this means that depending on the context we can choose the most convenient approach: operational, denotational or axiomatic. The framework is flexible enough because it is closely related to process algebras. Process algebras are a well-known paradigm for which many extensions have been defined.     

The challenge of conceptual modeling for product–service systems: status-quo and perspectives for reference models and modeling languages

Confronted with decreasing margins and a rising customer demand for integrated solutions, manufacturing companies integrate complementary services into their portfolio. Offering value bundles (consisting of services and physical goods) takes place in integrated product–service systems, spanning the coordinated design and delivery of services and physical goods for customers. Conceptual Modeling is an established approach to support and guide such efforts. Using a framework for the design and delivery of value bundles as an analytical lens, this study evaluates the current support of reference models and modeling languages for setting up conceptual models for an integrated design and delivery of value bundles. Consecutively, designing modeling languages and reference models to fit the requirements of conceptual models in product–service systems are presented as upcoming challenges in Service Research. To guide further research, first steps are proposed by exemplarily integrating reference models and modeling languages stemming from the service and manufacturing domains.     

Software process modeling languages: A systematic literature review

ContextOrganizations working in software development are aware that processes are very important assets as well as they are very conscious of the need to deploy well-defined processes with the goal of improving software product development and, particularly, quality. Software process modeling languages are an important support for describing and managing software processes in software-intensive organizations.ObjectiveThis paper seeks to identify what software process modeling languages have been defined in last decade, the relationships and dependencies among them and, starting from the current state, to define directions for future research.MethodA systematic literature review was developed. 1929 papers were retrieved by a manual search in 9 databases and 46 primary studies were finally included.ResultsSince 2000 more than 40 languages have been first reported, each of which with a concrete purpose. We show that different base technologies have been used to define software process modeling languages. We provide a scheme where each language is registered together with the year it was created, the base technology used to define it and whether it is considered a starting point for later languages. This scheme is used to illustrate the trend in software process modeling languages. Finally, we present directions for future research.ConclusionThis review presents the different software process modeling languages that have been developed in the last ten years, showing the relevant fact that model-based SPMLs (Software Process Modeling Languages) are being considered as a current trend. Each one of these languages has been designed with a particular motivation, to solve problems which had been detected. However, there are still several problems to face, which have become evident in this review. This let us provide researchers with some guidelines for future research on this topic.     

An algebraic semantics for MOF

In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the meta-object facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions: metamodel, model, and conformance of a model to its metamodel. Furthermore, by using the Maude language, which directly supports mel specifications, this formal semantics is executable. This executable semantics has been integrated within the Eclipse modeling framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for model-driven development processes.     

Towards Symbolic Analysis of Visual Modeling Languages

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture the operational semantics of modeling languages based on metamodeling techniques as demonstrated by benchmark applications focusing on the formal treatment of the Unified Modeling Language (UML). In the paper, we enable model checking-based symbolic verification for such modeling languages by providing a meta-level transformation of well-formed model instances into SAL specifications [4]. We also discuss several optimizations in the translation process that makes our approach efficient and independent of the SAL framework.     

Verifying BPEL-like programs with Hoare logic

The WS-BPEL language has recently become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many recent works have mainly focused on formal semantic models for WS-BPEL. In this paper, we make one step forward by investigating the verification problem for business processes written in BPEL-like languages. We propose a set of proof rules in Hoare-logic style as an axiomatic verification system for a BPEL-like core language containing key features such as data states, fault and compensation handling. We also propose a big-step operational semantics which incorporates all these key features. Our verification rules are proven sound with respect to this underlying semantics. The application of the verification rules is illustrated via the proof search process for a nontrivial example.     

A visual token-based formalization of BPMN 2.0 based on in-place transformations

ContextThe Business Process Model and Notation (BPMN) standard informally defines a precise execution semantics. It defines how process instances should be updated in a model during execution. Existing formalizations of the standard are incomplete and rely on mappings to other languages.ObjectiveThis paper provides a BPMN 2.0 semantics formalization that is more complete and intuitive than existing formalizations.MethodThe formalization consists of in-place graph transformation rules that are documented visually using BPMN syntax. In-place transformations update models directly and do not require mappings to other languages. We have used a mature tool and test-suite to develop a reference implementation of all rules.ResultsOur formalization is a promising complement to the standard, in particular because all rules have been extensively verified and because conceptual validation is facilitated (the informal semantics also describes in-place updates).ConclusionSince our formalization has already revealed problems with the standard and since the BPMN is still evolving, the maintainers of the standard can benefit from our results. Moreover, tool vendors can use our formalization and reference implementation for verifying conformance to the standard.     

Discovering expressive process models by clustering log traces

Process mining techniques have recently received notable attention in the literature; for their ability to assist in the (re)design of complex processes by automatically discovering models that explain the events registered in some log traces provided as input. Following this line of research, the paper investigates an extension of such basic approaches, where the identification of different variants for the process is explicitly accounted for, based on the clustering of log traces. Indeed, modeling each group of similar executions with a different schema allows us to single out "conformant" models, which, specifically, minimize the number of modeled enactments that are extraneous to the process semantics. Therefore, a novel process mining framework is introduced and some relevant computational issues are deeply studied. As finding an exact solution to such an enhanced process mining problem is proven to require high computational costs, in most practical cases, a greedy approach is devised. This is founded on an iterative, hierarchical, refinement of the process model, where, at each step, traces sharing similar behavior patterns are clustered together and equipped with a specialized schema. The algorithm guarantees that each refinement leads to an increasingly sound mDdel, thus attaining a monotonic search. Experimental results evidence the validity of the approach with respect to both effectiveness and scalability.     

ODM: An object oriented data model

ODM is a new data model thatintegrates the features of object oriented programming languages (e.g. Smalltalk-80) and Relational Data Model (RDM). It extends the data structures and operations of RDM and also provides the features of object oriented programming such as improved semantics, data abstraction, reusability of data structures and codes, and extensibility. We have introduced the concept of ‘u-set’ (uniform set) as an extension of relation of RDM. We employ messages to define an extension of RDM attributes and tuples. Definition of classes for databases, u-sets, and tuples allows us to define new (or modify existing) operations for the databases, u-sets, or tuples. Each database and its elements are u-sets.     

A semantic framework for metamodel-based languages

In the model-based development context, metamodel-based languages are increasingly being defined and adopted either for general purposes or for specific domains of interest. However, meta-languages such as the MOF (Meta Object Facility)—combined with the OCL (Object Constraint Language) for expressing constraints—used to specify metamodels focus on structural and static semantics but have no built-in support for specifying behavioral semantics. This paper introduces a formal semantic framework for the definition of the semantics of metamodel-based languages. Using metamodelling principles, we propose several techniques, some based on the translational approach while others based on the weaving approach, all showing how the Abstract State Machine formal method can be integrated with current metamodel engineering environments to endow language metamodels with precise and executable semantics. We exemplify the use of our semantic framework by applying the proposed techniques to the OMG metamodelling framework for the behaviour specification of the Finite State Machines provided in terms of a metamodel.     

Specification-oriented semantics for Communicating Processes

Summary A process P satisfies a specification S if every observation we can make of the behaviour of P is allowed by S. We use this idea of process correctness as a starting point for developing a specific form of denotational semantics for processes, called here specification — oriented semantics. This approach serves as a uniform framework for generating and relating a series of increasingly sophisticated denotational models for Communicating Processes. These models differ in the underlying structure of their observations which influences both the number of representable language operators and the induced notion of process correctness. Safety properties are treated by all models; the more sophisticated models also permit proofs of certain liveness properties. An important feature of the models is a special hiding operator which abstracts from internal process activity. This allows large processes to be composed hierarchically from networks of smaller ones in such a way that proofs of the whole are constructed from proofs of its components. We also show the consistency of our denotational models w.r.t. a simple operational semantics based on transitions which make internal process activity explicit. A preliminary version of this paper appeared in [42]     

Preface: UNIGRA''03 - Uniform Approaches to Graphical Process Specification Techniques

This volume contains selected papers of the proceedings of the workshop on Uniform Approaches to Graphical Process Specification Techniques (UNIGRA'03). The workshop was held in Warsaw, Poland, on April 5 and 6, 2003, as a satellite event of the sixth European Joint Conference on Theory and Practice of Software (ETAPS 2003). The workshop continues the UNIGRA workshop in 2001 which has been a successful satellite event of ETAPS 2001.Workshop ObjectivesDue to the increasing amount of divergent formalisms, the main idea of the UNIGRA workshops is to bring together people working especially in the following three areas:

• Low Level and High-Level Petri Nets

• Graph Transformation and High-Level Replacement Systems

• Visual Modeling Techniques including UML

In each of these areas there is a large variety of different approaches, however, first attempts for uniform approaches have been made already. According to the main idea and in order to further stimulate the research in this important area, this volume presents some uniform approaches and further introduce unifying and comparative studies across the borders of the three and related areas.Workshop ProgramIn the first part, unifying approaches for low-level and high-level Petri nets are proposed:The contribution by Ehrig shows how the notions occurrence net and process can be generalized from low-level to high-level Petri nets, and studies the behavior and instantiations of this new view of processes for high-level nets.In his overview on new developments in the area of Petri net transformations for Software Engineering, Urbášek presents recent work on net model transformations and net class transformations. Both kinds of transformations are studied with regard to the preservation of system properties such as safety properties or liveness. The formalization of Petri net transformations is originally based on the theory of graph transformation.Padberg considers a case study (the call center of a phone company)which is modeled using Petri net modules for structuring the operational behavior of the system. The notion of Petri net modules was achieved by a transfer from the concepts of algebraic module specifications to the modeling of component-based systems by Petri nets.Desel, Juhás and Lorenz deal with the semantics of place/transition nets. The authors relate the process semantics based on partial orders (individual token semantics) to the collective token semantics by defining partial orders associated to process terms of place/transition nets.In the second part concerning graph transformation and high-level replacement systems, new aspects of component modeling and application of graph transformation techniques are discussed:In their contribution on components for algebra transformation systems, Ehrig and Orejas define a component transformation semantics in terms of the semantics of the specifications included in the components. The underlying formal basis of the instantiation of their generic component framework are algebra transformation systems and high-level replacement rules.An application of the formal unifying framework of distributed transformation units is presented by Kuske and Knirsch. The authors illustrate how different features of agent systems can be modeled by distributed graph transformation systems in a uniform way.Another application for graph rewriting, presented by Van Eetvelde and Janssens, is the modeling of refactoring operations for programs. The authors propose a hierarchical graph representation for programs to facilitate the study of refactoring operation effects at class level.The third part contains contributions focusing on unifying concepts for visual modeling techniques including UML:Minas describes a graphical specification tool for DIAGEN, a diagram editor generator based on hypergraph transformation. The specification tool simplifies the specification and generation of diagram editors. It uses an XML-based specification language and comes with a generic XML editor.In his contribution on dynamic aspects of visual modeling languages, Bottoni proposes an approach to the definition of the syntax and semantics of visual languages based on a notion of transition of production/consumption of resources. Abstract meta-models for this notion of transition are presented.An approach to the model-based verification and validation of properties of UML models is presented by Engels, Kïster, Heckel and Lohmann. The authors use graph transformation techniques as a meta-language for the translation and analysis of models.In model-driven architectures, the problem arises to deal with multiple models. Kent and Smith focus in their contribution on bidirectional mappings between models for software requirements and models for software design as basis for tools checking model traceability and consistency.Program CommitteeThe following program committee of UNIGRA'03 has given valuable scientific support:

• Hartmut Ehrig (TU Berlin, Germany) [chair]

• Roswitha Bardohl (TU Berlin, Germany) [co-chair]

• Luciano Baresi (University of Milano, Italy)

• Paolo Bottoni (University of Pisa, Italy)

• Claudia Ermel (TU Berlin, Germany)

• Reiko Heckel (University of Paderborn, Germany)

• Dirk Janssens (University of Antwerp, Belgium)

• Stuart Kent (University of Kent, Great Britain)

• Hans-Jörg Kreowski (University of Bremen, Germany)

• Fernando Orejas (University of Catalunya, Espania)

• Julia Padberg (University of Bremen, Germany)

• Grzegorz Rozenberg (University of Leiden, The Netherlands)

AcknowledgementThis workshop is supported by the European research training network SegraVis, and by the steering committee of the International Conference on Graph Transformation (ICGT).June 2003, Roswitha Bardohl and Hartmut Ehrig     

Cognitive effectiveness of visual instructional design languages

The introduction of learning technologies into education is making the design of courses and instructional materials an increasingly complex task. Instructional design languages are identified as conceptual tools for achieving more standardized and, at the same time, more creative design solutions, as well as enhancing communication and transparency in the design process. In this article we discuss differences in cognitive aspects of three visual instructional design languages (E²ML, PoEML, coUML), based on user evaluation. Cognitive aspects are of relevance for learning a design language, creating models with it, and understanding models created using it. The findings should enable language constructors to improve the usability of visual instructional design languages in the future. The paper concludes with directions with regard to how future research on visual instructional design languages could strengthen their value and enhance their actual use by educators and designers by synthesizing existing efforts into a unified modeling approach for VIDLs.