SMT-based trace checking of CPS properties

Software is no longer designed only to support humans in complex calculations, but it is more and more used to replace humans in complex activities, where it performs its tasks interacting with a physical environment through hardware systems like sensors and actuators. Automated transportation, domotics, automated medical systems, and the Internet of Things are just examples of the fact that is now almost impossible to find a technical field in which software has not penetrated, greatly increasing the capabilities, but also the complexity, of our machinery. In synthesis, most of our systems are becoming, or have already become, Cyber-Physical, and they are often deployed in situations where safety and reliability are critical. This means that developing techniques that enable rigorous analysis of these types of systems is of paramount importance. However, analyzing Cyber-Physical Systems means being able to describe the complex amalgamation of two very different dynamics: the evolution of physical variables, typically represented as continuous signals, and the behavior of the software components, usually represented by a sequence of state changes and modeled through discrete event systems. Moreover, most of these systems tend to be fairly complex and present a high number of variables and parameters that need to be kept under observation in order to have a useful insight into their behaviour. This ever-increasing amount of data to organize and interpret requires the development of automated verification techniques aimed at complex systems. Trace-checking is a technique of runtime verification that produces a verdict on the conformity of a system to a certain requirement by comparing the execution trace of a system with its ideal behavior, expressed through a suitable specification language. It can be applied to both software systems and hardware systems, as long as a trace can be made available, and more recently it has also been applied to CPS. There are two main categories of languages used for specifying CPS requirements: time-based and sequence-based languages. Time-based languages, which interpret variables as signals over a time domain, are suitable to express CPS requirements related to physical quantities but are not easily amenable to specifying requirements related to software components. On the contrary, in sequence-based languages, traces are defined as sequences of consecutive records of events, which is ideal to describe the dynamics of software components, but not to represent the evolution of physical quantities. Hybrid languages exist to support the specification of both kinds of behaviors, but they are usually ad-hoc extensions of existing languages, focused on specific contexts. Typically, there is a trade-off between the expressiveness of the specification language and the efficiency of the trace-checking procedure; consequently, there is a delicate balance to strike between the expressive power of the specification language and the immediacy of the response, and this is one of the main challenges to face when designing a trace-checking approach for industrial use. In this context, considering the challenges and necessities of CPS development and testing, we present the Hybrid Logic of Signals (HLS), a new specification language tailored to specifying CPS requirements, and ThEodorE (Logic-based TracE checkEr for HLS), an efficient trace-checking approach for properties expressed in HLS. HLS supports the expression of CPS requirements as properties referring both to the time-stamps and the indices of the records of CPS traces, extending existing time and sequence-based languages. The behaviour of both cyber and physical components and their interactions can be captured, using the indices to express discontinuous changes of state, and the timestamps to capture the time relations of the continuous aspects of the system. ThEodorE translates the problem of trace-checking HLS properties to a satisfiability problem, which can be solved using existing Satisfiability Modulo Theories (SMT) solvers, which incorporate efficient decision procedures for several background theories, thus making it possible to check whether a formula expressed in first-order logic is satisfiable. ThEodorE is essentially a Domain Specific Language developed to express logic properties in HSL and assign them to the trace they refer to, augmented with a code generator to translate the data structures created this way into the target SMT logic. We implemented ThEodorE as an Eclipse IDE plugin using Eclipse Xtext, a tool for developing programming languages and DSLs, and Xtend, a Java dialect used in tandem with Xtext. We assessed the expressiveness of HSL and the applicability of ThEodorE through a case study provided by our industrial partner, LuxSpace. LuxSpace developed a satellite to collect tracking information from ships and to transmit those data to the ground, which is an emblematic case of a CPS made of complex software components interacting with many actuators and sensors and the surrounding physical environment, with critical requirements to satisfy regarding all these aspects. We considered 212 of these requirements and we attempted to express them using HSL and two state-of-the-art specification languages: SB-TemPsy-DSL and STL, both supported by publicly available trace checking tools. First, we evaluated the extent to which the requirements were expressible in each language. HSL was able to express 100% of the requirements, while SB-TemPsy-DSL and STL were able to express respectively only 68% and 48% of the requirements. LuxSpace also provided us with 20 traces, obtained by simulating the behavior of the satellite in different scenarios and for simulation times ranging from four to six hours. Their size ranges from 41844 to 1202241 entries. The applicability of ThEodorE was then tested on this dataset against the aforementioned tools, SB-TemPsy-Check and Breach. Applying the 212 requirements to the simulation traces we obtained 747 trace-requirement combinations. ThEodorE could compute a definitive verdict within one hour for 74.5% of the total combinations and in particular for 67.9% of the 337 trace-requirement combinations that could not be checked by the other tools due to language limitations. When the requirements are expressible in SB-TemPsy-DSL and STL, SBTemPsy-Check and Breach are faster than ThEodorE. However, given the usage scenario (offline trace checking), the difference in execution times does not have any practical consequences since the average trace-checking time is significantly lower than the time required to collect the traces. Being able to support a much wider range of properties than other tracecheckers and to verify them within practical time limits, our approach achieves a better trade-off between expressiveness and performances. Furthermore, the efficiency and effectiveness of ThEodorE are expected to improve in the future along with the underlying SMT technology.

