Search

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The relational logic based specification language Alloy and its accompanying tool the Alloy Analyzer have been used in the past to validate properties of model transformations. However Alloy based analysis of transformations suffers from several limitations. On one hand, it is time consuming and does not scale well. On the other hand, the reliance on Alloy, being a formal method, prevents the effective involvement of domain experts in the validation process which is crucial for pinpointing domain pertinent errors. Those limitations are even more severe when it comes to transformations whose input and/or output are themselves transformations (called compound transformations) because they are inherently more complex. To tackle the performance and scalability limitations, in previous work, we proposed an Alloy-based Domain Specific Language (DSL), called F-Alloy, that is tailored for model transformation specifications. Instead of pure analysis based validation, F-Alloy speeds up the validation of model transformations by applying a hybrid strategy that combines analysis with interpretation. In this paper, we formalize the notion of “hybrid analysis” and further extended it to also support efficient validation of compound transformations. To enable the effective involvement of domain experts in the validation process, we propose in this paper a new approach to model transformation validation, called Visualization-Based Validation (briefly VBV). Following VBV, representative instances of a to-be-validated model transformation are automatically generated by hybrid analysis and shown to domain experts for feedback in a visual notation that they are familiar with. We prescribe a process to guide the application of VBV to model transformations and illustrate it with a benchmark model transformation. [ABSTRACT FROM AUTHOR]

Today, service compositions often need to be assembled or changed on-the-fly, which leaves only little time for quality assurance. Moreover, quality assurance is complicated by service providers only giving information on their services in terms of domain specific concepts with only limited semantic meaning. In this paper, we propose a method for constructing service compositions based on pre-verified templates . Templates, given as workflow descriptions, are typed over a (domain-independent) template ontology defining concepts and predicates. Their meaning is defined by an abstract semantics , leaving the specific meaning of ontology concepts open, however, only up to given ontology rules . Templates are proven correct using a Hoare-style proof calculus, extended by a specific rule for service calls. Construction of service compositions amounts to instantiation of templates with domain-specific services. Correctness of an instantiation can then simply be checked by verifying that the domain ontology (a) adheres to the rules of the template ontology, and (b) fulfills the constraints of the employed template. [ABSTRACT FROM AUTHOR]

We present Stipula , a domain specific language that may assist legal practitioners in programming legal contracts through specific patterns. The language is based on a small set of programming abstractions that correspond to common patterns in legal contracts. We illustrate the language by means of two paradigmatic legal contracts: a bike rental and a bet contract. Stipula comes with a formal semantics, an observational equivalence and a type inference system, that provide for a clear account of the contracts' behaviour and illustrate how several concepts from concurrency theory can be adapted to automatically verify the properties and the correctness of software-based legal contracts. We also discuss a prototype centralized implementation of Stipula. • A domain-specific programming language for defining and running legal contracts. • Few primitives corresponding to the distinctive elements of juridical acts. • Formal definition of syntax, operational semantics, normative equivalence, type inference system. • Prototype implementation. • Encoding of two paradigmatic legal contracts: a bike rental and a bet contract. [ABSTRACT FROM AUTHOR]

The Kiama language processing library is a collection of domain-specific languages for software language processing embedded in the Scala programming language. The standard Scala parsing library is augmented by Kiama's facilities for defining attribute grammars, strategy-based rewriting rules and combinator-based pretty-printing. We describe how we used Kiama to implement an Oberon-0 compiler as part of the 2011 LDTA Tool Challenge. In addition, we explain how Scala enabled a modular approach to the challenge. Traits were used to define components that addressed the processing tasks for each Oberon-0 sub-language. Combining the traits as mixins yielded the challenge artefacts. We conclude by reflecting on the strengths and weaknesses of Kiama that were revealed by the challenge and point to some future directions. [ABSTRACT FROM AUTHOR]

