Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form
Get PDFWe present an approach for the translation of imperative code (like
C, C++) into the synchronous formalism Signal, in order to use a
model-checker to verify properties on the source code. The
translation uses SSA as an intermediate formalism, and the GCC
compiler as a front-end. The contributions of this paper with
respect to previous work are a more efficient translation scheme,
and the management of parallel code. It is applied successfully on
simple SystemC examples
User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?
Get PDFThis note considers the design of user interfaces for interactive theorem provers. The basic rules of interface design are reviewed, and their applicability to theorem provers is discussed, leading to considerations about the particular challenges of interface design for theorem provers. A short overview and classification of existing interfaces is given, followed by suggestions of possible future work in the area
Identifying the Challenges in Reducing Latency in GSN using Predictors
Get PDFSimulations based on real-time data continuously gathered from sensor networks all over the world have received growing attention due to the increasing availability of measured data. Furthermore, predictive techniques have been employed in the realm of such networks to reduce communication for energy-efficiency. However, research has focused on the high amounts of data transferred rather than latency requirements posed by the applications. We propose using predictors to supply data with low latency as required for accurate simulations. This paper investigates requirements for a successful combination of these concepts and discusses challenges that arise
From Hyperedge Replacement to Separation Logic and Back
Get PDFHyperedge-replacement grammars and separation-logic formulas both
define classes of graph-like structures. In this paper, we relate the different formalisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two approaches are of equivalent power. It follows that our fragment of separation-logic
inherits properties of hyperedge-replacement grammars, such as inexpressibility results. We also show that several operators of full separation logic cannot be expressed using hyperedge replacement
A Secure Remote Authentication, Operation and Management Infrastructure for Distributed Wireless Sensor Network Testbeds
Get PDFIn this paper we propose an infrastructure for a secure remote authentication, management and operation system for a distributed global wireless sensor network testbed. We base the design of the architecture on an existing well-established, widely deployed and frequently used authentication and authorization system developed to simplify inter-organizational access to web-resources. The proposed infrastructure
addresses the main challenges of a interconnected distributed sensor network
testbed, such as secure remote availability, multi-user access, confidentiality
and integrity. The paper further describes our perspective of a testbed workflow management and operation system aiming to provide a simple and comprehensive interface for remote wireless sensor network configuration and experimentation
Layered Architecture Consistency for MANETs: Introducing New Team Members
Get PDFIn this paper we extend our results concerning the layered architecture for modeling workflows in Mobile Ad-Hoc networks (MANETs) using algebraic higher order nets. MANETs are networks of mobile devices that communicate with each other via wireless links without relying on an underlying infrastructure. Workflows in \manets can be adequately modeled using a layered architecture, where the overall workflow, the team members' activities and the mobility issues are separated into three different layers, namely the workflow layer, the mobility layer and the team layer. In fromer papers a formal notion of layer consistency was suggested, that we now extend to allow changes of the interfaces of the gluing of the workflow and the mobility layer
Praxisfallbeispiel: Modernisierung einer Mainframe-Anwendung durch eine verteilte SOA
Get PDFAuch heute noch sind Legacy-Anwendungen auf Basis von Mainframe-DBMS wie Adabas und zugehörigen Programmiersprachen wie Natural häufig produktiv. Sie sind jedoch oft nur schlecht mit neuen Unternehmensanwendungen integriert. Der vorliegende Beitrag zeigt in einem Fallbeispiel die Modernisierung einer solchen Anwendung unter Einsatz von Web Services als Basis ihrer Integration in eine verteilte, Service-orientierte Architektur (SOA)
Open-DO: Open Framework for Critical Systems
Get PDFCritical systems development pushes software quality to the extreme. When human life depends on the correct operation of the software, strict processes are put in place to ensure, as much as possible, the absence of errors in the airborne system. These processes are very tool-demanding, and these tools also need to follow stringent and rigorous guidelines to provide the proper guarantees of quality. The Open-DO initiative aims at providing a framework federating open-source tools for safety-critical systems. A key point is that these tools will come with the material to ensure that industrial users can trust their output and use them to develop software compliant to the highest integrity levels
A Generic Graph Transformation, Visualisation, and Editing Framework in Haskell
Get PDFGraph transformation, visualisation, and editing are useful in many contexts, and require domain-specific customisation. However, many general-purpose graph solutions lack customisability in at least one area.
We present a framework that aims to allow polished customisation in all three areas, using the powerful abstraction capabilities of the pure functional programming language Haskell. The design of our framework integrates and adapts time-tested object-oriented designs into a purely functional framework, and uses current user-interface libraries (GTK+ and Cairo) to achieve polished presentation.
Our framework provides both a low-level programmed approach to graph transformation, and, on top of this, high-level approaches including SPO and DPO, which are implemented using categorical abstractions in an intuitive and flexible way