Indoor location is a growing topic for hospitals, retirement homes and in case of emergency. For the resource efficient (indoor) positioning of mobile individuals an optimized distribution of the used sensors is necessary. The placement of beacons (sensors) in a building (indoor positioning) can be a difficult and laborious task, especially if done by hand. Multiple researchers already tried to tackle this problem using different algorithms and under the consideration of distinct use cases. However, none of the currently known methods incorporate constraint programming by using only Boolean variables. In this paper we tried to develop a new method for an efficient placement of Bluetooth Low Energy (BLE) beacons in an indoor scenario. More specifically, we try to optimize the beacons for a trilateration algorithm used for indoor positioning. This algorithm requires that three beacons should be in range for every possible position in the building. In a next step the initially calculated beacon positions are further optimized. This is done by trying to reduce the number of beacons used. Afterwards we evaluate the quality of the beacon placements by comparing it against a manually optimized beacon placement and evaluating it in an existing building by checking the quality of multiple sample positions.

This paper describes a new approach on optimization of regular constraint satisfaction problems (rCSPs) using an auxiliary constraint satisfaction optimization problem (CSOP) that detects areas with a potentially high number of conflicts. The purpose of this approach is to remove conflicts by the combination of regular constraints with intersection and concatenation of their underlying deterministic finite automatons (DFAs). This, eventually, often allows to significantly speed-up the solution process of the original rCSP.

This paper describes a new approach to decompose constraint satisfaction problems (CSPs) using an auxiliary constraint satisfaction optimization problem (CSOP) that detects sub-CSPs which share only few common variables. The purpose of this approach is to find sub-CSPs which can be solved in parallel and combined to a complete solution of the original CSP. Therefore, our decomposition approach has two goals: 1. to evenly balance the workload distribution over all cores and solve the partial CSPs as fast as possible and 2. to minimize the number of shared variables to make the join process of the solutions as fast as possible.

In this work we present a verification framework for applications for the embedded system operating system Contiki, based on the software model checking tool CBMC. A challenge when verifying such systems is the modeling of the hardware environment, especially the handling of interrupts. After an introduction to the Contiki system, we discuss approaches to model interrupts at the level of hardware independent C source code and present a new modeling approach for periodically occurring interrupts. Finally, verification results for these approaches based on different Contiki applications are presented.

This paper presents the concept and realization of configurable resource models as extension of a treatment scheduling system for users in the medical sector. Our approach aims to ease the handling of automated treatment scheduling by domain experts without the immediate assistance of IT-experts. Configurable resource models were integrated into our automated treatment planning system for medical facilities and support a user-friendly configuration of resources such as specialized treatment rooms, medical devices, or medical staff. In our approach, treatment process models are defined in the BPMN workflow-language by the domain experts. The new concept of configurable resource models allows the end-user to interactively describe the available resources in their environment. These descriptions (i.e. configurable resource objects or CDOs) can then be linked to activities specified in the treatment models. Together, CDOs and the BPMN treatment models are automatically transformed into CSPs, i.e. mathematical descriptions which can be solved by constraint solvers, thus yielding optimal treatment plans.

Verification of embedded systems is a challenge due to the tight combination of hardware and software. We present an approach on the automatic verification of embedded system applications for the operating system Contiki using a standard bounded model checking tool for software. By using an operating system a higher abstraction level to hardware is possible. Our approach is therefore easily applicable for the verification of different hardware platforms.

Abstract Combining a set of existing constraint solvers into an integrated system of cooperating solvers is a useful and economic principle to solve hybrid constraint problems. In this paper we show that this approach can also be used to integrate different language paradigms into a unified framework. Furthermore, we study the syntactic, semantic and operational impacts of this idea for the amalgamation of declarative and constraint programming.