This paper describes LDTA tool challenge entry that is implemented using Simpl DSL toolkit. Simpl is targeted at enterprise software development, helping to create DSL implementations that can be embedded into other systems. Simpl builds up on top of existing tools and programming languages and adds: a simple language for grammar descriptions that can be used to generate both the parser and the data types for representing abstract syntax trees; a pretty-printing library; an IDE framework; and integration layer that combines all components into a single whole and minimizes the need for boilerplate code. When implementing the challenge, Simpl provided direct support for parsing and code generation tasks. Name and type checking were implemented in Scala. In addition to the challenge task, Simpl was used to create an Eclipse-based IDE for the target language. [ABSTRACT FROM AUTHOR]

Despite the fact that Domain Specific Modeling tools are becoming very powerful and more frequently used, the support for their cooperation has not reached its full strength, and demand for model management is growing. In cooperative work, the decision agents are semi-autonomous and therefore a solution for reconciliating DSM after a concurrent evolution is needed. Conflict detection and reconciliation are important steps for merging of concurrently evolved (meta)models in order to ensure collaboration. In this work, we present a conflict detection, reconciliation and merging framework for concurrently evolved meta-models and models. Additionally, we formally specify the EMF Ecore meta-model into set constructs that help to analyze the (meta)model and operations performed on it. [ABSTRACT FROM AUTHOR]

Dynamic program analysis (DPA) tools assist in many software engineering and development tasks, such as profiling, program comprehension, and performance model construction and calibration. On the Java platform, many DPA tools are implemented either using aspect-oriented programming (AOP), or rely on bytecode instrumentation to modify the base program code. The pointcut/advice model found in AOP enables rapid tool development, but does not allow expressing certain instrumentations due to limitations of mainstream AOP languages—developers thus use bytecode manipulation to gain more expressiveness and performance. However, while the existing bytecode manipulation libraries handle some low-level details, they still make tool development tedious and error-prone. Targeting this issue, we provide the first complete presentation of DiSL, an open-source instrumentation framework that reconciles the conciseness of the AOP pointcut/advice model and the expressiveness and performance achievable with bytecode manipulation libraries. Specifically, we extend our previous work to provide an overview of the DiSL architecture, advanced features, and the programming model. We also include case studies illustrating successful deployment of DiSL-based DPA tools. [ABSTRACT FROM AUTHOR]

We present a method for profiling programs that are written using domain-specific languages. Instead of reporting execution in terms of implementation details as in most existing profilers, our method operates at the level of the problem domain. Program execution generates a stream of events that summarises the execution in terms of domain concepts and operations. The events enable us to construct a hierarchical model of the execution. A flexible reporting system summarises the execution along developer-chosen model dimensions. The result is a flexible way for a developer to explore the execution of their program without requiring any knowledge of the domain-specific language implementation. These ideas are embodied in a new profiling library called dsprofile that is independent of the problem domain so it has no specific knowledge of the data and operations that are being profiled. We illustrate the utility of dsprofile by using it to profile programs that are written using our Kiama language processing library. Specifically, we instrument Kiama's attribute grammar and term rewriting domain-specific languages to use dsprofile to generate events that report on attribute evaluation and rewrite rule application. Examples of typical language processing tasks show how domain-specific profiling can help to diagnose problems in Kiama-based programs without the developer needing to know anything about how Kiama is implemented. [ABSTRACT FROM AUTHOR]

An Object Grammar is a variation on traditional BNF grammars, where the notation is extended to support declarative bidirectional mappings between text and object graphs. The two directions for interpreting Object Grammars are parsing and formatting . Parsing transforms text into an object graph by recognizing syntactic features and creating the corresponding object structure. In the reverse direction, formatting recognizes object graph features and generates an appropriate textual presentation. The key to Object Grammars is the expressive power of the mapping, which decouples the syntactic structure from the graph structure. To handle graphs, Object Grammars support declarative annotations for resolving textual names that refer to arbitrary objects in the graph structure. Predicates on the semantic structure provide additional control over the mapping. Furthermore, Object Grammars are compositional so that languages may be defined in a modular fashion. We have implemented our approach to Object Grammars as one of the foundations of the Ensō system and illustrate the utility of our approach by showing how it enables definition and composition of domain-specific languages (DSLs). [ABSTRACT FROM AUTHOR]

