TY - BOOK A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - Symbolic model generation for graph properties N2 - Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about graph properties. In particular, we want to be able to check automatically if a given graph property is satisfiable. Actually, in most application scenarios it is desirable to be able to explore graphs satisfying the graph property if they exist or even to get a complete and compact overview of the graphs satisfying the graph property. We show that the tableau-based reasoning method for graph properties as introduced by Lambers and Orejas paves the way for a symbolic model generation algorithm for graph properties. Graph properties are formulated in a dedicated logic making use of graphs and graph morphisms, which is equivalent to firstorder logic on graphs as introduced by Courcelle. Our parallelizable algorithm gradually generates a finite set of so-called symbolic models, where each symbolic model describes a set of finite graphs (i.e., finite models) satisfying the graph property. The set of symbolic models jointly describes all finite models for the graph property (complete) and does not describe any finite graph violating the graph property (sound). Moreover, no symbolic model is already covered by another one (compact). Finally, the algorithm is able to generate from each symbolic model a minimal finite model immediately and allows for an exploration of further finite models. The algorithm is implemented in the new tool AutoGraph. N2 - Graphen sind allgegenwärtig in der Informatik. Daher ist die Verfügbarkeit von Methoden zur Darstellung und Untersuchung von Grapheigenschaften in vielen Gebieten von großer Wichtigkeit. Insbesondere ist die vollautomatische Überprüfung von Grapheigenschaften auf Erfüllbarkeit von zentraler Bedeutung. Darüberhinaus ist es in vielen Anwendungsszenarien wünschenswert diejenigen Graphen geeignet aufzuzählen, die eine Grapheigenschaft erfüllen. Im Falle einer unendlich großen Anzahl von solchen Graphen ist ein kompletter und gleichzeitig kompakter Überblick über diese Graphen anzustreben. Wir zeigen, dass die Tableau-Methode für Grapheigenschaften von Lambers und Orejas den Weg für einen Algorithmus zur Generierung von symbolischen Modellen frei gemacht hat. Wir formulieren Grapheigenschaften hierbei in einer dedizierten Logik basierend auf Graphen und Graphmorphismen. Diese Logik ist äquivalent zu der First-Order Logic auf Graphen, wie sie von Courcelle eingeführt wurde. Unser parallelisierbarer Algorithmus bestimmt graduell eine endliche Menge von sogenannten symbolischen Modellen. Hierbei beschreibt jedes symbolische Modell eine Menge von endlichen Graphen, die die Grapheigenschaft erfüllen. Die symbolischen Modelle decken so gemeinsam alle endlichen Modelle ab, die die Grapheigenschaft erfüllen (Vollständigkeit) und beschreiben keine endlichen Graphen, die die Grapheigenschaft verletzen (Korrektheit). Außerdem wird kein symbolisches Modell von einem anderen abgedeckt (Kompaktheit). Letztlich ist der Algorithmus in der Lage aus jedem symbolischen Modell ein minimales endliches Modell zu extrahieren und weitere endliche Modelle abzuleiten. Der Algorithmus ist in dem neuen Werkzeug AutoGraph implementiert. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 115 KW - model generation KW - nested graph conditions KW - tableau method KW - graph transformation KW - satisfiabilitiy solving KW - Modellerzeugung KW - verschachtelte Graphbedingungen KW - Tableaumethode KW - Graphtransformation KW - Erfüllbarkeitsanalyse Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-103171 SN - 978-3-86956-396-1 SN - 1613-5652 SN - 2191-1665 IS - 115 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Klauck, Stefan A1 - Maschler, Fabian A1 - Tausche, Karsten T1 - Proceedings of the Fourth HPI Cloud Symposium "Operating the Cloud" 2016 N2 - Every year, the Hasso Plattner Institute (HPI) invites guests from industry and academia to a collaborative scientific workshop on the topic Every year, the Hasso Plattner Institute (HPI) invites guests from industry and academia to a collaborative scientific workshop on the topic "Operating the Cloud". Our goal is to provide a forum for the exchange of knowledge and experience between industry and academia. Co-located with the event is the HPI's Future SOC Lab day, which offers an additional attractive and conducive environment for scientific and industry related discussions. "Operating the Cloud" aims to be a platform for productive interactions of innovative ideas, visions, and upcoming technologies in the field of cloud operation and administration. On the occasion of this symposium we called for submissions of research papers and practitioner's reports. A compilation of the research papers realized during the fourth HPI cloud symposium "Operating the Cloud" 2016 are published in this proceedings. We thank the authors for exciting presentations and insights into their current work and research. Moreover, we look forward to more interesting submissions for the upcoming symposium later in the year. Every year, the Hasso Plattner Institute (HPI) invites guests from industry and academia to a collaborative scientific workshop on the topic "Operating the Cloud". Our goal is to provide a forum for the exchange of knowledge and experience between industry and academia. Co-located with the event is the HPI's Future SOC Lab day, which offers an additional attractive and conducive environment for scientific and industry related discussions. "Operating the Cloud" aims to be a platform for productive interactions of innovative ideas, visions, and upcoming technologies in the field of cloud operation and administration. N2 - Jedes Jahr lädt das Hasso-Plattner-Institut (HPI) Gäste aus der Industrie und der Wissenschaft zu einem kooperativen und wissenschaftlichen Workshop zum Thema Cloud Computing ein. Unser Ziel ist es, ein Forum für den Austausch von Wissen und Erfahrungen zwischen der Industrie und der Wissenschaft zu bieten. Parallel zur Veranstaltung findet der HPI Future SOC Lab Tag statt, der eine zusätzliche attraktive Umgebung für wissenschaftliche und branchenbezogene Diskussionen bietet. Der Workshop zielt darauf ab, eine Plattform für produktive Interaktionen von innovativen Ideen, Visionen und aufkommenden Technologien im Bereich von Cloud Computing zu bitten. Anlässlich dieses Symposiums fordern wir die Einreichung von Forschungsarbeiten und Erfahrungsberichte. Eine Zusammenstellung der im Rahmen des vierten HPI-Cloud-Symposiums "Operating the Cloud" 2016 angenommenen Forschungspapiere wird veröffentlicht. Wir danken den Autoren für spannende Vorträge und Einblicke in ihre aktuelle Arbeit und Forschung. Darüber hinaus freuen wir uns auf weitere interessante Einreichungen für das kommende Symposium im Laufe des Jahres. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 117 KW - cloud security KW - cloud storage KW - dependable computing KW - resource optimization KW - in-memory database KW - distribution algorithm KW - virtualization KW - Cloud-Speicher KW - Cloud-Sicherheit KW - zuverlässige Datenverarbeitung KW - Ressourcenoptimierung KW - In-Memory Datenbank KW - Verteilungsalgorithmen KW - Virtualisierung Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-394513 SN - 978-3-86956-401-2 SN - 1613-5652 SN - 2191-1665 IS - 117 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Dyck, Johannes A1 - Giese, Holger A1 - Lambers, Leen T1 - Automatic verification of behavior preservation at the transformation level for relational model transformation N2 - The correctness of model transformations is a crucial element for model-driven engineering of high quality software. In particular, behavior preservation is the most important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques either show that specific properties are preserved, or more generally and complex, they show some kind of behavioral equivalence or refinement between source and target model of the transformation. Both kinds of behavior preservation verification goals have been presented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach available at the transformation level, i.e. for all source and target models specified by the model transformation. In this report, we extend our results presented in [27] and outline a new sophisticated approach for the automatic verification of behavior preservation captured by bisimulation resp. simulation for model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we show that the behavior preservation problem can be reduced to invariant checking for graph transformation and that the resulting checking problem can be addressed by our own invariant checker even for a complex example where a sequence chart is transformed into communicating automata. We further discuss today's limitations of invariant checking for graph transformation and motivate further lines of future work in this direction. N2 - Die Korrektheit von Modelltransformationen ist von zentraler Wichtigkeit bei der Anwendung modellgetriebener Softwareentwicklung für die Entwicklung hochqualitativer Software. Insbesondere verhindert Verhaltensbewahrung als wichtigste Korrektheitseigenschaft die Entstehung semantischer Fehler während des modellgetriebenen Entwicklungsprozesses. Techniken zur Verifikation von Verhaltensbewahrung zeigen, dass bestimmte spezifische Eigenschaften bewahrt bleiben oder, im allgemeineren und komplexeren Fall, dass eine Form von Verhaltensäquivalenz oder Verhaltensverfeinerung zwischen Quell- und Zielmodell der Transformation besteht. Für beide Ansätze existieren automatisierte Werkzeuge für die Verifikation auf der Instanzebene, also zur Überprüfung konkreter Paare aus Quell- und Zielmodellen der Transformation. Allerdings existiert kein automatischer Verifikationsansatz, der auf der Transformationsebene arbeitet, also Aussagen zu allen Quell- und Zielmodellen einer Modelltransformation treffen kann. Dieser Bericht erweitert unsere Vorarbeit und Ergebnisse aus [27] und stellt einen neuen Ansatz zur automatischen Verifikation von Verhaltensbewahrung vor, der auf Bisimulation bzw. Simulation basiert. Dabei werden Modelltransformationen durch Triple-Graph-Grammatiken und Verhaltensdefinitionen mittels Graphtransformationsregeln beschrieben. Insbesondere weisen wir nach, dass das Problem der Verhaltensbewahrung durch Bisimulation auf Invariant-Checking für Graphtransformationssysteme reduziert werden kann und dass das entstehende Invariant-Checking-Problem für ein komplexes Beispiel durch unser Werkzeug zur Verifikation induktiver Invarianten gelöst werden kann. Das Beispiel beschreibt die Transformation von Sequenzdiagrammen in Systeme kommunizierender Automaten. Darüber hinaus diskutieren wir bestehende Einschränkungen von Invariant-Checking für Graphtransformationssysteme und Ansätze für zukünftige Arbeiten in diesem Bereich. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 112 KW - model transformation KW - behavior preservation KW - semantics preservation KW - relational model transformation KW - bisimulation KW - simulation KW - invariant checking KW - transformation level KW - behavioral equivalenc KW - behavioral refinement KW - behavioral abstraction KW - graph transformation systems KW - graph constraints KW - triple graph grammars KW - Modelltransformationen KW - Verhaltensbewahrung KW - relationale Modelltransformationen KW - Bisimulation KW - Simulation KW - Invariant-Checking KW - Transformationsebene KW - Verhaltensäquivalenz KW - Verhaltensverfeinerung KW - Verhaltensabstraktion KW - Graphtransformationssysteme KW - Graph-Constraints KW - Triple-Graph-Grammatiken Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-100279 SN - 978-3-86956-391-6 SN - 1613-5652 SN - 2191-1665 IS - 112 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Weyand, Christopher A1 - Chromik, Jonas A1 - Wolf, Lennard A1 - Kötte, Steffen A1 - Haase, Konstantin A1 - Felgentreff, Tim A1 - Lincke, Jens A1 - Hirschfeld, Robert T1 - Improving hosted continuous integration services T1 - Verbesserung gehosteter Dienste für kontinuierliche Integration N2 - Developing large software projects is a complicated task and can be demanding for developers. Continuous integration is common practice for reducing complexity. By integrating and testing changes often, changesets are kept small and therefore easily comprehensible. Travis CI is a service that offers continuous integration and continuous deployment in the cloud. Software projects are build, tested, and deployed using the Travis CI infrastructure without interrupting the development process. This report describes how Travis CI works, presents how time-driven, periodic building is implemented as well as how CI data visualization can be done, and proposes a way of dealing with dependency problems. N2 - Große Softwareprojekte zu entwickeln, ist eine komplizierte Aufgabe und fordernd für Entwickler. Kontinuierliche Integration ist eine geläufige Praxis zur Komplexitätsreduktion. Durch häufiges Integrieren und Testen werden Änderungen klein gehalten und sind daher übersichtlich. Travis CI ist ein Dienst, der kontinuierliche Integration und kontinuierliche Bereitstellung in der Cloud anbietet. Softwareprojekte werden auf der Travis CI Infrastruktur gebaut, getestet und bereitgestellt, ohne dass der Entwicklungsprozess unterbrochen wird. Dieser Bericht beschreibt, die Travis CI funktioniert, zeigt wie zeitgesteuertes, periodisches Bauen implentiert wurde, wie CI-Daten visualisiert werden können und schlägt ein Verfahren vor mit dem Abhängigkeitsprobleme gelöst werden können. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 108 KW - Travis CI KW - continuous integration KW - continuous testing KW - software tests KW - software architecture KW - periodic tasks KW - dependencies KW - visualization KW - Travis CI KW - kontinuierliche Integration KW - kontinuierliches Testen KW - Softwaretests KW - Softwarearchitektur KW - periodische Aufgaben KW - Abhängigkeiten KW - Visualisierung Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-94251 SN - 978-3-86956-377-0 SN - 1613-5652 SN - 2191-1665 IS - 108 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Tessenow, Philipp A1 - Felgentreff, Tim A1 - Bracha, Gilad A1 - Hirschfeld, Robert T1 - Extending a dynamic programming language and runtime environment with access control T1 - Verbesserung gehosteter Dienste für kontinuierliche Integration N2 - Complexity in software systems is a major factor driving development and maintenance costs. To master this complexity, software is divided into modules that can be developed and tested separately. In order to support this separation of modules, each module should provide a clean and concise public interface. Therefore, the ability to selectively hide functionality using access control is an important feature in a programming language intended for complex software systems. Software systems are increasingly distributed, adding not only to their inherent complexity, but also presenting security challenges. The object-capability approach addresses these challenges by defining language properties providing only minimal capabilities to objects. One programming language that is based on the object-capability approach is Newspeak, a dynamic programming language designed for modularity and security. The Newspeak specification describes access control as one of Newspeak’s properties, because it is a requirement for the object-capability approach. However, access control, as defined in the Newspeak specification, is currently not enforced in its implementation. This work introduces an access control implementation for Newspeak, enabling the security of object-capabilities and enhancing modularity. We describe our implementation of access control for Newspeak. We adapted the runtime environment, the reflective system, the compiler toolchain, and the virtual machine. Finally, we describe a migration strategy for the existing Newspeak code base, so that our access control implementation can be integrated with minimal effort. N2 - Die Komplexität von Softwaresystemen hat einen hohen Einfluss auf Entwicklungs- und Wartungskosten. Um diese Komplexität zu beherschen, werden Softwaresysteme in Module unterteilt, da diese getrennt leichter zu entwickeln und zu testen sind. Zur Unterstützung einer sauberen Aufteilung von Modulen, sollten sie minimale und klar definierte Schnittstellen haben. Dafür ist die Fähigkeit, mit Hilfe der Berechtigungskontrolle selektiv die Sichtbarkeit von Funktionen eines Modules einzuschränken, von zentraler Bedeutung. Softwaresysteme sind immer stärker verteilt, was nicht nur zu ihrer Komplexität beiträgt, sondern auch Herausforderungen bezüglich der Sicherheit mit sich bringt. Der Object-Capability-Ansatz löst genau jene Sicherheitsprobleme, da dadurch Programmobjekten nur die minimal erforderlichen Fähigkeiten gegeben werden. Für diesen Ansatz ist es essentiell, dass die öffentliche Schnittstelle eines Objektes durch Berechtigungskontrolle eingeschränkt werden kann. Auf dem Object-Capability-Ansatz basiert Newspeak, eine moderne und dynamische Programmiersprache, die besonders auf Sicherheit sowie Modularität Wert legt. Die Berechtigungskontrolle ist eine zentrale Funktion, sowohl für die Modularität, als auch für die Sicherheit von Newspeak. Daher ist sie auch in der Spezifikation von Newspeak definiert. Bisher gibt es allerdings keine Implementierung, die die Berechtigungskontrolle durchsetzt. In dieser Arbeit stellen wir eine Implementierung der Berechtigungskontrolle für Newspeak vor. Damit wird sowohl die Modularität von Newspeak Programmen verbessert, als auch die Sicherheit durch den Object-Capability-Ansatz erst ermöglicht. Wir beschreiben eine Implementierung der Berechtigungskontrolle für Newspeak und passen dabei die Laufzeitumgebung, die Reflexions- und Introspektionsmodule, den Compiler sowie die virtuelle Maschine an. Große Teile des Newspeak-Programmcodes müssen für die Benutzung der Berechtigungskontrolle angepasst werden. Durch eine Migration des Newspeak-Programmcodes wird es möglich, unsere Implementierung mit existierenden Newspeak-Programmen zu benutzen. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 107 KW - access control KW - virtual machines KW - Newspeak KW - dynamic programming languages KW - Zugriffskontrolle KW - virtuelle Maschinen KW - Newspeak KW - dynamische Programmiersprachen Y1 - 2016 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-92560 SN - 978-3-86956-373-2 SN - 1613-5652 SN - 2191-1665 IS - 107 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Beckmann, Tom A1 - Hildebrand, Justus A1 - Jaschek, Corinna A1 - Krebs, Eva A1 - Löser, Alexander A1 - Taeumel, Marcel A1 - Pape, Tobias A1 - Fister, Lasse A1 - Hirschfeld, Robert T1 - The font engineering platform T1 - Eine Plattform für Schriftarten BT - collaborative font creation in a self-supporting programming environment BT - kollaborative Schriftartgestaltung in Einer selbsttragenden Programmierumgebung N2 - Creating fonts is a complex task that requires expert knowledge in a variety of domains. Often, this knowledge is not held by a single person, but spread across a number of domain experts. A central concept needed for designing fonts is the glyph, an elemental symbol representing a readable character. Required domains include designing glyph shapes, engineering rules to combine glyphs for complex scripts and checking legibility. This process is most often iterative and requires communication in all directions. This report outlines a platform that aims to enhance the means of communication, describes our prototyping process, discusses complex font rendering and editing in a live environment and an approach to generate code based on a user’s live-edits. N2 - Die Erstellung von Schriften ist eine komplexe Aufgabe, die Expertenwissen aus einer Vielzahl von Bereichen erfordert. Oftmals liegt dieses Wissen nicht bei einer einzigen Person, sondern bei einer Reihe von Fachleuten. Ein zentrales Konzept für die Gestaltung von Schriften ist der Glyph, ein elementares Symbol, das ein einzelnes lesbares Zeichen darstellt. Zu den erforderlichen Domänen gehören das Entwerfen der Glyphenformen, technische Regeln zur Kombination von Glyphen für komplexe Skripte und das Prüfen der Lesbarkeit. Dieser Prozess ist meist iterativ und erfordert ständige Kommunikation zwischen den Experten. Dieser Bericht skizziert eine Plattform, die darauf abzielt, die Kommunikationswege zu verbessern, beschreibt unseren Prototyping-Prozess, diskutiert komplexe Schriftrendering und -bearbeitung in einer Echtzeitumgebung und einen Ansatz zur Generierung von Code basierend auf direkter Manipulation eines Nutzers. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 128 KW - smalltalk KW - squeak KW - font rendering KW - font engineering KW - prototyping KW - Smalltalk KW - Squeak KW - Schriftrendering KW - Schriftartgestaltung KW - Prototyping Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427487 SN - 978-3-86956-464-7 SN - 1613-5652 SN - 2191-1665 IS - 128 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - A logic-based incremental approach to graph repair T1 - Ein logikbasierter inkrementeller Ansatz für Graphreparatur N2 - Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update. N2 - Die Reparatur von Graphen, die Wiederherstellung der Konsistenz eines Graphen, spielt in mehreren Bereichen der Informatik und darüber hinaus eine herausragende Rolle: Beispielsweise wird in der modellgetriebenen Konstruktion die abstrakte Syntax von Modellen in der Regel mithilfe von Graphen kodiert. Flexible Bearbeitungsvorgänge erstellen vorübergehend inkonsistente Diagramme, die kein gültiges Modell darstellen, und erfordern daher eine Reparatur des Diagramms. Auf ähnliche Weise können Aktualisierungen in Graphendatenbanken - die das Speichern und Bearbeiten von Graphendaten verwalten - dazu führen, dass eine bestimmte Datenbank einige Integritätsbeschränkungen nicht erfüllt und auch eine Graphreparatur erforderlich macht. Wir präsentieren einen logikbasierten inkrementellen Ansatz für die Graphreparatur, der eine solide und vollständige (nach Beendigung) Übersicht über die am wenigsten verändernden Reparaturen erstellt. In unserem Kontext formalisieren wir die Konsistenz mittels sogenannten Graphbedingungen die der Logik erster Ordnung in Graphen entsprechen. Wir stellen zwei Arten von Reparaturalgorithmen vor: Die zustandsbasierte Reparatur stellt die Konsistenz unabhängig vom Verlauf der Graphänderung wieder her, während die deltabasierte (oder inkrementelle) Reparatur diesen Verlauf explizit berücksichtigt. Technisch stützen sich unsere Algorithmen auf einen vorhandenen Modellgenerierungsalgorithmus für in AutoGraph implementierte Graphbedingungen. Darüber hinaus verwendet der deltabasierte Ansatz das neue Konzept der Erfüllungsbäume (STs) zum Kodieren, ob und wie ein Graph eine Graphbedingung erfüllt. Wir zeigen dann, wie diese STs in Bezug auf eine Graphaktualisierung inkrementell manipuliert werden. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 126 KW - nested graph conditions KW - graph repair KW - model repair KW - consistency restoration KW - verschachtelte Graphbedingungen KW - Graphreparatur KW - Modellreparatur KW - Konsistenzrestauration Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427517 SN - 978-3-86956-462-3 SN - 1613-5652 SN - 2191-1665 IS - 126 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Giese, Holger A1 - Maximova, Maria A1 - Sakizloglou, Lucas A1 - Schneider, Sven T1 - Metric temporal graph logic over typed attributed graphs BT - extended version N2 - Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update. N2 - Verschiedene Arten typisierter attributierter Graphen können verwendet werden, um Systemzustände aus einem breiten Bereich von Domänen darzustellen. Für dynamische Systeme können etablierte Formalismen wie die Graphtransformation ein formales Modell für die Definition von Zustandssequenzen liefern. Wir betrachten den Fall, in dem zwischen Zustandsänderungen Zeit vergehen kann, und führen eine Logik ein, die als Metric Temporal Graph Logic (MTGL) bezeichnet wird, um über solche zeitgesteuerten Graphsequenzen zu urteilen. Mit dieser Logik drücken wir Eigenschaften der Struktur und der Attribute von Zuständen sowie des Auftretens von Zuständen über die Zeit aus, die durch ihre innere Struktur miteinander verbunden sind, was bisher keine formale Logik über Graphen präzise bewerkstelligt. Erstens, basierend auf zeitgesteuerten Graphsequenzen als Modelle für die Systemevolution, definieren wir MTGL, indem wir den zeitlichen Operator bis zu einer gewissen Zeitgrenze in die etablierte Logik von (verschachtelten) Graphbedingungen integrieren. Zweitens skizzieren wir, wie eine endliche zeitgesteuerte Diagrammsequenz als einzelnes Diagramm dargestellt werden kann, das alle zeitlichen Änderungen enthält (als Diagramm mit Verlauf bezeichnet), wie die Erfüllung von MTGL-Bedingungen für ein solches Diagramm definiert werden kann, und zeigen, dass beide Darstellungen dieselben MTGL-Bedingungen erfüllen. Drittens zeigen wir, wie MTGL-Bedingungen auf (verschachtelte) Diagrammbedingungen reduziert werden können, und zeigen anhand dieser Reduzierung, dass beide zugrunde liegenden Logiken gleichermaßen aussagekräftig sind. Schließlich stellen wir eine Erweiterung des Tools AutoGraph vor, mit der die Erfüllung der MTGL-Bedingungen für zeitgesteuerte Diagrammsequenzen überprüft werden kann, indem die Erfüllung der (verschachtelten) Diagrammbedingungen überprüft wird, die unter Verwendung der vorgeschlagenen Reduzierung für das Diagramm mit dem Verlauf entsprechend dem zeitgesteuerten Diagramm erhalten wurden. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 127 KW - typisierte attributierte Graphen KW - metrisch temporale Graph Logic KW - Spezifikation von gezeiteten Graph Transformationen KW - typed attributed graphs KW - metric termporal graph logic KW - specification of timed graph transformations Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427522 SN - 978-3-86956-463-0 SN - 1613-5652 SN - 2191-1665 IS - 127 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Weber, Benedikt T1 - Human pose estimation for decubitus prophylaxis T1 - Verwendung von Posenabschätzung zur Dekubitusprophylaxe N2 - Decubitus is one of the most relevant diseases in nursing and the most expensive to treat. It is caused by sustained pressure on tissue, so it particularly affects bed-bound patients. This work lays a foundation for pressure mattress-based decubitus prophylaxis by implementing a solution to the single-frame 2D Human Pose Estimation problem. For this, methods of Deep Learning are employed. Two approaches are examined, a coarse-to-fine Convolutional Neural Network for direct regression of joint coordinates and a U-Net for the derivation of probability distribution heatmaps. We conclude that training our models on a combined dataset of the publicly available Bodies at Rest and SLP data yields the best results. Furthermore, various preprocessing techniques are investigated, and a hyperparameter optimization is performed to discover an improved model architecture. Another finding indicates that the heatmap-based approach outperforms direct regression. This model achieves a mean per-joint position error of 9.11 cm for the Bodies at Rest data and 7.43 cm for the SLP data. We find that it generalizes well on data from mattresses other than those seen during training but has difficulties detecting the arms correctly. Additionally, we give a brief overview of the medical data annotation tool annoto we developed in the bachelor project and furthermore conclude that the Scrum framework and agile practices enhanced our development workflow. N2 - Dekubitus ist eine der relevantesten Krankheiten in der Krankenpflege und die kostspieligste in der Behandlung. Sie wird durch anhaltenden Druck auf Gewebe verursacht, betrifft also insbesondere bettlägerige Patienten. Diese Arbeit legt eine Grundlage für druckmatratzenbasierte Dekubitusprophylaxe, indem eine Lösung für das Einzelbild-2D-Posenabschätzungsproblem implementiert wird. Dafür werden Methoden des tiefen Lernens verwendet. Zwei Ansätze, basierend auf einem Gefalteten Neuronalen grob-zu-fein Netzwerk zur direkten Regression der Gelenkkoordinaten und auf einem U-Netzwerk zur Ableitung von Wahrscheinlichkeitsverteilungsbildern, werden untersucht. Wir schlussfolgern, dass das Training unserer Modelle auf einem kombinierten Datensatz, bestehend aus den frei verfügbaren Bodies at Rest und SLP Daten, die besten Ergebnisse liefert. Weiterhin werden diverse Vorverarbeitungsverfahren untersucht und eine Hyperparameteroptimierung zum Finden einer verbesserten Modellarchitektur durchgeführt. Der wahrscheinlichkeitsverteilungsbasierte Ansatz übertrifft die direkte Regression. Dieses Modell erreicht einen durchschnittlichen Pro-Gelenk-Positionsfehler von 9,11 cm auf den Bodies at Rest und von 7,43 cm auf den SLP Daten. Wir sehen, dass es gut auf Daten anderer als der im Training verwendeten Matratzen funktioniert, aber Schwierigkeiten mit der korrekten Erkennung der Arme hat. Weiterhin geben wir eine kurze Übersicht des medizinischen Datenannotationstools annoto, welches wir im Zusammenhang mit dem Bachelorprojekt entwickelt haben, und schlussfolgern außerdem, dass Scrum und agile Praktiken unseren Entwicklungsprozess verbessert haben. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 153 KW - machine learning KW - deep learning KW - convolutional neural networks KW - pose estimation KW - decubitus KW - telemedicine KW - maschinelles Lernen KW - tiefes Lernen KW - gefaltete neuronale Netze KW - Posenabschätzung KW - Dekubitus KW - Telemedizin Y1 - 2023 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-567196 SN - 978-3-86956-551-4 SN - 1613-5652 SN - 2191-1665 IS - 153 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK ED - Meinel, Christoph ED - Plattner, Hasso ED - Döllner, Jürgen Roland Friedrich ED - Weske, Mathias ED - Polze, Andreas ED - Hirschfeld, Robert ED - Naumann, Felix ED - Giese, Holger T1 - Proceedings of the 5th Ph.D. Retreat of the HPI Research School on Service-oriented Systems Engineering T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 46 Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-51472 SN - 978-3-86956-129-5 PB - Universitätsverlag Potsdam CY - Potsdam ER -