Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Faster FDR Counterexample Generation Using SAT-Solving
Get PDFWith the flourishing development of efficient SAT-solvers, bounded model checking (BMC) has proven to be an extremely powerful symbolic model checking technique. In this paper, we address the problem of applying BMC to concurrent systems involving the interaction of multiple processes running in parallel. We adapt the BMC framework to the context of CSP and FDR yielding bounded refinement checking. Refinement checking reduces to checking for reverse containment of possible behaviours. Therefore, we exploit the SAT-solver to decide bounded language inclusion as opposed to bounded reachability of error states, as in most existing model checkers. We focus on the CSP traces model which is sufficient for verifying safety properties. We present a Boolean encoding of CSP processes resting on FDR's hybrid two-level approach for calculating the operational semantics using supercombinators. We describe our bounded refinement-checking algorithm which is based on watchdog transformations and incremental SAT-solving. We have implemented a tool, SymFDR, written in C++ which uses FDR as a shared library for manipulating CSP processes and the state-of-the-art SAT-solver MiniSAT. Experiments indicate that in some cases, especially for complex combinatorial problems, SymFDR significantly outperforms FDR
Control Plane Issues in the 4WARD Network Virtualization Architecture
Get PDFNetwork virtualization technologies offer a lot of opportunities and advantages
but create also new issues that need to be solved. In this paper, we discuss
control mechanisms, interfaces, and protocols required in order to allow for dynamic
setup of virtual networks. Finally, we describe some runtime aspects by examining
control interfaces and signaling protocols necessary for the management of virtual
networks
Overcoming a Communication Barrier on the Way Towards a Global Sensor Network
Get PDFIn a global sensor network different sensor platforms will be deployed. A
grave obstacle on the way of building sensor networks out of different sensor nodes are incompatible implementations of network protocol stacks used with different sensor node platforms. We describe our efforts to overcome this obstacle in a heterogeneous sensor network consisting out of MICAz Motes and Sun SPOTs, both using an IEEE 802.15.4 radio chip. We explain the major differences in the respective network stacks and our approach to bridge them. A network stack that bridges the gap between different platforms allows for more flexible and robust networks
Proofs-as-Programs in Computable Analysis
Get PDFSince the work of Brouwer, Kolmogorov, Goedel, Kleene and many others
we know that constructive proofs have computational meaning. In
Computer Science this idea is known as the
"proofs-as-programs paradigm" or "Curry-Howard correspondence".
We present examples from computable analysis showing that this
paradigm not only works in principle, but can be used to automatically
synthesise practically relevant certified programs
Understanding how OSS Development Models can influence assessment methods
Get PDFOne of the most important aspects of OSS that distinguishes it from COTS is both the variety and specific characteristics of the development models used. Understanding these development models will be critical to the effective design of assessment approaches. This paper documents the more common development models used by OSS projects and explores the complex landscape of stakeholders that these models expose
Using Resources as Synchronizers to Manage Mobile Process Adaptation
Get PDFProcess management in Mobile Ad-hoc NETworks (MANETs) has to deal with different types of tasks and resources. Teams can be formed with specific goals, such as recognition of a damaged area for disaster assessment, where each member of a team is assigned some task to be performed according to some policy. However, in real situations, it is possible that task assignments and policies have to be revised due to different causes. In addition to typical causes for dynamic changes in adaptive workflows, mobility introduces some specific problems, e.g. the need for new connectivity-maintaining tasks, or reassignment of tasks originally for members who have become unreachable, or who have no sufficient resources to complete the original plan. As these modifications occur dynamically, it is difficult to manage them through hard-coded programs. Rather, we propose the use of a rule-based formalism, expressed in terms of multi-set rewriting. This supports a resource-centered view, in which both data-dependencies between tasks and plan-dependent ordering of tasks are expressed as production and consumption of resources of different types. In turn, rules are themselves seen as resources, so that they are prone to the same rewriting process, in order to redefine process schemas. The paper illustrates these notions and formalisms, and shows some cases of their application
Using a Triple Graph Grammar for State Machine Implementations
Get PDFTypical techniques of model-driven development use graph transformations to manipulate models and use generators to produce source code. In this contribution we suggest to use graph transformations instead of generators in order to get a closer connection between model and code. We define a Triple Graph Grammar for the mapping from a modeling tool data format to source code and derive a sample set of transformation rules from this. Thereby both truly simultaneous manipulation of model and code is enabled as well as virtually simultaneous manipulation by direct propagation of changes from code to model and back again
Experimental Evaluation of Multi-Path Routing in a Wireless Mesh Network Inside a Building
Get PDFMulti-path routing can provide robustness and load balancing to com-
munication in wireless mesh networks (WMNs). We present a Linux implementation of an existing multi-path routing scheme and evaluate it in our inhouse WMN testbed. In addition to our implementation, we describe the testbed where we performed evaluations regarding end-to-end delay and packet loss. Furthermore, we identify the limitations of the implemented protocol in a real-world scenario with interferences due to dense node placement as well as third-party networks and discuss possible enhancements and general directions of research
Fuzzy Logic supported Consistency Management in DDVEs
Get PDFIn distributed virtual environments, where avatars permanently change their properties (e.g. their position) or perform modifications on shared objects, inconsistent states may occur due to message latency or concurrent updates. Here, the consistency often falls prey to high interactivity and responsiveness demands. To minimize the presence of inconsistent states or data, the Elastic Consistency model aims at providing an optimal trade-off between consistency and system responsiveness. In this paper we present a Fuzzy Logic driven approach for the computation of this trade-off on the basis of environmental characteristics at the application runtime. Furthermore, we evaluate the impacts of this parameter on consistency and system responsiveness by adjusting the behavior of a classic mutual exclusion algorithm. In this paper we show that an acceptable degree of consistency with respect to required system responsiveness can be efficiently achieved, even when addressing a large number of users
An Architectural Approach to the Design and Analysis of Cyber-Physical Systems
Get PDFThis paper presents an extension of existing software architecture tools to model physical systems, their interconnections, and the interactions between physical and cyber components. A new CPS architectural style is introduced to support the principled design and evaluation of alternative architectures for cyber-physical systems (CPSs). The implementation of the CPS architectural style in AcmeStudio includes behavioral annotations on components and connectors using either finite state processes (FSP) or linear hybrid automata (LHA) with plug-ins to perform behavior analysis using the Labeled Transition System Analyzer (LTSA) or Polyhedral Hybrid Automata Verifier (PHAVer), respectively. The CPS architectural
style and analysis plug-ins are illustrated with an example