Thanks to the popularity of mobile devices a large number of location-based services (LBS) have emerged. While a large number of privacy-preserving solutions for LBS have been proposed, most of these solutions do not ...

The GI Working Group“Programming Languages and Computing Concepts” arranges since 1984 each spring a workshop in the the “Physikzentrum Bad Honnef” (a convention centre of the German Physical Society). The meeting serves ...

A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, they must be lax enough to allow for hardware and compiler optimizations; on the other, ...

Refactoring is an essential operation in software engineering, with the purpose of improving the structural qualities of software. An emerging trend in software engineering is the use of model-driven approaches in which ...

In model-driven engineering approaches, models are considered firstclass entities. The composition of models is a necessity for modelling software systems. Structural composition of models has been studied thoroughly during ...

In this research report we propose a self-organizing media streaming solution that supports multiple interacting participants as well as a large number of observers. This solution is aimed at a number of emerging multimedia ...

We present a representation of spatial data that supports answering of qualitative queries (involving e.g. containment and overlap), using less time than numerical computations on coordinates, and less space than explicitly ...

Less than Best Effort (LBE) transports are transport protocols that use spare bandwidth left by Best Effort (BE) transports to fulfill their own data transfer tasks. Such kind of protocols can be used by non-delay/bandwidth ...

The concrete problem this paper addresses is the following: Given a set of objects with a spatial interpretation and a set of qualitative relations, construct a bintree representation that returns the same answers to queries ...

This report explains the details of a configurable index structure that allows to perform efficiently the kinds of filtering operations required to implement faceted search over RDF data. Unlike previous systems, it is ...

In this paper, we formalize an operational semantics of a weak memory model similar to the one in Go, concentrating on buffered writes, i.e., ignoring the possibility of buffered reads.

In recent years, it has come to attention that governments have been doing mass surveillance of personal communications without the consent of the citizens. As a consequence of these revelations, developers have begun ...

Railway systems designs deal with complex and large-scale, safety-critical infrastructures, where formal methods play an important role, especially in verifying the safety of so-called interlockings through model checking. ...

We provide a non-interleaving operational semantics for the pi-calculus as asynchronous transition systems, which generalizes the standard interleaving structural operational semantics and unfolds to standard, stable prime ...

The rapidly increasing pervasiveness and integration of computers in human and animal society calls for a broad discipline under which this development can be studied. We argue that to design and use technology one needs ...

Modern cloud applications consist of software components deployed on multiple virtual machines. Deploying such applications is error prone and requires detailed system expertise. The deployment optimization problem is about ...

Client platform infection poses a significant threat to secure user authentication. Com- bining vulnerable client platforms with special security devices, as often the case in e- banking, can increase significantly the ...

The rapidly increasing pervasiveness and integration of computers in human and animal society calls for a broad discipline under which this development can be studied. We argue that to design and use technology one needs ...

Identity and authentication solutions often lack usability and scalability, or do not provide high enough authentication assurance. The concept of Lucidman (Local User-Centric Identity Management) is an approach to providing ...

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method ...

Publish/subscribe (pub/sub) is a popular communication paradigm in the design of largescale distributed systems. A fundamental challenge in deploying pub/sub systems on a data center or a cloud infrastructure is efficient ...

Congestion occurs at a bottleneck along an Internet path; multiple flows between the same sender and receiver pairs can benefit from using only a single congestion control instance when they share the same bottleneck. These ...

We prove that a selection of quality of information optimisation problems related to event detection in sensor networks are NP-hard.

Several formal models combine probabilistic and nondeterministic features. To allow their probabilistic simulation and statistical model checking by means of pseudo-random number sampling, all sources of nondeterminism ...

Unbounded data structures, advanced functions and data types, and/or different forms of communication are often needed to model large and complex probabilistic real-time systems such as wireless sensor network algorithms. ...

PSMaude is a probabilistic extension of Maude that provides an expressive probabilistic strategy language to quantify the nondeterminism in probabilistic rewrite theories, allowing the user to specify different probabilistic ...

We investigate the usage of a history-based specification approach for concurrent and distributed systems. In particular, we compare two approaches on checking that those systems behave according to their specification. ...

This report investigates the possibilities of modeling OSLC Resources with Class Models, and also transforming these models into OSLC server and client code fragments that use these resources.

