Projects

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.

SecurePort - Sicherheit im Seehafen Lübeck

Als Betreiber der öffentlichen Lübecker Häfen ist die LHG für die Sicherheit im Hafen und der eingesetzten Informationstechnischen Lösungen verantwortlich. Mit Hilfe von innovativen IT-Lösungen möchte die LHG im Umfeld der Sicherheit automatisieren, Lücken schließen, die Sicherheit weiter verbessern und die umfangreichen gesetzlichen Anforderungen erfüllt werden.  Zudem zielt die LHG darauf ab, Vorreiter im Einsatz von Flug- und Unterwasserdrohen im Hafenumfeld zu sein. Gemeinsam mit den Projektpartnern sollen die Rahmenbedingungen geschaffen, sowie geeignete Hardware und Anwendungsfälle entwickelt werden.

RoRo-Hafen-4.0 – Durchführbarkeitsstudie RoRo-Hafen-4.0

In Anlehnung an „Industrie 4.0“ soll die Studie zur Plattform „RoRo-Hafen-4.0“ die Steuerung und Organisation der gesamten Transportketten über einen RoRo-Hafen, der Lübecker Hafengesellschaft mbH, integrieren. Dies betrifft den gesamten Transportlebenszyklus, von der Quelle bis zum Ziel, und orientiert sich an den individuellen Wünschen von Verladern und Empfängern. Zudem soll eine unternehmensübergreifende Vernetzung aller Instanzen stattfinden. Dabei ist über die informationstechnische Vernetzung hinausgehend vor allem eine online basierte, integrierte und kooperative Disposition aller Prozesse angestrebt, die dort mit den internen Produktionslogistikketten verknüpft werden kann.

COEMS – Continuous Observation of Embedded Multicore Systems

Within COEMS, a novel platform for online monitoring of multicore systems is developed. It gives insight to the system’s behaviour without affecting it. This insight is crucial to detect non-deterministic failures as for example caused by race conditions and access to inconsistent data.

ARAMiS II – Debugging, Integration und Test für sicherheitskritische Multicore-Systeme

Im Rahmen des Projektes ARAMiS II werden Entwicklungsprozesse, -werkzeuge und Plattformen für den effizienten Einsatz von Multicore-Technologie analysiert und entwickelt. In enger Zusammenarbeit mit dem Partner Accemic entwickelt das ISP moderne Runtime-Verification-Techniken für Multicore-Plattformen.

Software Development Kit for the Open Surgical Communication Protocol

We are developing a software development kit (SDK) for the Open Surgical Communication Protocol (OSCP) that supports the development of interconnected medical devices according to the recent IEEE 11073 standards for interoperable medical device communication. Our tool, the OSCP Device Modeler, allows the specification of temporal assertions for the respective data streams of the systems and generates automatically corresponding monitors that may be used during testing, but also during the application in field to ensure adherence to the interface specification. A further tool, the OSCP Swiss Army Knife, allows subscribing to the services provided via the interfaces of the system under development and thereby supports its debugging.

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.

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.

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.

Pages

Subscribe to Projects