feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    UID:
    gbv_1824018002
    Format: 1 Online-Ressource (37 Seiten, 1723 KB) , Diagramme
    ISBN: 9783869565316
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 143
    Content: The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces and may be equipped with multiple or even infinitely many start graphs. To mitigate these problems, static analysis techniques based on finite symbolic representations of sets of states or paths thereof have been devised. We focus on the technique of k-induction for establishing invariants specified using graph conditions. To this end, k-induction generates symbolic paths backwards from a symbolic state representing a violation of a candidate invariant to gather information on how that violation could have been reached possibly obtaining contradictions to assumed invariants. However, GTSs where multiple agents regularly perform actions independently from each other cannot be analyzed using this technique as of now as the independence among backward steps may prevent the gathering of relevant knowledge altogether. In this paper, we extend k-induction to GTSs with multiple agents thereby supporting a wide range of additional GTSs. As a running example, we consider an unbounded number of shuttles driving on a large-scale track topology, which adjust their velocity to speed limits to avoid derailing. As central contribution, we develop pruning techniques based on causality and independence among backward steps and verify that k-induction remains sound under this adaptation as well as terminates in cases where it did not terminate before.
    Content: Die Analyse von Verhaltensmodellen wie Graphtransformationssystemen (GTSs) ist von zentraler Bedeutung im Model Driven Engineering. GTSs führen jedoch häufig zu unhanhabbar großen oder sogar unendlichen Zustandsräumen und können mit mehreren oder sogar unendlich vielen Startgraphen ausgestattet sein. Um diese Probleme abzumildern, wurden statische Analysetechniken entwickelt, die auf endlichen symbolischen Darstellungen von Mengen von Zuständen oder Pfaden basieren. Wir konzentrieren uns auf die Technik der k-Induktion zur Ermittlung von Invarianten, die unter Verwendung von Graphbedingungen spezifiziert sind. Zum Zweck der Analyse erzeugt die k-Induktion symbolische Rückwärtspfade von einem symbolischen Zustand, der eine Verletzung einer Kandidateninvariante darstellt, um Informationen darüber zu sammeln, wie diese Verletzung erreicht werden konnte, wodurch möglicherweise Widersprüche zu angenommenen Invarianten gefunden werden. GTSs, bei denen mehrere Agenten regelmäßig unabhängig voneinander Aktionen ausführen, können derzeit jedoch nicht mit dieser Technik analysiert werden, da die Unabhängigkeit zwischen Rückwärtsschritten das Sammeln von relevantem Wissen möglicherweise verhindert. In diesem Artikel erweitern wir die k-Induktion auf GTSs mit mehreren Agenten und unterstützen dadurch eine breite Palette zusätzlicher GTSs. Als laufendes Beispiel betrachten wir eine unbegrenzte Anzahl von Shuttles, die auf einer großen Tracktopologie fahren und die ihre Geschwindigkeit an Geschwindigkeitsbegrenzungen anpassen, um ein Entgleisen zu vermeiden. Als zentralen Beitrag entwickeln wir Beschneidungstechniken basierend auf Kausalität und Unabhängigkeit zwischen Rückwärtsschritten und verifizieren, dass die k-Induktion unter dieser Anpassung korrekt bleibt und in Fällen terminiert, in denen sie zuvor nicht terminierte.
    Additional Edition: Erscheint auch als Druck-Ausgabe Schneider, Sven Invariant analysis for multi-agent graph transformation systems using k-Induction Potsdam : Universitätsverlag Potsdam, 2022 ISBN 9783869565316
    Language: German
    Keywords: Mehragentensystem ; Transformation ; Forschungsbericht
    URL: Volltext  (kostenfrei)
    Author information: Schneider, Sven
    Author information: Maximova, Maria
    Author information: Giese, Holger 1970-
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 2
    UID:
    gbv_1807534987
    Format: 1 Online-Ressource (135 Seiten, 1916 KB) , Diagramme
    ISBN: 9783869565033
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 135
    Content: Language developers who design domain-specific languages or new language features need a way to make fast changes to language definitions. Those fast changes require immediate feedback. Also, it should be possible to parse the developed languages quickly to handle extensive sets of code. Parsing expression grammars provides an easy to understand method for language definitions. Packrat parsing is a method to parse grammars of this kind, but this method is unable to handle left-recursion properly. Existing solutions either partially rewrite left-recursive rules and partly forbid them, or use complex extensions to packrat parsing that are hard to understand and cost-intensive. We investigated methods to make parsing as fast as possible, using easy to follow algorithms while not losing the ability to make fast changes to grammars. We focused our efforts on two approaches. One is to start from an existing technique for limited left-recursion rewriting and enhance it to work for general left-recursive grammars. The second approach is to design a grammar compilation process to find left-recursion before parsing, and in this way, reduce computational costs wherever possible and generate ready to use parser classes.
    Content: Rewriting parsing expression grammars is a task that, if done in a general way, unveils a large number of cases such that any rewriting algorithm surpasses the complexity of other left-recursive parsing algorithms. Lookahead operators introduce this complexity. However, most languages have only little portions that are left-recursive and in virtually all cases, have no indirect or hidden left-recursion. This means that the distinction of left-recursive parts of grammars from components that are non-left-recursive holds great improvement potential for existing parsers. In this report, we list all the required steps for grammar rewriting to handle left-recursion, including grammar analysis, grammar rewriting itself, and syntax tree restructuring. Also, we describe the implementation of a parsing expression grammar framework in Squeak/Smalltalk and the possible interactions with the already existing parser Ohm/S. We quantitatively benchmarked this framework directing our focus on parsing time and the ability to use it in a live programming context. Compared with Ohm, we achieved massive parsing time improvements while preserving the ability to use our parser it as a live programming tool. The work is essential because, for one, we outlined the difficulties and complexity that come with grammar rewriting. Also, we removed the existing limitations that came with left-recursion by eliminating them before parsing.
    Additional Edition: Erscheint auch als Druck-Ausgabe Eichenroth, Friedrich Fast packrat parsing in a live programming environment Potsdam : Universitätsverlag Potsdam, 2022 ISBN 9783869565033
    Language: German
    Keywords: Programmierumgebung ; Domänenspezifische Sprache ; Forschungsbericht
    Author information: Hirschfeld, Robert 1969-
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 3
    UID:
    gbv_1032382406
    Format: Online-Ressource
    ISSN: 2191-1665
    Additional Edition: ISSN 1613-5652
    Additional Edition: Erscheint auch als Druck-Ausgabe Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Potsdam : Universitätsverlag, 2018 ISSN 1613-5652
    Former: Fortsetzung von Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam
    Language: German
    Keywords: Monografische Reihe
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 4
    UID:
    gbv_1854147846
    Format: 1 Online Ressource (vi, 144 Seiten, 28339 KB) , Illustrationen, Diagramme
    ISBN: 9783869565132
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 138
    Content: Design and Implementation of service-oriented architectures imposes a huge number of research questions from the fields of software engineering, system analysis and modeling, adaptability, and application integration. Component orientation and web services are two approaches for design and realization of complex web-based system. Both approaches allow for dynamic application adaptation as well as integration of enterprise application. Service-Oriented Systems Engineering represents a symbiosis of best practices in object-orientation, component-based development, distributed computing, and business process management. It provides integration of business and IT concerns. The annual Ph.D. Retreat of the Research School provides each member the opportunity to present his/her current state of their research and to give an outline of a prospective Ph.D. thesis. Due to the interdisciplinary structure of the research school, this technical report covers a wide range of topics. These include but are not limited to: Human Computer Interaction and Computer Vision as Service; Service-oriented Geovisualization Systems; Algorithm Engineering for Service-oriented Systems; Modeling and Verification of Self-adaptive Service-oriented Systems; Tools and Methods for Software Engineering in Service-oriented Systems; Security Engineering of Service-based IT Systems; Service-oriented Information Systems; Evolutionary Transition of Enterprise Applications to Service Orientation; Operating System Abstractions for Service-oriented Computing; and Services Specification, Composition, and Enactment.
    Content: Der Entwurf und die Realisierung dienstbasierender Architekturen wirft eine Vielzahl von Forschungsfragestellungen aus den Gebieten der Softwaretechnik, der Systemmodellierung und -analyse, sowie der Adaptierbarkeit und Integration von Applikationen auf. Komponentenorientierung und WebServices sind zwei Ansätze für den effizienten Entwurf und die Realisierung komplexer Web-basierender Systeme. Sie ermöglichen die Reaktion auf wechselnde Anforderungen ebenso, wie die Integration großer komplexer Softwaresysteme. "Service-Oriented Systems Engineering" repräsentiert die Symbiose bewährter Praktiken aus den Gebieten der Objektorientierung, der Komponentenprogrammierung, des verteilten Rechnen sowie der Geschäftsprozesse und berücksichtigt auch die Integration von Geschäftsanliegen und Informationstechnologien. Die Klausurtagung des Forschungskollegs "Service-oriented Systems Engineering" findet einmal jährlich statt und bietet allen Kollegiaten die Möglichkeit den Stand ihrer aktuellen Forschung darzulegen. Bedingt durch die Querschnittstruktur des Kollegs deckt dieser Bericht ein weites Spektrum aktueller Forschungsthemen ab. Dazu zählen unter anderem Human Computer Interaction and Computer Vision as Service; Service-oriented Geovisualization Systems; Algorithm Engineering for Service-oriented Systems; Modeling and Verification of Self-adaptive Service-oriented Systems; Tools and Methods for Software Engineering in Service-oriented Systems; Security Engineering of Service-based IT Systems; Service-oriented Information Systems; Evolutionary Transition of Enterprise Applications to Service Orientation; Operating System Abstractions for Service-oriented Computing; sowie Services Specification, Composition, and Enactment.
    Additional Edition: Erscheint auch als Druck-Ausgabe Meinel, Christoph, 1954 - Proceedings of the HPI research school on service-oriented systems engineering 2020 fall retreat Potsdam : Universitätsverlag Potsdam, 2023 ISBN 9783869565132
    Language: English
    Keywords: Forschungsbericht
    URL: Volltext  (kostenfrei)
    Author information: Meinel, Christoph 1954-
    Author information: Weske, Mathias 1963-
    Author information: Naumann, Felix 1971-
    Author information: Giese, Holger 1970-
    Author information: Rabl, Tilmann
    Author information: Uebernickel, Falk 1979-
    Author information: Lehmann, Anja
    Author information: Böttinger, Erwin
    Author information: Hölzle, Katharina 1974-
    Author information: Hirschfeld, Robert 1969-
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 5
    UID:
    gbv_1850649669
    Format: 1 Online Ressource (140 Seiten, 8132 KB) , Illustrationen, Diagramme
    ISBN: 9783869565507
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 152
    Content: The RailChain project designed, implemented, and experimentally evaluated a juridical recorder that is based on a distributed consensus protocol. That juridical blockchain recorder has been realized as distributed ledger on board the advanced TrainLab (ICE-TD 605 017) of Deutsche Bahn. For the project, a consortium consisting of DB Systel, Siemens, Siemens Mobility, the Hasso Plattner Institute for Digital Engineering, Technische Universität Braunschweig, TÜV Rheinland InterTraffic, and Spherity has been formed. These partners not only concentrated competencies in railway operation, computer science, regulation, and approval, but also combined experiences from industry, research from academia, and enthusiasm from startups. Distributed ledger technologies (DLTs) define distributed databases and express a digital protocol for transactions between business partners without the need for a trusted intermediary. The implementation of a blockchain with real-time requirements for the local network of a railway system (e.g., interlocking or train) allows to log data in the distributed system verifiably in real-time. For this, railway-specific assumptions can be leveraged to make modifications to standard blockchains protocols. EULYNX and OCORA (Open CCS On-board Reference Architecture) are parts of a future European reference architecture for control command and signalling (CCS, Reference CCS Architecture – RCA). Both architectural concepts outline heterogeneous IT systems with components from multiple manufacturers. Such systems introduce novel challenges for the approved and safety-relevant CCS of railways which were considered neither for road-side nor for on-board systems so far. Logging implementations, such as the common juridical recorder on vehicles, can no longer be realized as a central component of a single manufacturer. All centralized approaches are in question. The research project RailChain is funded by the mFUND program and gives practical evidence that distributed consensus protocols are a proper means to immutably (for legal purposes) store state information of many system components from multiple manufacturers. The results of RailChain have been published, prototypically implemented, and experimentally evaluated in large-scale field tests on the advanced TrainLab. At the same time, the project showed how RailChain can be integrated into the road-side and on-board architecture given by OCORA and EULYNX. Logged data can now be analysed sooner and also their trustworthiness is being increased. This enables, e.g., auditable predictive maintenance, because it is ensured that data is authentic and unmodified at any point in time
    Content: ensured that data is authentic and unmodified at any point in time. Das Projekt RailChain hat einen verteilten Juridical Recorder entworfen, implementiert und experimentell evaluiert, der auf einem echtzeitfähigen verteilten Konsensprotokoll basiert. Dieser Juridical Blockchain Recorder wurde als distributed ledger an Bord des advanced TrainLabs der Deutschen Bahn (ICE-TD 605 017) umgesetzt. Für das Projekt hat sich ein Konsortium aus DB Systel, Siemens, Siemens Mobility, dem Hasso-Plattner-Institut für Digital Engineering, der Technischen Universität Braunschweig, sowie TÜV Rheinland InterTraffic und Spherity formiert und dabei Kompetenzen aus den Bereichen Bahnbetrieb, Informatik und Zulassungswesen gebündelt. Die Partner kombinieren Erfahrungen aus der Industrie und die akademische Forschung mit der Aufbruchstimmung aus dem Start-Up-Umfeld. Distributed-Ledger-Technologien (DLTs) definieren verteilte Datenbanken und stellen ein digitales Protokoll für Transaktionen zwischen Geschäftspartnern dar, ohne dass ein Mittelsmann beteiligt sein müsste. Die Implementierung einer Blockchain mit Echtzeitanforderungen für das lokale Netzwerk einer Eisenbahnanlage (z. B. Stellwerk oder Zug) erlaubt es, die im verteilten System entstehenden Daten nachweislich in Echtzeit zu protokollieren. Dabei können eisenbahnspezifische Randbedingungen ausgenutzt werden, um Standard-Blockchain-Protokolle anzupassen. EULYNX und OCORA (Open CCS On-board Reference Architecture) sind Bestandteile einer zukünftigen europäischen Referenzarchitektur für das Leit- und Sicherungssystem (Reference CCS Architecture – RCA, Control Command and Signalling – CCS). Beide Architekturkonzepte skizzieren herstellerübergreifende, komponentenbasierende heterogene IT-Systeme. Solche Systeme bergen neue Herausforderungen, die bislang im Kontext der zugelassenen, sicherheitsrelevanten Leit- und Sicherungstechnik der Bahn weder strecken- noch fahrzeugseitig adressiert werden mussten. Logbuch-Implementierungen, wie der gängige Juridical Recorder auf Fahrzeugen, können nun nicht mehr als zentrale Systemkomponente eines einzelnen Herstellers umgesetzt werden. Alle zentralisierten Lösungsansätze sind in Frage gestellt. Das mFUND-geförderte Forschungsprojekt erbringt den praktischen Nachweis, dass Zustandsinformationen über eine Vielzahl von Systemkomponenten herstellerübergreifend und gerichtsfest mittels verteilten Konsensprotokollen gespeichert werden können. Ergebnisse von RailChain wurden publiziert, prototypisch implementiert und in großen Feldtests auf dem advanced TrainLab experimentell evaluiert. Gleichzeitig wurde aufgezeigt, wie sich RailChain in den mit OCORA und EULYNX vorgegebenen fahrzeug- und streckenseitigen Architekturentwurf integrieren lässt. Daten können dadurch zeitnaher ausgewertet werden und gleichzeitig wird ihre Vertrauenswürdigkeit erhöht. Dies ermöglicht u. a. nachvollziehbare zustandsorientierte Wartung, denn es kann jederzeit sichergestellt werden, dass die Daten authentisch sind und auch nicht verändert wurden.
    Additional Edition: Erscheint auch als Druck-Ausgabe Schwarzer, Ingo RailChain Potsdam : Universitätsverlag Potsdam, 2023 ISBN 9783869565507
    Language: English
    Keywords: Forschungsbericht
    URL: Volltext  (kostenfrei)
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 6
    UID:
    gbv_1880908468
    Format: 1 Online-Ressource (114 Seiten, 3217 KB) , Illustrationen, Diagramme
    ISBN: 9783869565248
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 142
    Content: This technical report presents the results of student projects which were prepared during the lecture “Operating Systems II” offered by the “Operating Systems and Middleware” group at HPI in the Summer term of 2020. The lecture covered ad- vanced aspects of operating system implementation and architecture on topics such as Virtualization, File Systems and Input/Output Systems. In addition to attending the lecture, the participating students were encouraged to gather practical experience by completing a project on a closely related topic over the course of the semester. The results of 10 selected exceptional projects are covered in this report. The students have completed hands-on projects on the topics of Operating System Design Concepts and Implementation, Hardware/Software Co-Design, Reverse Engineering, Quantum Computing, Static Source-Code Analysis, Operating Systems History, Application Binary Formats and more. It should be recognized that over the course of the semester all of these projects have achieved outstanding results which went far beyond the scope and the expec- tations of the lecture, and we would like to thank all participating students for their commitment and their effort in completing their respective projects, as well as their work on compiling this report.…
    Content: Dieser technische Bericht beschriebt die Ergebnisse der Projekte, welche im Rahmen der Lehrveranstaltung "Betriebssysteme II" on teilnehmenden Studierenden durchgeführt wurden. Die Lehrveranstaltung wurde von der "Betriebssysteme und Middleware" am HPI im Sommersemester 2020 durchgeführt und behandele fortgeschrittene Aspekte der Betriebssystemarchitektur und -Implementierung am Beispiel der Virtualisierung, der Dateisysteme und der Eingabe/Ausgabe (I/O) Systeme. Zusätzlich zu den Vorlesungen wurden die Studierenden angeleitet, durch die Durchführung eines begleitenden Projekts praktische Erfahrungen im Umgang mit den behandelten Themen zu sammeln. Die Ergebnisse von 10 ausgewählten, herausragenden Projekten werden in diesem Report vorgestellt. Die Studierenden haben unter anderem Projekte zu den Themen Betriebssystemdesign und -Implementierung, Hardware/Software Co-Design, Reverse Engineering, Quanten-Computing, Statische Quellcodeanalyse, Betriebssystemgeschichte, dem Binärformat von ausführbaren Dateien durchgeführt. Es ist anzuerkennen, dass alle teilnehmenden Studierenden im Verlauf des Semesters herausragende Ergebnisse erzielt haben, die weit über die Anforderungen der Lehrveranstaltung hinausgingen. Wir möchten uns bei allen teilnehmenden Studierenden für Ihren Einsatz bei der Durchführung der Projekte, sowie bei der Erstellung dieses Reports bedanken.
    Additional Edition: Erscheint auch als Druck-Ausgabe Operating systems II - student projects Potsdam : Universitätsverlag, 2023 ISBN 9783869565248
    Language: English
    Keywords: Forschungsbericht
    URL: Volltext  (kostenfrei)
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 7
    UID:
    gbv_1851540180
    Format: 1 Online Ressource (73 Seiten, 15322 KB) , Illustrationen, Diagramme
    ISBN: 9783869565514
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 153
    Content: 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.
    Content: 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 -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.
    Note: Literaturverzeichnis: Seite 51-58
    Additional Edition: Erscheint auch als Druck-Ausgabe Weber, Benedikt Human pose estimation for decubitus prophylaxis Potsdam : Universitätsverlag Potsdam, 2023 ISBN 9783869565514
    Language: English
    Keywords: Forschungsbericht
    URL: Volltext  (kostenfrei)
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 8
    UID:
    gbv_1789231957
    Format: 1 Online-Ressource (58 Seiten, 546 KB) , Illustrationen
    ISBN: 9783869565026
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 134
    Content: The formal modeling and analysis is of crucial importance for software development processes following the model based approach. We present the formalism of Interval Probabilistic Timed Graph Transformation Systems (IPTGTSs) as a high-level modeling language. This language supports structure dynamics (based on graph transformation), timed behavior (based on clocks, guards, resets, and invariants as in Timed Automata (TA)), and interval probabilistic behavior (based on Discrete Interval Probability Distributions). That is, for the probabilistic behavior, the modeler using IPTGTSs does not need to provide precise probabilities, which are often impossible to obtain, but rather provides a probability range instead from which a precise probability is chosen nondeterministically. In fact, this feature on capturing probabilistic behavior distinguishes IPTGTSs from Probabilistic Timed Graph Transformation Systems (PTGTSs) presented earlier. Following earlier work on Interval Probabilistic Timed Automata (IPTA) and PTGTSs, we also provide an analysis tool chain for IPTGTSs based on inter-formalism transformations. In particular, we provide in our tool AutoGraph a translation of IPTGTSs to IPTA and rely on a mapping of IPTA to Probabilistic Timed Automata (PTA) to allow for the usage of the Prism model checker. The tool Prism can then be used to analyze the resulting PTA w.r.t. probabilistic real-time queries asking for worst-case and best-case probabilities to reach a certain set of target states in a given amount of time.
    Content: Die formale Modellierung und Analyse ist für Softwareentwicklungsprozesse nach dem modellbasierten Ansatz von entscheidender Bedeutung. Wir präsentieren den Formalismus von Interval Probabilistic Timed Graph Transformation Systems (IPTGTS) als Modellierungssprache auf hoher abstrakter Ebene. Diese Sprache unterstützt Strukturdynamik (basierend auf Graphtransformation), zeitgesteuertes Verhalten (basierend auf Clocks, Guards, Resets und Invarianten wie in Timed Automata (TA)) und intervallwahrscheinliches Verhalten (basierend auf diskreten Intervallwahrscheinlichkeitsverteilungen). Das heißt, für das probabilistische Verhalten muss der Modellierer, der IPTGTS verwendet, keine genauen Wahrscheinlichkeiten bereitstellen, die oft nicht zu bestimmen sind, sondern stattdessen einen Wahrscheinlichkeitsbereich bereitstellen, aus dem eine genaue Wahrscheinlichkeit nichtdeterministisch ausgewählt wird. Tatsächlich unterscheidet diese Funktion zur Erfassung des probabilistischen Verhaltens IPTGTS von den zuvor vorgestellten PTGTS (Probabilistic Timed Graph Transformation Systems). Nach früheren Arbeiten zu Intervall Probabilistic Timed Automata (IPTA) und PTGTS bieten wir auch eine Analyse-Toolkette für IPTGTS, die auf Interformalismus-Transformationen basiert. Insbesondere bieten wir in unserem Tool AutoGraph eine Übersetzung von IPTGTSs in IPTA und stützen uns auf eine Zuordnung von IPTA zu probabilistischen zeitgesteuerten Automaten (PTA), um die Verwendung des Prism-Modellprüfers zu ermöglichen. Das Werkzeug Prism kann dann verwendet werden, um den resultierenden PTA bezüglich probabilistische Echtzeitabfragen (in denen nach Worst-Case- und Best-Case-Wahrscheinlichkeiten gefragt wird, um einen bestimmten Satz von Zielzuständen in einem bestimmten Zeitraum zu erreichen) zu analysieren.
    Additional Edition: Erscheint auch als Druck-Ausgabe Maximova, Maria Interval probabilistic timed graph transformation systems Potsdam : Universitätsverlag Potsdam, 2021 ISBN 9783869565026
    Language: English
    Keywords: Verteiltes System ; Eingebettetes System ; Wahrscheinlichkeitsverteilung ; Zeitbehafteter Automat ; Forschungsbericht
    URL: Volltext  (kostenfrei)
    Author information: Schneider, Sven
    Author information: Maximova, Maria
    Author information: Giese, Holger 1970-
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 9
    UID:
    gbv_1794958940
    Format: 1 Online-Ressource (53 Seiten, 1843 KB) , Illustrationen
    ISBN: 9783869565019
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 133
    Content: The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on e.g. concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of probabilistic timed graph transformation systems is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces. We present an approach for the analysis of large scale systems modeled as probabilistic timed graph transformation systems by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large scale system under analysis. We consider a running example in which we model shuttles driving on tracks of a large scale topology and for which we verify that shuttles never collide and are unlikely to execute emergency brakes. In our evaluation, we apply an implementation of our approach to the running example.
    Content: Die Analyse von Verhaltensmodellen ist für cyber-physikalische Systeme von hoher Bedeutung, da die Systeme häufig komplexes Verhalten umfassen, das z.B. parallele Komponenten mit gegenseitigem Ausschluss oder probabilistischen Fehlern bei Bedarf umfasst. Der regelbasierte Formalismus probabilistischer zeitgesteuerter Graphtransformationssysteme ist eine geeignete Wahl, wenn die Modelle, die Zustände des Systems darstellen, als Graphen verstanden werden können und zeitgesteuertes und probabilistisches Verhalten wichtig ist. Modelchecking von PTGTSs ist jedoch auf Systeme mit relativ kleinen Zustandsräumen beschränkt. Wir präsentieren einen Ansatz zur Analyse von Großsystemen, die als probabilistische zeitgesteuerte Graphtransformationssysteme modelliert wurden, indem ihre Zustandsräume systematisch in überschaubare Fragmente zerlegt werden. Um qualitative und quantitative Analyseergebnisse für ein Großsystem zu erhalten, überprüfen wir, ob die für seine Fragmente erhaltenen Ergebnisse als Überannäherungen für die entsprechenden Ergebnisse des Großsystems dienen. Unser Ansatz ermöglicht es daher, Verstöße gegen qualitative und quantitative Sicherheitseigenschaften für das untersuchte Großsystem zu erkennen. Wir betrachten ein Beispiel, in dem wir Shuttles modellieren, die auf Gleisen einer großen Topologie fahren, und für die wir überprüfen, dass Shuttles niemals kollidieren und wahrscheinlich keine Notbremsungen ausführen. In unserer Auswertung wenden wir eine Implementierung unseres Ansatzes auf das Beispiel an.
    Additional Edition: Erscheint auch als Druck-Ausgabe Maximova, Maria Compositional analysis of probabilistic timed graph transformation systems Potsdam : Universitätsverlag Potsdam, 2021 ISBN 9783869565019
    Language: English
    Keywords: Verteiltes System ; Eingebettetes System ; Wahrscheinlichkeitsverteilung ; Zeitbehafteter Automat ; Forschungsbericht
    Author information: Schneider, Sven
    Author information: Maximova, Maria
    Author information: Giese, Holger 1970-
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 10
    UID:
    gbv_1039864767
    Format: 1 Online-Ressource (29 Seiten, 1802 KB) , Illustrationen, Diagramme
    Series Statement: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam Nr. 123
    Content: Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences.
    Content: Verschiedene Arten von getypten attributierten Graphen werden benutzt, um Zustände von Systemen in vielen unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein formales Model, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten den erweiterten Fall von solchen Sequenzen, in dem Zeit zwischen zwei verschiedenen Systemzuständen vergeht, und führen eine Logik ein, um solche Sequenzen zu beschreiben. Mit dieser Logik drücken wir zum einen Eigenschaften über die Struktur und die Attribute von Zuständen aus und beschreiben zum anderen temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Solche Eigenschaften können bisher von keiner der existierenden Logiken auf Graphen vergleichbar darstellt werden. Erstens führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, wenn nötig, seiner Löschung versehen. Zweitens definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die wohl-etablierte Logik der verschachtelten Graphbedingungen integrieren. Drittens beweisen wir, dass unsere Logik gleich ausdrucksmächtig ist, wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Zuletzt erlaubt uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen zu führen.
    Additional Edition: ISBN 9783869564333
    Additional Edition: Erscheint auch als Druck-Ausgabe Giese, Holger, 1970 - Metric temporal graph logic over typed attributed graphs [Potsdam] : Universitätsverlag Potsdam, 2018 ISBN 9783869564333
    Language: English
    Keywords: Graph ; Forschungsbericht
    Author information: Schneider, Sven
    Author information: Giese, Holger 1970-
    Author information: Maximova, Maria
    Author information: Sakizloglou, Lucas
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. Further information can be found on the KOBV privacy pages