Approcci funzionali alla progettazione del lato discreto dei sistemi ibridi

Question

Sto lavorando allo sviluppo di controller per sistemi ibridi in Haskell.

Le librerie FRP (in questo momento sto usando netwire, ma ce ne sono molte buone e molte ricerche interessanti su quelle future) forniscono un'ottima soluzione per il problema del tempo continuo. Aumentandoli con nomi di segnali, dimensioni, unità preferite e così via, si ottiene un sistema che ha modularità, è auto-descrittivo e ha un percorso diretto verso la fiducia nella correttezza.

Sto cercando informazioni, folclore o documenti che offrono proprietà simili per il lato discreto. In un certo senso il problema è molto più facile, le macchine di stato sono ben studiate e semplici. In altri sensi è più difficile, spiegherò brevemente come.

La correttezza è ovviamente la cosa più importante, e per fortuna è anche semplice.

L'auto-descrizione è più di un problema. Vorresti che il controller non fosse solo nello stato corretto, ma che fosse in grado di dirti in che stato si trova. Inoltre, come è arrivato. E dove potrebbe andare dopo. In questo modo è possibile associare i nomi a tutto e funziona, ma è in qualche modo in conflitto con la modularità. Ti piacerebbe anche essere in grado di costruire complessi comportamenti a tempo discreto da quelli più semplici. Ma quando chiedi al sistema in che stato è, generalmente la risposta di alto livello è più interessante (o almeno interessante) della risposta di basso livello. Come lo si ottiene in modo pulito? Ho provato alcuni approcci ingenui e mi sono avvolto in spaghetti in modi diversi, ma sembra che ci debbano essere soluzioni eleganti?

Un altro problema che ho avuto con l'auto-descrizione è che mi piacerebbe avere un elenco di condizioni auto-descrittive (in genere confronti: sono passati 10 secondi? Sono a meno di 3 piedi dal prossimo waypoint? la carica della batteria è scesa al di sotto del 15%? ecc.) che vengono monitorati e che potrebbero innescare la successiva transizione di stato. Ci sono domande complicate su ciò che anche qui sono le semantiche desiderabili, dal momento che sembra che alcuni di questi eventi siano gestiti meglio "dal basso verso l'alto" (ad esempio condizioni di terminazione attese di qualunque livello di basso livello che si sta eseguendo) e alcuni "dall'alto" giù "(ad es. rilevamento guasti dell'attrezzatura, geofencing, ...). Questo può portare a spaghetti propri, anche se si rilassa l'obiettivo di auto-descrizione.

Oltre alla diagnostica, le informazioni accurate di auto-descrizione qui potrebbero anche essere molto utili per l'interpretazione astratta, proiettando lo stato del sistema nel futuro indovinando quali eventi possono verificarsi quando. Molte delle condizioni dell'evento portano a supposizioni abbastanza semplici (ad esempio usando velocità fatte bene, tasso di consumo di carburante, timer). Altri sono più complicati, ma potrebbero comunque valere lo sforzo di sviluppare proiezioni per alcune applicazioni (ad esempio ordini previsti dagli operatori, previsioni meteorologiche, tracce proiettate per spostare oggetti di interesse). Sarebbe bello trovare un design che annoti le condizioni non solo con i nomi, ma anche con funzioni per questo tipo di cose.

Qualcuno ha esperienza con questo che è disposto a condividere?

Answer 1

Ok, quindi direi che la "vera" risposta alla tua domanda è che alcune delle cose che stai chiedendo sono aree aperte di ricerca --- in particolare penso che alcune delle caratteristiche che si auto-descrivono che desideri possano richiede un certo grado di "spaghetti" semplicemente perché il problema che stai cercando di risolvere è intrinsecamente complicato.

Detto questo, l'attenzione per la modularità è esattamente l'approccio giusto. Direi, date un'occhiata a Keymaera perché credo che abbia le caratteristiche che state cercando nonostante siano in Java. Raccomando anche di consultare la pagina delle pubblicazioni sul sito Web Keymaera in quanto ciò dovrebbe fornire preziose informazioni sul problema in generale.

Se non ti piace l'approccio di Keymaera, puoi anche utilizzare Timed Automata, che è un altro modello di direzione che dovrebbe essere sufficiente per la descrizione del tuo problema.