Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Formal verification of a theory of packages
Get PDFOver the years, open source distributions have become increasingly largeand complex—as an example, the latest Debian distribution contains almost 30 000packages.Consequently, the tools that deal with these distribution have also become more andmore complex. Furthermore, to deal with increasing distribution sizes optimisationhas become more important as well.To make sure that correctness is not sacrificed for complexity and optimisation, it isimportant to verify the underlying assumptions formally.In this paper, we present an example of such a verification: a formalisation in Coqof a theory of packages and their interdependencies
Graph Tuple Transformation
Get PDFGraph transformation units are rule-based devices to model and compute relations between initial and terminal graphs. In this paper, they are generalized to graph tuple transformation units that allow one to combine different kinds of graphs into tuples and to process the component graphs simultaneously and interrelated with each other. Moreover, one may choose some of the working components as inputs and some as outputs such that a graph tuple transformation unit computes a relation between input and output tuples of potentially different kinds of graphs rather than a binary relation on a single kind of graphs
Graph Rewriting with Contextual Refinement
Get PDFIn the standard theory of graph transformation, a rule modifies only subgraphs of constant size and fixed shape. The rules supported by the graph-rewriting tool GrGen are far more expressive: they may modify subgraphs of unbounded size and variable shape. Therefore properties like termination and confluence cannot be analyzed as for the standard case. In order to lift such results, we formalize the outstanding feature of GrGen rules by using plain rules on two levels: schemata} are rules with variables; they are refined with meta-rules, which are based on contextual hyperedge replacement, before they are used for rewriting.We show that every rule based on single pushouts, on neighborhood-controlled embedding, or on variable substitution can be modeled by a schema with appropriate meta-rules. It turns out that the question whether schemata may have overlapping refinements is not decidable
Edit languages for information trees
Get PDFWe consider a simple set of edit operations for unordered, edge-labeled trees, called information trees by Dal Zilio et al in "A Logic You Can Count On". We define tree languages using the sheaves automata from Foster et al's "A Logic Your Typechecker Can Count On" which in turn are based on Dal Zilio et al and provide an algorithm for deciding whether a complex edit preserves membership in a tree language. This allows us to view sheaves automata and subsets of tree edits as edit languages in the sense of Hofmann et al's "Edit Lenses". They can then be used to instantiate the framework of edit lenses between such languages and model concrete examples such as synchronisation between different file systems or address directories
On Propagation-Based Concurrent Model Synchronization
Get PDFThe aim of concurrent model synchronization is to merge pairs of updates on interrelated models. For instance, this situation may occur in the context of model driven software development when the work is distributed between different teams. A first problem is that, if the updates are in conflict, this conflict is never explicit. The reason is that the updates do not interfere directly since they are assumed to modify different models. For this reason, detecting and solving conflicts becomes already more difficult than in the more standard case of synchronizing concurrent updates over a given model. Existing general approaches define the solution to this problem in terms of the solution to the simpler problem of update propagation in bidirectional model transformation. We call these approaches \emph{propagation based}.In this paper, we first state some properties that, in our opinion, must be satisfied by a concurrent synchronization procedure to be considered correct. Then, we show how to check whether the given updates are conflict-free and, in this case, we present a correct synchronization procedure based on this check. Finally, we consider the case where the given updates are in conflict and we show how we can build solutions that satisfy some of the correctness properties but, in general, not all of them. Specifically, we present counter-examples that show how some of these properties may fail
Delta Lenses and Opfibrations
Get PDFWe compare the delta lenses, also known as d-lenses, of Diskin et al. with the c-lenses, known to be equivalent to opfibrations, already studied by the authors. Contrary to expectation a c-lens is a d-lens but not conversely. This result is surprising because d-lenses appear to provide the same information as c-lenses, and some more besides, suggesting that the implication would be the reverse -- a d-lens would appear to be a special kind of c-lens. The source of the surprise can be traced to the way the two concepts deal differently with morphisms in a certain base comma category (G,1_\bV). Both c-lenses and d-lenses are important because they extend the notion of lens to take account of the information available in known transitions between states and this has important implications in practice
Derivation Languages of Graph Grammars
Get PDFWe investigate sequential derivation languages associated with graph grammars, as a loose generalisation of free-labeled Petri nets and Szilard languages. The grammars are used to output strings of rule labels, and the applicability of a special rule determines the acceptance of a preceding derivation.Due to the great power of such grammars, this family of languages is quite large and endowed with many closure properties. All derivation languages are decidable in nondeterministic polynomial time and space O(n log n), by simulation of the graph grammar on a Turing machine
Tabling with Support for Relational Features in a Deductive Database
Get PDFTabling has been acknowledged as a useful technique in the logic programming arena for enhancing both performance and declarative properties of programs. As well, deductive database implementations benefit from this technique for implementing query solving engines. In this paper, we show how unusual operations in deductive systems can be integrated with tabling.Such operations come from relational database systems in the form of null-related (outer) joins, duplicate support and duplicate elimination. The proposal has been implemented as a proof of concept rather than an efficient system in the Datalog Educational System (DES) using Prolog as a development language and its dynamic database
The ScenarioTools Play-Out of Modal Sequence Diagram Specifications with Environment Assumptions
Get PDFMany software-intensive systems consist of multiple components that provide complex functionality by their interaction. The scenario-based languages LSCs and MSDs are intuitive, but precise means to specify interactions; the engineers can specify how a system can, must, or must not react to events in its environment. A key benefit of LSCs/MSDs is that they can be executed via the play-out algorithm, which allows engineers to perform an early automated analysis of the specification. However, LSCs/MSDs lack support for expressing also what can or cannot happen in the environment. This is crucial especially in embedded systems: very often, the software will only be able to satisfy its requirements if certain assumptions are made about the behavior of mechanical parts or the physical environment. We extend MSD specifications to formally express such environment assumptions, and propose a corresponding extension of the play-out algorithm. The concepts are implemented in a novel, Eclipse-based tool
Verifying Total Correctness of Graph Programs
Get PDFGP 2 is an experimental nondeterministic programming language based on graph transformation rules, allowing for visual programming and the solving of graph problems at a high-level of abstraction. In previous work we demonstrated how to verify graph programs using a Hoare-style proof calculus, but only partial correctness was considered. In this paper, we add new proof rules and termination functions, which allow for proofs to additionally guarantee that program executions always terminate (weak total correctness), or that programs always terminate and do so without failure (total correctness). We show that the new proof rules are sound with respect to the operational semantics of GP 2, complete for termination, and demonstrate their use on some example programs