Projects

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.

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.

OR.NET—Safe Interconnection of Medical Devices in Operation Rooms

OR.NET - Safe Interconnection of Medical Devices in Operation Rooms Nowadays in Europe the interconnection of medical devices in an operating room is almost always limited to devices from a single manufacturer or the clinic operator assumes the role of a manufacturer. This is partially due to technical restrictions but especially due to the legal requirements needed in the medical domain. These legal requirements impose that a complete system-of-systems has been successfully tested and certified before its use in an operating room. The OR.NET project focuses on the safe, secure and dynamic interconnection of medical devices from different manufacturers in an operating room.

CONIRAS – Kontinuierliche nicht-intrusive Laufzeitanalyse von SoCs

CONIRAS – Kontinuierliche nicht-intrusive Laufzeitanalyse von SoCsDer Einsatz von Multicore-Prozessoren in eingebetten Systemen erfordert umfassende Beobachtungsmöglichkeiten, um die mit besonderer Wahrscheinlichkeit auftretenden nichtdeterministischen Fehler zu verstehen und die zugrunde liegenden Defekte beseitigen zu können. Die dazu nötige Erfassung von Systemzuständen ist bei bisher verfügbaren Emulationssystemen nur eingeschränkt möglich, da deren Möglichkeiten zur Erfassung und Auswertung von Trace-Daten vielen qualitativen und quantitativen Ansprüchen nicht genügen. Ziel dieses Projektes ist es daher, mit Hilfe eines neuartigen Debugging-Systems Trace-Daten in Echtzeit zu erfassen und im Hinblick auf ausgewählte Fragestellungen auszuwerten. Dazu sollen eine FPGA-Plattform und passende spezialisierte Synthese-Werkzeuge entwickelt werden.

jUnitRV—Temporal Assertions for jUnit

jUnitRV
jUnitRV is a tool extending the unit testing framework jUnit by runtime verification capabilities. It provides a new annotation @Monitors listing monitors classes that obseve the test case execution and verify temporal assertions. jUnit’s concept of assert-based verification is extended towards checking properties of complete execution paths.

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.

LamaConv—Logics and Automata Converter Library

LamaConv—Logics and Automata Converter LibraryLamaConv (internal code name RltlConv) is a Java library that is capable of translating expressions in temporal logics into equivalent automata and to generate monitors out of these automata. These monitors can be used for runtime verification and model checking.

Green Navigation

Green Navigation Green Navigation is a prototypic system to compute energy-optimal routes and to predict the remaining crusing range for electric vehicles. It consists of a central server that carries out the computations and various client front-ends accessing the services provided by this server. It uses freely available OpenStreetMap geospatial data and NASA altitude maps.

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.

Mufin–Runtime Monitoring with Union-Find Structures

Mufin–Runtime Monitoring with Union-Find StructuresMufin is a tool for runtime verification of object-oriented software system. It uses a novel algorithm for monitoring the individual behaviour and interaction of an unbounded number of runtime objects. This allows for evaluating complex correctness properties that take runtime data in terms of object identities into account. In particular, the underlying formal model can express hierarchical interdependencies of individual objects.

Pages

Subscribe to Projects