共查询到20条相似文献,搜索用时 15 毫秒
1.
2.
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. 相似文献
3.
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. 相似文献
4.
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. 相似文献
5.
《Information and Software Technology》2013,55(11):1925-1947
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. 相似文献
6.
Jörg Becker Daniel F. Beverungen Ralf Knackstedt 《Information Systems and E-Business Management》2010,8(1):33-66
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. 相似文献
7.
《Information and Software Technology》2014,56(2):103-116
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. 相似文献
8.
An algebraic semantics for MOF 总被引:1,自引:0,他引:1
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. 相似文献
10.
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. 相似文献
11.
Verifying BPEL-like programs with Hoare logic 总被引:1,自引:0,他引:1
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. 相似文献
12.
13.
《Information and Software Technology》2013,55(2):365-394
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. 相似文献
14.
Discovering expressive process models by clustering log traces 总被引:5,自引:0,他引:5
Greco G. Guzzo A. Ponieri L. Sacca D. 《Knowledge and Data Engineering, IEEE Transactions on》2006,18(8):1010-1027
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. 相似文献
15.
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. 相似文献
16.
A semantic framework for metamodel-based languages 总被引:1,自引:0,他引:1
Angelo Gargantini Elvinia Riccobene Patrizia Scandurra 《Automated Software Engineering》2009,16(3-4):415-454
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. 相似文献
17.
18.
Specification-oriented semantics for Communicating Processes 总被引:4,自引:0,他引:4
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] 相似文献
19.
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
- • 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)
20.
Kathrin Figl Michael Derntl Manuel Caeiro Rodriguez Luca Botturi 《Journal of Visual Languages and Computing》2010,21(6):311-373
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 (E2ML, 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. 相似文献