Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Automatically Generating CSP Models for Communicating Haskell Processes
Get PDFTools such as FDR can check whether a CSP model of an implementation is a refinement of a given CSP specification. We present a technique for generating such CSP models of Haskell implementations that use the Communicating Haskell Processes library. Our technique avoids the need for a detailed semantics of
the Haskell language, and requires only minimal program annotation. The generated CSP-M model can be checked for deadlock or refinements by FDR, allowing easy use of formal methods without the need to maintain a model of the program implementation alongside the program itself
Testing self-adaptive applications with simulation of context events
Get PDFModern trends in mobile computing have raised the expectations of users
in terms of such features such as context-awareness and self-adaptiveness. With
such capabilities, applications can autonomously sense their context and automate a
number of tasks, effectively reducing the attention required by the end users. This
paper presents a custom simulation engine, designed to support the testing of applications
developed using the MUSIC platform. The simulation tool consists of
a platform-independent server module, deployed along with the application, and
a client module which is responsible for interpreting and executing the simulation
script. The use of the tool is demonstrated in the scope of the SatMotion application,
which is designed to assist satellite antenna installers with specialized functionality
Tightly coupled verification of pervasive systems
Get PDFWe consider the problem of verifying context-aware, pervasive, interactive systems when the interaction involves both system configuration and system use. Verification of configurable systems is more tightly coupled to design when the verification process involves reasoning about configurable formal models. The approach is illustrated with a case study: using the model checker SPIN and a SAT solver to reason about a configurable model of an activity monitor from the MATCH homecare infrastructure. Parts of the models are generated automatically from actual log files
Pattern-Based Layout Specifications for Visual Language Editors
Get PDFWhen creating an editor for a visual language, a challenging task is the layout specification. Many visual languages, e.g., Ecore diagrams or Petri nets, show similar layout characteristics, and hence reuse of layout behavior should be enabled. For that purpose, we introduce the concept of layout patterns, which encapsulates certain layout behavior. With the approach, it is possible to combine different layout algorithms, e.g., standard graph drawing algorithms and constraint-based algorithms. In addition, rule-based layout algorithms may be used that are specifically tailored to the interactive nature of visual language editors
Towards Theorem Proving Graph Grammars using Event-B
Get PDFGraph grammars may be used as specification technique for different kinds of systems, specially in situations in which states are complex structures that can be adequately modeled as graphs (possibly with an attribute data part) and in which the behavior involves a large amount of parallelism and can be described as reactions to stimuli that can be observed in the state of the system. The verification of properties of such systems is a difficult task due to many aspects: in many situations the systems have an infinite number of states; states themselves are complex and large; there are a number of different computation possibilities due to the fact that rule applications may occur in parallel. There are already some approaches to verification of graph grammars based on model checking, but in these cases only finite state systems can be analyzed. Other approaches propose over- and/or under-approximations of the state-space, but in this case it is not possible to check arbitrary properties. In this work, we propose to use the Event-B formal method and its theorem proving tools to analyze graph grammars. We show that a graph grammar can be translated into an Event-B specification preserving its semantics, such that one can use several theorem provers available for Event-B to analyze the reachable states of the original graph grammar. The translation is based on a relational definition of graph grammars, that was shown to be equivalent to the Single-Pushout approach to graph grammars
Specification and Verification of Model Transformations
Get PDFModel transformations are a key concept within model driven development and there is an enormous need for suitable formal analysis techniques for model transformations, in particular with respect to behavioural equivalence of source models and their corresponding target models.
For this reason, we discuss the general challenges that arise for the specification and verification of model transformations and present suitable formal techniques that are based on graph transformation. In this context, triple graph grammars show many benefits for the specification process, e.g. modelers can work on an intuitive level of abstraction and there are formal results for syntactical correctness, completeness and efficient execution. In order to verify model transformations with respect to behavioural equivalence we apply well-studied techniques based on the double pushout approach with borrowed context, for which the model transformations specified by triple graph transformation rules are flattened to plain (in-situ) graph transformation rules.
The potential and adequateness of the presented techniques are demonstrated by an intuitive example, for which we show the correctness of the model transformation with respect to bisimilarity of source and target models
Testing as a Certification Approach
Get PDFFor years, one of the main reasons to buy commercial software instead of adopting open-source applications was the, supposed, guarantee of quality. Unfortunately that was rarely true and, fortunately, open-source projects soon adopted some good practices in their code development that lead to better tested software and therefore higher quality products.
In this article we provide a guided tour of some of the best practices that have been implemented in the Perl community in the recent years, as the pathway to a better community oriented repository of modules, with automatic distributed testing in different platforms and architectures, and with automatic quality measures calculation
Evaluation of the Technology Agnostic Service Creation Approach
Get PDFThe current computing and communication services provide convenience and functionality. The creation of these services is however not an easy task. Service development is still mainly technical oriented, where service creation tools are meant for serving and assisting the professional developers. In other words, service creation is not seen as a task for end-users. In our research, we wish to enable service creation for the end-users. This is achieved by introducing the technology agnostic approach into the process. In this paper, we present the conceptual architecture as the proposed solution. Prototype tools were designed and implemented as proof of concept. An evaluation event was held to obtain user feedback on the approach and the prototype tools. This paper presents and discusses the outcome of the evaluation
A Termination Criterion for Graph Transformations with Negative Application Conditions
Get PDFTermination of graph transformations is in general undecidable, but it is possible to prove it for specific systems by checking for sufficient conditions. In the presence of rules with negative application conditions, the difficulties increase.
In this paper we propose a different approach to the identification of a (sufficient) criterion for termination, based on the construction of a labelled transition system whose states represent overlaps between the negative application condition and the right hand side that can give rise to cycles