Funktionelle Ansätze zum Entwurf der diskreten Seite von Hybridsystemen

Question

Ich arbeite an der Entwicklung von Steuerungen für Hybridsysteme in Haskell.

FRP-Bibliotheken (derzeit verwende ich netwire, aber es gibt einige gute und viele interessante Forschung über zukünftige) bieten eine großartige Lösung für die zeitkontinuierliche Seite des Problems. Wenn Sie sie mit Signalnamen, Dimensionen, bevorzugten Einheiten usw. erweitern, erhalten Sie ein System, das Modularität besitzt, selbstbeschreibend ist und einen direkten Weg zum Vertrauen in die Korrektheit bietet.

Ich bin auf der Suche nach Informationen, Folklore oder Papiere, die ähnliche Eigenschaften für die zeitdiskrete Seite bieten. In gewissem Sinne ist das Problem viel einfacher, Zustandsautomaten sind gut untersucht und einfach. In anderer Hinsicht ist es schwieriger, ich werde kurz erklären, wie.

Korrektheit ist offensichtlich das Wichtigste, und zum Glück ist es auch einfach.

Selbstbeschreibung ist eher ein Problem. Sie möchten, dass der Controller nicht nur im richtigen Zustand ist, sondern Ihnen sagen kann, in welchem ​​Zustand er ist. Auch wie er dort angekommen ist. Und wohin es als nächstes gehen könnte. So können Sie Namen auf alles ausrichten, und es funktioniert, aber es widerspricht etwas mit Modularität. Sie möchten auch komplexe diskrete Zeitverhalten aus einfacheren bauen können. Aber wenn Sie das System fragen, in welchem ​​Zustand es sich befindet, ist im Allgemeinen die High-Level-Antwort interessanter (oder zumindest so interessant) wie die Low-Level-Antwort. Wie bekommst du das sauber? Ich habe ein paar naive Ansätze ausprobiert und mich ein wenig auf Spaghetti eingelassen, aber es scheint, dass es elegante Lösungen geben muss.

Ein weiteres Problem, das ich mit Selbstbeschreibung hatte, ist, dass ich eine Liste von selbstbeschreibenden Bedingungen haben möchte (im Allgemeinen Vergleiche: war es 10 Sekunden? Bin ich innerhalb von 3 Fuß vom nächsten Wegpunkt?) die Batterieleistung unter 15%? usw.), die überwacht werden, was den nächsten Zustandsübergang auslösen könnte. Es gibt knifflige Fragen darüber, was hier überhaupt die wünschenswerte Semantik ist, da es so aussieht, als würden einige dieser Ereignisse "von unten" besser behandelt (zB erwartete Abbruchbedingungen von jedem niedrigen Level-Schritt) und einige "von oben" "(zB Geräteausfallerkennung, Geofencing, ...). Dies kann zu Spaghetti führen, selbst wenn Sie das Ziel der Selbstbeschreibung entspannen.

Zusätzlich zur Diagnose können genaue Selbstbeschreibungsinformationen hier auch für die abstrakte Interpretation sehr nützlich sein, indem der Zustand des Systems in die Zukunft projiziert wird, indem man rät, welche Ereignisse wahrscheinlich wann auftreten. Viele der Ereignisbedingungen führen zu ziemlich einfachen Vermutungen (z. B. Verwenden der Geschwindigkeit, Kraftstoffverbrauchsrate, Timer). Andere sind komplizierter, könnten aber dennoch die Mühe wert sein, für einige Anwendungen Projektionen zu entwickeln (z. B. erwartete Befehle von Betreibern, Wettervorhersagen, projizierte Spuren zum Bewegen von Objekten von Interesse). Es wäre schön, ein Design zu finden, das Bedingungen nicht nur mit Namen, sondern auch mit Funktionen für diese Art von Dingen annotiert.

Hat jemand Erfahrung damit, dass sie bereit sind zu teilen?

Answer 1

Okay, also würde ich sagen, die "echte" Antwort auf Ihre Frage ist, dass einige der Dinge, nach denen Sie fragen, offene Bereiche der Forschung sind - insbesondere denke ich, einige der selbstbeschreibenden Funktionen, die Sie wünschen "Spaghetti" brauchen Sie nur, weil das Problem, das Sie lösen wollen, von Natur aus kompliziert ist.

Das heißt, Ihr Fokus auf Modularität ist genau der richtige Ansatz. Ich würde sagen, werfen Sie einen Blick auf Keymaera, wie ich glaube, dass es die Funktionen hat, die Sie suchen, obwohl Sie in Java sind. Ich würde auch empfehlen, die Veröffentlichungsseite auf der Keymaera-Website zu betrachten, da dies Ihnen wertvolle Einblicke in das Problem im Allgemeinen geben sollte.

Wenn Sie den Ansatz von Keymaera nicht mögen, können Sie auch mit Timed Automata arbeiten, was eine andere Richtung für die Modellierung ist, die für Ihre Problembeschreibung ausreichen sollte.