Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Security in Open Model Software with Hardware Virtualisation – The Railway Control System Perspective
Get PDFUsing the openETCS initiative as a starting point, we describe how open software can be applied in combination with platform-specific, potentially closed source extensions, in the development, verification, validation and certification of safety-critical railway control systems. We analyse the safety and security threats presented by this approach and discuss conventional operating system partitioning mechanisms, as well as virtualisation methods with respect to their potential to overcome these problems. Furthermore, we advocate a shift from open source to open models, in order to increase the development efficiency of combined open and proprietary solutions
Ambient Contracts
Get PDFWith current programming languages programmers have to manually keep track of device connectivity state changes while interacting with multiple partners in an ambient environment. This leads to complex code which is hard to evolve and maintain. We propose ambient contracts, a novel programming abstraction which tracks connectivity states in order to react appropriately when failure occurs. With ambient contracts the programmer no longer needs to be concerned about connectivity state changes during interaction, which leads to cleaner code
Stepping from Graph Transformation Units to Model Transformation Units
Get PDFGraph transformation units are rule-based entities that allow to transform source graphs into target graphs via sets of graph transformation rules according to a control condition. The graphs and rules are taken from an underlying graph transformation approach. Graph transformation units specify model transformations whenever the transformed graphs represent models. This paper is based on the observation that in general models are not always suitably represented as single
graphs, but they may be specified as the composition of a variety of different formal structures such as sets, tuples, graphs, etc., which should be transformed by compositions of different types of rules and operations instead of single graph
transformation rules. Consequently, in this paper, graph transformation units are generalized to model transformation units that allow to transform such kind of composed
models in a rule-based and controlled way. Moreover, two compositions of model transformation units are presented
Algebraic Model Checking
Get PDFThree algebraic approaches to model checking are presented and compared with each other with respect to their range of applications and their degree of automation. They have been implemented and tested in our Haskell-based formal-reasoning and -presentation system Expander2. Besides realizing and integrating state-of-the-art proof and computation rules the system admits the co/algebraic specification of the models to be checked in terms of rewrite rules and functional-logic programs. It also offers flexible features for visualizing and even animating models and computations. This paper does not present purely theoretical work. Due to the increasing abstraction potential of programming languages like Haskell, traditional gaps between specification formalisms and their executable implementations as well as between systems developed in different communities are going to vanish. The topics discussed in this article and the way of their presentation reflect this fact
OCL contracts for the verification of model transformations
Get PDFA model-driven engineering process relies on a set of transformations which are usually sequentially executed, starting from an abstract level to produce code or a detailed implementation specification. These transformations may be entirely automated or may require manual intervention by designers. In this paper, we propose a method to verify that a transformation result is correct with respect to the transformation specification. This method both includes automated transformations and manual interventions. For that, we focus on transformation contracts written in OCL. This leads to making the proposed method independent of modeling and transformation tools. These contracts are partially or fully generated through a dedicated tool
Declarative Models for Business Processes and UI Generation using OCL
Get PDFThis paper presents an approach to model business processes and associated user interfaces in a declarative way, relying on constraints. An UML-based meta-model to define processes, activities and user-interface objects is proposed. Connecting activities and user interface objects in an integrated model allows expressing interdependencies and mutual effects. Flexible execution logic for workflows and UI control flows are specified by OCL invariants. The model is constructed for the UML tool USE. Using object snapshots, USE can animate and validate business scenarios. Snapshots represent states of a process and a UI at specific times. Such animation enables business process and UI designers to discuss sensible scenarios on basis of the flexible declarative models. The intention is to create validated concrete process models in connection with UI elements that will provide a basis for the system implementation
Recognizable Graph Languages for Checking Invariants
Get PDFWe generalize the order-theoretic variant of the Myhill-Nerode theorem to graph languages, and characterize the recognizable graph languages as the class of languages for which the Myhill-Nerode quasi order is a well quasi order. In the second part of the paper we restrict our attention to graphs of bounded interface size, and use Myhill-Nerode quasi orders to verify that, for such bounded graphs, a recognizable graph property is an invariant of a graph transformation system. A recognizable graph property is a recognizable graph language, given as an automaton functor. Finally, we present an algorithm to approximate the Myhill-Nerode ordering
Symbolic Attributed Graphs for Attributed Graph Transformation
Get PDFIn this paper we present a new approach to deal with attributed graphs and attributed graph transformation. This approach is based on working with what we call symbolic graphs, which are graphs labelled with variables together with a formula that constrains the possible values that we may assign to these variables. In particular, in this paper we will compare in detail this new approach with the standard approach to attributed graph transformation
From Graph Transformations to Differential Equations
Get PDFIn a variety of disciplines models are used to predict, measure or explain quantitative properties. Examples include the concentration of a chemical substance produced within a given period, the growth of the size of a population of individuals, the time taken to recover from a communication breakdown in a network, etc.
The models such properties arise from are often discrete and structural in nature. Adding information on the time and/or probability of any actions performed, quantitative models can be derived. In the first example above, commonly referred to as
kinetic analysis of chemical reactions, a system of differential equations describing the evolution of concentrations is extracted from specifications of individual chemical reactions augmented with reaction rates. Recently, this construction has inspired approaches based on stochastic process specification techniques aiming to extract a continuous, quantitative model of a system
from a discrete, structural one. This paper describes a methodology for such an extraction based on stochastic graph transformations. The approach is based on a variant of the construction of critical pairs and has been implemented using the AGG tool and validated for a simple reaction of unimolecular
nucleophilic substitution (SN1)