Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
A Modular and Statically Typed Effectful Stack for Custom Graph Traversals
Get PDFProgrammers often have to implement custom graph traversals by hand as either there are no suitable text-book algorithms for their tasks, or their problems are too complex for a pure querying language that lacks modularity or static typing. Our new Scala-based graph traversal language uses an effectful stack that adapts monads and type classes. Arbitrary graph effect computations and graph processing rules can be defined and composed in a modular and statically typed way. Custom graph traversals become expressible in a concise notation, run both in-memory and on graph databases, and also allow for parallelization. We evaluate the usability of our approach by detecting occurences of an anti-pattern in a Java source code archive. Our approach outperforms the well-known Gremlin approach due to parallelization
Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling
Get PDFIntegrating graphical representations with formal methods can help bridge the gap between requirements and formal modelling. In this paper, we compare and evaluate two graphical approaches aiming at describing control flows and refinement in Event-B, and we use a fire dispatch system case study to perform this evaluation. The fire dispatch system case study provides a good example of a complex workflow through which we try to identify a process that facilitates defining the structural and the behavioural parts of the Event-B model. In our case study, we focus on building the dynamic part of the model to evaluate the two diagrammatic notations: UML Activity Diagrams and Atomicity Decomposition Diagrams. Based on our evaluation, we try to identify the advantages and limitations of both approaches. Finally, we try to compare how both graphical notations can affect the Event-B formal modelling of our case study
ScenarioTools Real-Time Play-Out for Test Sequence Validation in an Automotive Case Study
Get PDFIn many areas, such as automotive, healthcare, or production, we find software-intensive systems with complex real-time requirements. To efficiently ensure the quality of these systems, engineers require automated tools for the validation of the requirements throughout the development. This, however, requires that the requirements are specified in an analyzable way. We propose modeling the specification using Modal Sequence Diagrams (MSDs), which express what a system may, must, or must not do in certain situations. MSDs can be executed via the play-out algorithm to investigate the behavior emerging from the interplay of multiple scenarios; we can also test if traces of the final product satisfy all scenarios. In this paper, we present the first tool supporting the play-out of MSDs with real-time constraints. As a case study, we modeled the requirements on gear shifts in an upcoming standard on vehicle testing and use our tool to validate externally generated gear shift sequences
Improving the Search Capabilities of a CFLP(FD) System
Get PDFThe CFLP system TOY(FD) is implemented in SICStus Prolog, and supports FD constraints by interfacing the CP(FD) solvers of Gecode and ILOG Solver. In this paper TOY(FD) is extended with new search primitives, in a setting easily adaptable to other Prolog CLP or CFLP systems. The primitives are described from a solver-independent point of view, pointing out some novel concepts not directly available in the Gecode and ILOG Solver libraries, as well as how to specify some search criteria at TOY(FD) level and how easily these strategies can be combined to set different search scenarios. The implementation of the primitives is described, presenting an abstract view of the requirements and how they are targeted to the Gecode and ILOG libraries. Finally, some benchmarks show that the new search strategies improve the solving performance of TOY(FD)
The Implementation of the CHA-Q Meta-Model: A Comprehensive, Change-Centric Software Representation
Get PDFAlthough contemporary software development processes have embraced the need for continuous change, most development tools still assume that they act upon a single complete release of the system. The CHA-Q project (Change-centric Quality Assurance) aims to strike a balance between agility and reliability through change-centric quality assurance tools. These tools are to share a first-class representation of changes to software artefacts. In this paper we present the CHA-Q meta-model that defines this representation and highlight important characteristics of its implementation: an object-oriented API, persistency through a graph database, and a strategy for tracking the history of artefacts in a memory-efficient manner
Simplifying proofs of linearisability using layers of abstraction
Get PDFLinearisability has become the standard correctness criterion for concurrent data structures, ensuring that every history of invocations and responses of concurrent operations has a matching sequential history. Existing proofs of linearisability require one to identify so-called linearisation points within the operations under consideration, which are atomic statements whose execution causes the effect of an operation to be felt. However, identification of linearisation points is a non-trivial task, requiring a high degree of expertise. For sophisticated algorithms such as Heller et al’s lazy set, it even is possible for an operation to be linearised by the concurrent execution of a statement outside the operation being verified. This paper proposes a method for verifying linearisability that does not require identification of linearisation points. Instead, using an interval-based logic, we show that every behaviour of each concrete operation over any interval is a possible behaviour of a corresponding abstraction that executes with coarse-grained atomicity. This approach is applied to Heller et al’s lazy set to show that verification of linearisability is possible without having to consider linearisation points within the program code
Clone Detection in Matlab Stateflow Models
Get PDFMatlab Simulink is one of the leading tools for model based software development in the automotive industry. One extension to Simulink is Stateflow, which allows the user to embed Statecharts as components in a Simulink Model. These state machines contain nested states, an action language that describes events, guards, conditions and actions and complex transitions. As Stateflow has become increasingly important in Simulink models for the automotive sector, we extend previous work on clone detection of Simulink models to Stateflow components
The GPUVerify Method: a Tutorial Overview
Get PDFI present a tutorial overview demonstrating the key technique used by GPUVerify, a static verification tool for graphics processing unit (GPU) kernels. The technique is a method for translating a massively parallel GPU kernel into a sequential program such that correctness of the sequential program implies data race-freedom of the parallel kernel
Richer Interface Automata with Optimistic and Pessimistic Compatibility
Get PDFModal transition systems are a popular semantic underpinning of interface theories, such as Nyman et al.’s IOMTS and Bauer et al.’s MIO, which facilitate component-based reasoning of concurrent systems. Our interface theory MIA repaired a compositional flaw of IOMTS-refinement and introduced a conjunction operator. In this paper, we first modify MIA to properly deal with internal computations including internal must-transitions, which were largely ignored already in IOMTS. We then study a MIA variant that adopts MIO’s pessimistic – rather than IOMTS’ optimistic – view on component compatibility and define, for the first time in a pessimistic, non-deterministic setting, conjunction and disjunction on interfaces. For the pessimistic MIA variant we also provide a mechanism for extending alphabets when refining interfaces, which is a desired feature in practice. We illustrate our advancements via a small example
Late Propagation in Near-Miss Clones: An Empirical Study
Get PDFIf two or more code fragments in the code-base of a software system are exactly or nearly similar to one another, we call them code clones. It is often important that updates (i.e., changes) in one clone fragment should be propagated to the other similar clone fragments to ensure consistency. However, if there is a delay in this propagation because of unawareness, the system might behave inconsistently. This delay in propagation, also known as late propagation, has been investigated by a number of existing studies. However, the existing studies did not investigate the intensity as well as the effect of late propagation in different types of clones separately. Also, late propagation in Type 3 clones is yet to investigate. In this research work we investigate late propagation in three types of clones (Type 1, Type 2, and Type 3) separately. According to our experimental results on six subject systems written in three programming languages, late propagation is more intense in Type 3 clones compared to the other two clone-types. Block clones are mostly involved in late propagation instead of method clones. Refactoring of block clones can possibly minimize late propagation. If not refactorable, then the clones that often need to be changed together consistently should be placed in close proximity to one another