Publish/subscribe (pub/sub) is a popular communication paradigm in the design of largescale distributed systems. A provider of a pub/sub service (whether centralized, peer-assisted, or based on a federated organization of ...

Active Queue Management (AQM) design has again come into the spotlight of network operators, vendors and OS developers. This reflects the growing concern and sensitivity about the end-to-end latency perceived by today’s ...

RDF data transformations are transformations of RDF graphs to RDF graphs which preserve in different degree the data content in the source to the target. These transformation therefore give special attention to the data ...

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the code level of ...

This report extends our behavioral type and effect system for detecting dealocks in [8] by polymorphism and formalizing type inference (wrt. the lock types. Our inference is defined for a simple concurrent, first-order ...

In emergency intervention and rescue operations, the coordination and collaboration of the rescue personnel is highly important for the success of the mission. Data networks formed between the devices carried by the rescue ...

We present an effect based static analysis to calculate upper and lower bounds on the memory resource consumption in a transactional calculus. The calculus is a concurrent variant of Featherweight Java extended by transactional ...

Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. The ...

Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. ...

Risk analysis is an important tool for developers to establish the appropriate protection level of a system. Unfortunately, the shifting environment of components and component-based systems is not adequately addressed by ...

We study three timed extensions of Petri nets. We demonstrate methods for transforming these types of Petri nets into Real-Time Maude programs. This lays the groundwork for a timed Petri net analysis tool in which these ...

We propose a novel approach to the well-studied problem of making a nite, ordered sequence of decisions under uncertainty. Most existing work in this area concentrates on graphical representations of decision problems, ...

The aim of the workshop is to bring together practitioners and researchers from academia, industry and government to present and discuss ideas about: • How to deal with the complexity of software projects by multi-view ...

Feil nr (409) på tittelbladet. Skal være Research report nr 406.

In this paper, we propose a probabilistic extension of the Creol modeling language, called PCreol, for which we give the operational semantics in Probabilistic Rewrite Logic. We give details on the implementation of a ...

Biomolecular interaction data is an increasingly important bioinformatics dataset used to examine biological systems. However, these data are spread across multiple databases and expressed in disparate data structures and ...

Modular system development causes challenges for security and safety as upgraded subcomponents may interact with the system in unforeseen ways. Due to their lack of modularity, conventional risk analysis methods are poorly ...

We present a partial correctness proof system for ABS, an imperative, concurrent and object-oriented language which provides asynchronous communication model that is suitable for loosely coupled objects in the distributed ...

iRefIndex provides an index of protein interactions available in a number of primary interaction databases. This index allows the user to search for a protein and retrieve a non-redundant list of interactors for that ...

Double eigenvalues are not generic for matrices without any particular structure. A matrix depending linearly on a scalar parameter, A+ mu B, will however generically have double eigenvalues for some values of the parameter ...

Transactions are a high-level alternative for low-level concurrencycontrol mechanisms such as locks, semaphores, monitors. A recent proposal for integrating transactional features into programming languages is Transactional ...

UML sequence diagrams partially describe a system. We show how the description may be augmented with exceptions triggered by the violation of timing constraints and compare our approach to those of the UML 2.1 simple time ...

The work reported here is concerned with the definition of a logic (which we call CL) for reasoning about legal contracts. The report presents the syntax of the logic and the associated semantics. There are two semantics ...

Polygonal hybrid systems (SPDIs) are planar hybrid systems, whose dynamics are defined in terms of constant differential inclusions, one for each of a number of polygonal regions partitioning the plane. The reachability ...

The 2nd Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’08) is held in Malta. The aim of the workshop is to bring together researchers and practitioners working on language-based solutions ...

Creol is a high-level, object-oriented language for distributed systems, featuring active objects and asynchronous method calls. In this paper we present a behavioral interface speci cation language over communication trace ...

Mobile Ad-Hoc Networks (MANETs) are an important communication infrastructure to support emergency and rescue operations. To address the frequent disconnections and network partitions that might occur, we have developed a ...

Soft real-time requirements are often related to communication in distributed systems. Therefore it is interesting to understand how UML sequence diagrams can be used to specify such requirements. We propose a way of ...

In this report we explore aspect-oriented modeling for UML 2.0 sequence diagrams. We ensure that the aspect weaving is semantics-based by using a formal trace model for sequence diagrams. A major challenge is to handle ...

UML sequence diagrams is a specification language that has proved itself to be of great value in system development. When put to applications such as simulation, testing and other kinds of automated analysis there is a ...

Mobile Ad-Hoc Networks maintain information about reachable nodes in the routing table. In many application scenarios, human groups play an important role. This is visible at the network level as independent network ...

Current object-oriented approaches to distributed programs may be criticized in several respects. First, method calls are generally synchronous, which leads to much waiting in distributed and unstable networks. Second, the ...

This paper describes a technique for realizing a high-rank channel matrix in a line-of-sight (LOS) multiple-input multiple-output (MIMO) transmission scenario. This is beneficial for systems which are unable to make use ...

The integration of XML documents in object-oriented programming languages is becoming paramount with the advent of the use of Internet in new applications like web services. Such integration is not easy in general and ...

STAIRS is an approach to the compositional development of UML interactions, such as sequence diagrams and interaction overview diagrams. An important aspect of STAIRS is the ability to distinguish between underspecification ...

This paper formalizes the observable interface behavior of an concurrent, objectoriented language with futures and promises. The calculus captures the core of Creol, a language, featuring in particular asynchronous method ...

Having a sequence diagram specification and a computer system, we need to answer the question: Is the system compliant with the sequence diagram specification in the desired way? We present a procedure for answering this ...

Having a sequence diagram specification and a computer system, we need to answer the question: Is the system compliant with the sequence diagram specification in the desired way? We present a procedure for answering this ...

During the past decade, the telecommunication environment has evolved from single operator featuring voice services to multi-operator featuring a range of different types of services. Services are being provided today in ...

STAIRS is a method for the compositional development of interactions in the setting of UML 2.0. In addition to defining denotational trace semantics for the main aspects of interactions, STAIRS focuses on how interactions ...

The coordination and collaboration of the personnel from various organisations involved in a rescue operation is important for a successful operation. Data networks can facilitate effective collaboration by providing an ...

The throughput of a possible future fixed wireless access multiple-input multiple-output (MIMO) system operating at high frequencies is investigated. We extend our previous theoretical work on MIMO for line-of-sight (LOS) ...

This analysis of the audio quality of DAB has been made independently of the broadcasting companies and aims at balancing their information. Through measurement of the audio signal and through informal listening, we have ...

This paper presents a case study evaluating the use of STAIRS when specifying a system for connecting service providers and people requesting those services. As part of the case study, we give an example of how STAIRS may ...

Late binding allows flexible code reuse but complicates formal reasoning significantly, as a method call’s receiver class is not statically known. This is especially true when programs are incrementally developed by extending ...

STAIRS is an approach to the compositional development of sequence diagrams supporting the specification of mandatory as well as potential behavior. In order to express the necessary distinction between black-box and ...

Nondeterminism in specifications may be used for at least two different purposes. One is to express underspecification, which means that the specifier for the same environment behavior allows several alternative behaviors ...

The Ad Hoc Routing Protocol with Cellular Assistance is intended to be used for high-bandwidth streaming on a heterogeneous 3G-cellular and Ad Hoc IEEE 802.11 network architecture. This report describes the protocol in ...

Traditionally, availability has been seen as an atomic property asserting the average time a system is "up" or "down". In order to model and analyse the availability of computerised systems in a world where the dependency ...

We study two simple multiresoultion analyses and their stability in the L1-norm: Faber decomposition and C1 quadratic Hermite interpolation, both with nonuniform knot sequences. The use of the L1 norm is natural in many ...

We propose a semantic paradigm for component-based specification supporting the documentation of security risk behaviour. By security risk, we mean behaviour that constitutes a risk with regard to ICT security aspects, ...

The trends over the recent years show an increase in streaming media transported across the Internet in addition to al- ready abundant web traffic, increasing the need for distri- bution schemes that efficiently handle ...

In this paper, elements of network simulations are identified and defined to provide a clear terminology for discourse on network simulators. Then we identify the two stakeholders involved in conducting network simulation ...

In UML, the operator neg is used to specify negative, or unwanted, system behaviour. We agree that being able to specify negative behaviour is important. However, the UML neg is currently not wellsuited for this purpose, ...

Development of applications and protocols for wireless ad-hoc networks has always been a challenge. Spe-cific characteristics such as frequent topology changes due to nodes moving around, popping up or being turned off, ...

Mobile ad-hoc networks (MANETs) provide the technical platform for efficient information sharing in emergency and rescue operations. Some the data present on the scene is highly confidential and requires protection. However, ...

Real-Time Maude is a language and tool supporting the formal specification and analysis of realtime and hybrid systems. The specification formalism is based on rewriting logic, emphasizes generality and ease of specification, ...

In the following essay we shall describe models for the theory MINPAR, the theory for finite binary trees, described in Jervell [2003]. In particular we shall investigate non-standard models simpler than the one presented ...