Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Model-to-Model Transformation in Meta-Modeled CINCO Domains
In this paper we present an approach to transform models of concrete domains specified with CINCO, a meta-modeling suite, into other CINCO domains. This procedure is demonstrated by transforming Webstory models to DIME applications. The model-to-model transformation increases benefits gained from domain-specific solutions, as shown with the DIME to web application generator, ultimately allowing for Webstories to be deployed and run as web applications
Conditions, constraints and contracts: On the use of annotations for policy modeling
Organisational policies express constraints on generation and processing of resources. Application domains, however, rely on transformation processes, which are in principle orthogonal to policy specifications, so that domain rules and policies may evolve in a non-synchronised way. In previous papers, we proposed annotations as a flexible way to model aspects of some kinds of policy. Annotations could be used to impose constraints on domain configurations, and we showed how to derive application conditions on transformations, and how to annotate complex patterns. We extend the approach here in different directions: we allow domain model elements (individual resources or collections thereof) to be annotated with collections of elements; we propose an original construction to solve the problem of orphan annotations, when annotated resources are consumed; we introduce a notion of contract, used by a policy to impose additional pre-conditions and postconditions on rules for deriving new resources. We also show how contracts for refined rules can be derived from contract schemes defined on some rule kernel. We discuss a concrete case study of linguistic resources, annotated with information on the licenses under which they can be used. The annotation framework allows forms of reasoning such as identifying conflicts among licenses, enforcing the presence of licenses, or ruling out some modifications of a licence configuration
Proving Correctness of Graph Programs Relative to Recursively Nested Conditions
We propose a new specification language for the proof-based approach to verification of graph programs by introducing mu-conditions as an alternative to existing formalisms which can express path properties. The contributions of this paper are the lifting of constructions from nested conditions to the new, more expressive conditions and a proof calculus for partial correctness relative to mu-conditions. In particular, we exhibit and prove the correctness of a construction to compute weakest preconditions with respect to finite graph programs
Cotransforming Grammars with Shared Packed Parse Forests
SPPF (shared packed parse forest) is the best known graph representation of a parse forest (family of related parse trees) used in parsing with ambiguous/conjunctive grammars. Systematic general purpose transformations of SPPFs have never been investigated and are considered to be an open problem in software language engineering. In this paper, we motivate the necessity of having a transformation operator suite for SPPFs and extend the state of the art grammar transformation operator suite to metamodel/model (grammar/graph) cotransformations
Parallel Evaluation of Interaction Nets: Case Studies and Experiments
Interaction nets are a particular kind of graph rewriting system that have many properties that make them useful for capturing sharing and parallelism. There have been a number of research efforts towards implementing interaction nets in parallel, and these have focused on the implementation technologies. In this paper we investigate a related question: when is an interaction net system suitable for parallel evaluation? We observe that some nets cannot benefit from parallelism (they are sequential) and some have the potential to be evaluated in a highly parallel way. This first investigation aims to highlight a number of issues, by presenting experimental evidence for a number of case studies. We hope this can be used to help pave the way to a wider use of this technology for parallel evaluation
On Single-Pushout Rewriting of Partial Algebras
We introduce Single-Pushout Rewriting for arbitrary partial algebras. Thus, we give up the usual restriction to graph structures, which are algebraic categories with unary operators only. By this generalisation, we obtain an integrated and straightforward treatment of graphical structures (objects) and attributes (data). We lose co-completeness of the underlying category. Therefore, a rule is no longer applicable at any match. We characterise the new application condition and make constructive use of it in some practical examples
20 Years of Triple Graph Grammars: A Roadmap for Future Research
Triple graph grammars (TGGs) provide a declarative, rule-based means of specifying binary consistency relationships between different types of graphs. Over the last 20 years, TGGs have been applied successfully in a range of application scenarios including: model neration,conformance testing, bidirectional model transformation, and incremental model synchronisation. In this paper, we review the progress made in TGG research up until now by exploring multiple research dimensions, including both the current frontiers of TGG research as well as important future challenges. Our aim is to provide a roadmap for the coming years of TGG research by stating clearly what we regard as adequately researched, and what we view as still unexplored potential
Composition of M,N-adhesive Categories with Application to Attribution of Graphs
This paper continues the work on M,N-adhesive categories and shows some important composition properties for these categories. We present a new concept of attributed graphs and show that the corresponding category is M,N-adhesive. As a consequence, we inherit all nice properties for M,N-adhesive systems such as the Local Church-Rosser Theorem, the Parallelism Theorem, and the Concurrency Theorem for this type of attributed graphs
Estimating Rewards & Rare Events in Nondeterministic Systems
Exhaustive verification can quantify critical behaviour arising from concurrency in nondeterministic models. Rare events typically entail no additional challenge, but complex systems are generally intractable. Recent work on Markov decision processes allows the extremal probabilities of a property to be estimated using Monte Carlo techniques, offering the potential to handle much larger models. Here we present algorithms to estimate extremal rewards and consider the challenges posed by rarity. We find that rewards require a different interpretation of confidence and that reachability rewards require the introduction of an auxiliary hypothesis test. We show how importance sampling can significantly improve estimation when probabilities are low, but find it is not a panacea for rare schedulers