We present a method for profiling programs that are written using domain-specific languages. Instead of reporting execution in terms of implementation details as in most existing profilers, our method operates at the level of the problem domain. Program execution generates a stream of events that summarises the execution in terms of domain concepts and operations. The events enable us to construct a hierarchical model of the execution. A flexible reporting system summarises the execution along developer-chosen model dimensions. The result is a flexible way for a developer to explore the execution of their program without requiring any knowledge of the domain-specific language implementation. These ideas are embodied in a new profiling library called dsprofile that is independent of the problem domain so it has no specific knowledge of the data and operations that are being profiled. We illustrate the utility of dsprofile by using it to profile programs that are written using our Kiama language processing library. Specifically, we instrument Kiama's attribute grammar and term rewriting domain-specific languages to use dsprofile to generate events that report on attribute evaluation and rewrite rule application. Examples of typical language processing tasks show how domain-specific profiling can help to diagnose problems in Kiama-based programs without the developer needing to know anything about how Kiama is implemented. [ABSTRACT FROM AUTHOR]

Flow networks are inductively defined, assembled from small components to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. We carry out this induction formally using a domain-specific language (DSL). Associated with our DSL are a semantics and a typing theory. The latter gives rise to a system of formal annotations that enforce desirable properties of flow networks as invariants across their interfaces. A prerequisite for a typing theory is a formal semantics, i.e., a rigorous characterization of flows that are safe for the network (limited to the notion of feasible flows in this paper, unfeasible flows being considered unsafe). We give a detailed presentation of a denotational semantics only, but also point out the elements that an equivalent operational semantics must include. [ABSTRACT FROM AUTHOR]

Abstract: ISO 26262 addresses development of safe in-vehicle functions by specifying methods potentially used in the design and development lifecycle. It does not indicate what is sufficient and leaves room for interpretation. Yet the architects of electric/electronic systems need design boundaries to make decisions during architecture evolutionary design without adding a risk of late changes. Correct selection of safety mechanisms from alternatives at early design stages is vital for time-to-market of critical systems. In this paper we present and discuss an iterative architecture design and refinement process that is centered around ISO 26262 requirements and model-based analysis of safety-related metrics. This process simplifies identification of the most sensitive parts of the architecture, selection of the best suitable safety mechanisms to reduce thereby failure rate on the system level and improve the metrics defined by the standard. To support the defined process we present the metamodels that can be integrated with existing DSL (domain-specific language) frameworks to extend them with information supporting further extraction of fault propagation behavior. We provide a framework for architecture model analysis and selection of safety mechanisms. We provide details on the model-based toolset that has been developed to support the proposed analysis and synthesis methods, and demonstrate its application to analysis of a steer-by-wire system model and selection of safety mechanisms for it. [Copyright &y& Elsevier]

Abstract: Dynamic programming algorithms are traditionally expressed by a set of matrix recurrences—a low level of abstraction, which renders the design of novel dynamic programming algorithms difficult and makes debugging cumbersome. Bellman's GAP is a declarative, domain-specific language, which supports dynamic programming over sequence data. It implements the algebraic style of dynamic programming and allows one to specify algorithms by combining so-called yield grammars with evaluation algebras. Products on algebras allow to create novel types of analyses from already given ones, without modifying tested components. Bellman's GAP extends the previous concepts of algebraic dynamic programming in several respects, such as an “interleaved” product operation and the analysis of multi-track input. Extensive analysis of the yield grammar and the evaluation algebras is required for generating efficient imperative code from the algebraic specification. This article gives an overview of the analyses required and presents several of them in detail. Measurements with “real-world” applications demonstrate the quality of the code produced. [Copyright &y& Elsevier]

Abstract: The feature model formalism has become the de facto standard for managing variability in software product lines (SPLs). In practice, developing an SPL can involve modeling a large number of features representing different viewpoints, sub-systems or concerns of the software system. This activity is generally tedious and error-prone. In this article, we present FAMILIAR a Domain-Specific Language (DSL) that is dedicated to the large scale management of feature models and that complements existing tool support. The language provides a powerful support for separating concerns in feature modeling, through the provision of composition and decomposition operators, reasoning facilities and scripting capabilities with modularization mechanisms. We illustrate how an SPL consisting of medical imaging services can be practically managed using reusable FAMILIAR scripts that implement reasoning mechanisms. We also report on various usages and applications of FAMILIAR and its operators, to demonstrate their applicability to different domains and use for different purposes. [Copyright &y& Elsevier]

