Software level adaptation in cyber physical systems

Cyberphysical systems (CPSs) are a category of engineered systems that combines physical processes with computational control. The key property of these systems is that their functionality is emerging from the intense interactions between computational devices and the real world. Consider a typical CPS application: a Wireless Sensor Network (WSN) for the environmental monitoring. The environment exhibits multiple dimensions that are changing continuously and independently. As the WSN monitors these changes, its functionality heavily depends on the environmental dynamics, which leads to the need for the WSN software to be adaptive. Another large class of CPSs are Unmanned Aerial Vehicles (UAVs). These are representative of time-critical CPSs. The typical UAV control board also consists of a number of sensors that are used to calculate the modulation of the motors and to keep the flight stable. Similarly to WSNs, UAVs monitor the environment through sensors to control the flight. Crucially, UAVs rely on the sensor input, and generate the control decisions in real-time. In this thesis we focus on the adaptive software for such systems. Our goal is to provide language independent concepts that can help developers to design, verify and implement the adaptive software for time-critical systems. Unlike most existing work, we do not present the mechanisms or algorithms for adaptation. Our aim is to make the ways these mechanisms and/or algorithms are designed, programmed, and verified more effective. In the first part of this thesis we introduce our language-independent design concepts to organize the WSN operating modes, decoupling the abstractions from their concrete implementation in a programming language. Our language CONESC natively supports the dedicated adaptation mechanisms and allows developers to implement adaptive WSN software. To verify this software we provided a dedicated verification algorithm. The latter is integrated with our tool GREVECOM that delivers the seamless way to build the model of the software, to exhaustively verify it against the environmental evolutions, and to build the CONESC templates. Finally, CONESC sources are compiled with the dedicated translator yielding the binary that is ready to be deployed. The evaluation have shown that our concepts increase the ease of the developing and verifying of the adaptive WSNs software with a very little price, such as less than 2.5% memory overhead and less that 200ms verification time. In the second part of the thesis we focus on the time aspect in enforcing adaptation decisions. Our concepts deliver different activation types for the CPS operation modes, trading off latency at run-time vs. programming efforts. Each activation type has also time boundaries that can be optionally enabled by the programmer. We show the usefulness of our concepts in a prototype built for the Cortex-M3 microcontroller. Our early evaluation has revealed that with the cost of a small MCU performance overhead, we provide an additional functionality and guaratees that do not exists in current approaches.

I sistemi cyberfisici (Cyberphysical Systems) sono una categoria di sistemi ingegnerizzati che combina processi fisici con il controllo digitale. La proprietà fondamentale di questi sistemi è che la loro funzionalità emerge dalle interazioni tra i dispositivi di calcolo e il mondo reale. Si consideri una tipica applicazione CPS: una rete di sensori wireless per il monitoraggio ambientale. L'ambiente presenta molteplici dimensioni che mutano continuamente e in modo indipendente. L’operatività della rete di sensori dipende fortemente da queste dinamiche ambientali; ciò porta alla necessità di realizzare software adattativo. Una diversa classe di sistemi cyberfisici sono gli aeromobili a pilotaggio remoto (APR), che rappresentano funzionalità time-critical. La scheda di controllo del dispositivo consiste in una serie di sensori utilizzati per determinare il funzionamento dei motori e per mantenere la stabilità di volo. Analogamente alle reti di sensori wireless, gli APR monitorano l'ambiente attraverso sensori per il controllo del volo. Nel determinare il funzionamento dei motori, le decisioni di controllo devono essere generate in tempo reale. Questa tesi si concentra sullo sviluppo di software adattativo per questi sistemi. Il nostro obiettivo è di fornire concetti e costrutti di programmazione che possono aiutare gli sviluppatori nel progettare, verificare, e implementare tale software adattativo. Diversamente dalla stato dell’arte, non presentiamo meccanismi o algoritmi per l'adattamento. Il nostro obiettivo è di rendere più efficace il design, implementazione, e verifica di tali meccanismi o algoritmi. Nella prima parte di questa tesi presentiamo concetti di design indipendenti dal linguaggio di programmazione per esprimere le diverse modalità operative di una rete di sensori wireless, disaccoppiando le astrazioni dalla loro concreta realizzazione in un linguaggio di programmazione. Per questo, progettiamo un linguaggio dedicato, chiamato ConesC, che supporta in modo nativo i concetti di design. Per le attività di verifica del software, presentiamo un algoritmo dedicato e lo integriamo in GREVECOM: un tool che supporta la costruzione del modello del software, la verifica in modo esaustivo della correttezza rispetto alle evoluzioni ambientali, e la generazione di template ConesC. Infine, il codice ConesC è compilato con un traduttore dedicato per ottenere il codice binario pronto per essere distribuito. La nostra valutazione indica che la nostra soluzione migliora la facilità di sviluppo e la verifica del software adattivo con costi limitati, ad esempio, meno del 2,5% di crescita nell’occupazione di memoria e meno di 200ms per la verifica nelle applicazioni che abbiamo considerato. Nella seconda parte della tesi ci concentriamo sull'aspetto temporale nelle decisioni di adattamento. Definiamo concetti per offrire diversi tipi di attivazione delle differenti modalità di funzionamento, e per controllare i tempi di esecuzione delle decisioni di adattamento. Mostriamo l'utilità dei nostri concetti in un prototipo costruito per il microcontrollore Cortex-M3. La nostra valutazione iniziale rivela che il costo del nostro approccio è limitato in termini di sovraccarico del microcontrollore, ma forniamo una funzionalità e garanzie aggiuntive non fornite da soluzioni esistenti.