You are here

Home › Research ›

Projects

SALT – Structured Assertion Language for Temporal Logic

SALT stands for Smart Assertion Language for Temporal Logic. It is a temporal specification language that is similar in spirit to programming languages like C and Java and is therefore well suited for software engineers. Its expressiveness, on the other side, covers LTL, or, when the realtime operators of SALT are used, covers TLTL (Timed LTL).

Integration of Runtime Verification into Metamodeling

Runtime verification is an approach growing in popularity to verify the correctness of complex and distributed systems by monitoring their executions. Domain Specific Modeling Languages are a technique used for specifying such systems in an abstract way, but still close to the solution domain. We aim at integrating runtime verification and domain specific modeling into the development process of complex systems. Such integration is achieved by linking the elements of the system model with the atomic propositions of the temporal correctness properties used to specify monitors.

IT für Lübecker Schulen

Das Institut für Softwaretechnik und Programmiersprachen (ISP) der Universität zu Lübeck hat die Hansestadt Lübeck beraten, wie sie als Schulträger ihrer Verpflichtung nachkommen kann, für die Ausstattung und den Unterhalt von pädagogischer IT in den Schulen zu sorgen.

LEGO® meets RV—Distributed Runtime Verification on Embedded Systems

LEGO® meets RV The project LEGO® meets RV is an implementation of distributed runtime verification for LEGO® Mindstorms NXT robots. The robots are programmed using the C-dialect Not eXactly C (NXC). In the source code you can add special comments which are parsed by the preprocessor developed in this project and freely available on this page. These special comments contain correctness properties which will be verified by monitors generated out of the annotations. To specify the properties the Distributed Temporal Logic (DTL) is used. This logic is based on LTL but contains the new @-operator which specifies on which agent a subformula should be evaluated.

WS-RV—Runtime Verification for Web Services

WS-RV is a framework to integrate Runtime Monitoring seamlessly into Service Oriented Architectures and other environments using XML Web Services as middleware. WS-RV is based on the Java API for XML Web Services (JAX-WS). The basic concepts of the framework are Interceptors, Monitoring Services and Monitors. Interceptors can be attached to the Java Webservices Stack and send messages to Monitoring Services. Monitoring Services can be deployed to arbitrary Web Service Containers and mangage serveral monitors. Monitors check the observed sequence of messages with respect to some temporal correctness properties. These properties are specified in a high level language based on XML and are automatically synthesised during initialisation of the corresponding monitoring service.

ZeLiM

The future of energy production lies within the use of renewable energy sources. The storage of such energy can make a big contribution to utilising this renewable energy. The ZeLiM project (Zentralisiertes Lithium-Speicher-Monitoring - Centralised Lithium Storage Monitoring) is aimed at developing a computer supported system for centralised monitoring, configuration and management of decentralised energy storage devices.

Passat Accommodation Scheduling System

Passat Accommodation Scheduling System The goal of the project Passat was to design and build a ready to use accom- modation scheduling system for the historic ship Passat. Most of the rooms aboard the ship can be rented for events or to stay overnight. The ship is kept by the administration of the city of Lübeck where this was done using pen and paper when this project began. Project Passat started as a masters case study and is currently continued launching and maintaining the software for the administration of the city of Lübeck. In the scope of a bachelor thesis an extended statistics module for the software is being developed.

SmartCAR – Masters Case Study

In the course of this case study, the challenge was to develop a car computer, that facilitates energy saving, and itself works in a power-efficient way. A framework to link vehicle and external agents (for example smartphones) was developed. This framework is based upon various embedded hardware platforms that are attached to the onboard control units of the car, and it provides services to external and internal agents, such as the on-board computer Interfaces are provided to allow application developers to provide custom, helpful applications

Flens – Runtime Verification for Clojure

Flens is a runtime verification framework written in the Clojure programming language. Flens is an acronym for "Functional logic evaluation and notification system". With Flens assistance it is possible to specify correctness properties for Clojure programs which are checked at runtime. From a user’s point of view, Flens thus consists of two major functional components

Stream-based System Design

Ein Strom modelliert die Geschichte der Kommunikation über einen uni-direktionalen Kanal, d.h. die Sequenz von Nachrichten auf diesem Kanal als einem Teil eines verteilten Systems. Strom-verarbeitende Funktionen, die Eingabe-Ströme auf Ausgabe-Ströme abbilden, modellieren die interaktiven Komponenten eines solchen verteilten Systems. In diesem Umfeld werden Verfeinerungstechniken für den schrittweisen Entwurf von Komponenten entwickelt. Kontakt: Annette Stümpel

Pages

Subscribe to Projects