Abstract: Embedded domain-specific languages (EDSLs) are known to improve the productivity of developers. However, for many domains no DSL implementation is available and two important reasons for this are: First, the effort to implement EDSLs that provide the domain’s established syntax (called concrete syntax) is very high. Second, the EDSL and its underlying general-purpose programming language (GPL) are typically tightly integrated. This hampers reusability across different GPLs. Besides these implementation issues, the productivity gains of using EDSLs are also limited by the lack of explicit tool support for EDSL users—such as syntax highlighting or code analyses. In this paper, we present an approach that significantly reduces the necessary effort to implement embedded DSLs with concrete syntax. The idea is to use island grammars to specify the EDSL’s concrete syntax. This enables the developer to implement the embedded DSL as a library and to incrementally specify the concrete syntax using meta-data. Only those parts of the EDSL’s grammar need to be specified that deviate from the grammar of the GPL. By analyzing an EDSL’s implementation using reflection, it is possible to provide tool support for EDSLs without having the developer implement it explicitly, such as syntax highlighting. An evaluation demonstrates the feasibility of our approach by embedding a real-world DSL into a GPL. [Copyright &y& Elsevier]

Most large software applications rely on an external relational database for storing and managing persistent data. Typically, such applications interact with the database by first constructing strings that represent SQL statements, and then submitting these for execution by the database engine. The fact that these statements are only checked for correctness at runtime is a source for many potential defects, including type and syntax errors and vulnerability to injection attacks. The AraRat system presented here offers a method for dealing with these difficulties by coercing the host C++ compiler to do the necessary checks of the generated strings. A library of templates and preprocessor directives is used to embed in C++ a little language representing an augmented relational algebra formalism. Type checking of this embedded language, carried out by our template library, assures, at compile-time, the correctness and safety of the generated SQL strings. All SQL statements constructed by AraRat are guaranteed to be syntactically correct, and type safe with respect to the database schema. Moreover, AraRat statically ensures that the generated statements are immune to all injection attacks. The standard techniques of “expression templates” and “compile-time symbolic derivation” for compile-time representation of symbolic structures, are enhanced in our system. We demonstrate the support of a type system and a symbol table lookup of the symbolic structure. A key observation of this work is that type equivalence of instantiated nominally typed generics in C++ (as well as other languages, e.g., Java) is structural rather than nominal. This makes it possible to embed the structural type system, characteristic to persistent data management, in the nominal type system of C++. For some of its advanced features, AraRat relies on two small extensions to the standard C++ language: the typeof pseudo operator and the __COUNTER__ preprocessor macro. [Copyright &y& Elsevier]

Abstract: We propose a domain-specific aspect language to prevent denial of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, aspects can be seen as formal timed properties on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties. This article presents the main approach (programs, aspects, weaving) formally using timed safety automata. The specification of resources, optimizations and verification are sketched in a more intuitive fashion. Even if a concrete implementation remains as future work, we address some high-level implementation issues and illustrate the approach by small examples and a case study. [Copyright &y& Elsevier]

Abstract: Over the past two decades, Scheme macros have evolved into a powerful API for the compiler front end. Like Lisp macros, their predecessors, Scheme macros expand source programs into a small core language; unlike Lisp systems, Scheme macro expanders preserve lexical scoping, and advanced Scheme macro systems handle other important properties such as source location. Using such macros, Scheme programmers now routinely develop the ultimate abstraction: embedded domain-specific programming languages. Unfortunately, a typical Scheme programming environment provides little support for macro development. This lack makes it difficult for programmers to debug their macros and for novices to study the behavior of macros. In response, we have developed a stepping debugger specialized to the concerns of macro expansion. This debugger presents the macro expansion process as a linear rewriting sequence of annotated terms; it graphically illustrates the binding structure of the program as expansion reveals it; and it adapts to the programmer’s level of abstraction, hiding details of syntactic forms that the programmer considers built-in. [Copyright &y& Elsevier]