Al giorno d’oggi, componenti informatiche sono sempre più utilizzate per sostituire l’uomo in attività complesse, dove è necessario che interagiscano con l’ambiente fisico in cui sono collocati. Forme di trasporto automatizzato, applicazioni di domotica, sistemi medicali di nuova generazione e la nascita del cosiddetto “Internet of Things” sono solo esempi del fatto che è ormai quasi impossibile trovare un dominio della tecnica in cui l’informatica non sia penetrata, aumentando notevolmente le capacità, ma di pari passo anche la complessità, dei macchinari che ci circondano. In sintesi, la maggior parte dei nostri sistemi stanno diventando, o sono già diventati, ciber-fisici, e sono spesso impiegati in situazioni in cui la sicurezza e l’affidabilità sono aspetti critici. Ne consegue che lo sviluppo di tecniche che consentano un’analisi rigorosa di questo tipo di sistemi è diventato di fondamentale importanza. Tuttavia, analizzare i Sistemi Ciber-Fisici significa essere in grado di descrivere quello che spesso risulta essere un amalgama complesso di due dinamiche molto diverse tra loro: l’evoluzione delle variabili fisiche, tipicamente rappresentate come segnali continui, e il comportamento delle componenti software, solitamente rappresentato da una sequenza di cambiamenti di stato e modellato attraverso sistemi ad eventi discreti. Inoltre, la maggior parte di questi sistemi tendono ad essere notevolmente complessi e presentano un numero elevato di variabili e parametri da tenere sotto osservazione per ottenere una descrizione sufficientemente esaustiva del loro comportamento. Questa quantità sempre crescente di dati da organizzare e interpretare ha portato allo sviluppo di tecniche di verifica automatizzate ad essi dedicate. Il Trace-checking è una di queste tecniche. Essa mira a produrre un verdetto riguardante la conformità di un sistema ad un certo requisito, confrontando la traccia di esecuzione di un sistema, ovvero la misurazione di un insieme di variabili che ne descrivono lo stato durante le sue operazioni, con il suo comportamento ideale, espresso attraverso formule logiche scritte in un adeguato linguaggio di specificazione. Può essere applicata sia a sistemi software che a sistemi hardware, purché sia possibile registrare una traccia, e più recentemente si è iniziato ad usarla anche per i sistemi ciber-fisici. Ci sono due categorie principali di linguaggi usati per specificare i requisiti logici: i linguaggi time-based, ovvero basati sul tempo e quelli basati sul concetto di sequnza di eventi (sequence-based). I linguaggi basati sul tempo, che interpretano le variabili come segnali in un dominio temporale, sono adatti ad esprimere i requisiti relativi alle grandezze fisiche, ma non sono facilmente adattabili a specificare i requisiti relativi ai componenti software. Al contrario, nei linguaggi sequence-based, le tracce sono definite tramite sequenze ordinate di eventi consecutivi (come quelle prodotte dagli automi a stati finiti) che risultano adeguate per descrivere la dinamica delle componenti informatiche, ma non ottimali per rappresentare l’evoluzione di grandezze del mondo fisico. Ad oggi sono stati sviluppati anche linguaggi ibridi che tentano di supportare la specificazione di entrambi i tipi di comportamento, ma sono solitamente estensioni ad hoc di linguaggi esistenti, focalizzati su contesti specifici e che spesso ereditano alcune delle limitazioni del linguaggio di partenza. Oltretutto, esiste generalmente un rapporto di proporzionalità inversa tra l’espressività del linguaggio di specifica e l’efficienza della procedura di tracechecking; di conseguenza, occorre trovare un compromesso tra la potenza espressiva del linguaggio e l’immediatezza della risposta, affinché sia possibile avvalersi della tecnica sviluppata nella pratica. Questa è una delle principali sfide da affrontare quando si progetta un approccio di trace-checking per uso industriale. In questo contesto, considerando le sfide e le necessità dello sviluppo e del testing dei sistemi ciber-fisici, presentiamo Hybrid Logic of Signals, in breve HLS, un nuovo linguaggio di specifica pensato per questa classe di sistemi, e ThEodorE (Logic-based TracE checkEr for HLS), un algoritmo di tracechecking automatico svluppato per le proprietà espresse in HLS. HLS supporta l’espressione di requisiti riferiti sia ai timestamps, ovvero ai tempi di acquisizione dei record della traccia, che agli indici numerici dei record. Diventa quindi possibile catturare il comportamento delle componenti sia informatiche che fisiche e le loro interazioni, utilizzando gli indici per esprimere i cambiamenti discontinui di stato e i timestamp per catturare le relazioni temporali degli aspetti continui del sistema. ThEodorE riduce il problema del controllo delle proprietà HLS in un problema di Satisfiability Modulo Theories, che puo essere risolto da numerosi solver già esistenti, i quali incorporano procedure decisionali efficienti per diverse teorie logiche, rendendo così possibile verificare se la fomula che rappresenta l’unione della proprietà espressa e del comportamento della traccia è soddisfatta o meno. ThEodorE è essenzialmente un Domain Specific Language (Linguaggio di Dominio Specifico) sviluppato per esprimere le proprietà logiche in HSL e assegnarle alla traccia a cui si riferiscono, dotato di un generatore di codice per tradurre le strutture dati create in questo modo nella logica SMT di destinazione. Abbiamo implementato ThEodorE usando Eclipse Xtext, uno strumento per sviluppare linguaggi di programmazione, e Xtend, un dialetto di Java pensato per essere usato assieme a Xtext, e lo abbiamo finalizzato nella forma di un plugin per Eclipse IDE. Abbiamo valutato l’espressività di HSL e l’applicabilità di ThEodorE attraverso un caso di studio fornitoci dal nostro partner industriale, LuxSpace. LuxSpace è un azienda del settore aerospaziale che ha sviluppato un satellite per raccogliere informazioni di tracciamento dalle navi e per trasmettere questi dati a terra. Rappresenta un caso emblematico di sistema ciber-fisco composto da componenti software complessi che interagiscono con un gran numero di attuatori e sensori e con l’ambiente fisico circostante. Visto il contesto di impiego, il settore industriale e l’utilizzo previsto per il satellite, esso è oggetto di molti requisiti tecnici e di funzionamento che deve soddisfare. Abbiamo preso in considerazione 212 di questi requisiti e abbiamo cercato di esprimerli utilizzando HSL e due linguaggi di specifica all’avanguardia, ovvero SB-TemPsy-DSL e STL, entrambi supportati, come HSL, da strumenti di trace-checking. In primo luogo, abbiamo valutato la misura in cui i requisiti erano esprimibili da ogni linguagggio. HSL è stato in grado di esprimere il 100% dei requisiti, mentre SB-TemPsy-DSL e STL sono stati in grado di esprimerne rispettivamente solo il 68% e il 48%. LuxSpace ci ha anche fornito 20 tracce, ottenute simulando il comportamento del satellite in diversi scenari e per tempi di simulazione che vanno dalle quattro alle sei ore. La loro dimensione varia da 41844 a 1202241 voci. L’applicabilità di ThEodorE è stata quindi testata su questo dataset contro SB-TemPsy-Check e Breach, i due algoritmi di trace-checking relativi ai suddetti linguaggi. Applicando i 212 requisiti alle tracce di simulazione abbiamo ottenuto 747 combinazioni di tracce e requisiti. ThEodorE è riuscito a calcolare un verdetto definitivo entro un’ora per il 74,5% del totale delle combinazioni. In particolare, è riuscito a valutare il 67,9% delle 337 combinazioni che i linguaggi concorrenti non hanno potuto esprimere. Quando i requisiti sono esprimibili in SB-TemPsy-DSL e STL, SB-TemPsyCheck e Breach sono più veloci di ThEodorE. Tuttavia, dato lo scenario di utilizzo (controllo delle tracce offline), la differenza nei tempi di esecuzione non ha alcuna conseguenza pratica, poiché il tempo medio di controllo delle tracce, nell’ordine dei minuti, è in ogni caso significativamente inferiore alle ore necessarie per raccogliere le tracce. Essendo in grado di esprimere un insieme di proprpietà molto più ampio rispetto ad altri sistemi e di verificare le suddette tracce entro limiti di tempo pratici, ThEodorE rappresenta un migliore compromesso tra espressività e performance. Inoltre, si prevede che l’efficienza e l’efficacia di ThEodorE miglioreranno in futuro insieme alla tecnologia SMT sottostante, in quanto i solver in questione sono tuttora oggetto di ricerca e sviluppo continuo.