Formal specification and analysis of hybrid systems
KL Ka Lok Man, Rrh Ramon Schiffelers · TU/e Research Portal · 2006
reviewing the manuscript of this thesis and giving us valuable comments.Thirdly, we thank our colleagues of the Systems Engineering Group, the Formal Methods Group, the Design and Analysis of Systems Group and the (Eindhoven) Embedded System Institute for contributing to a pleasant working atmosphere.Finally, we thank our families and friends for their support.All research presented in this thesis is joint work.In particular, we would like to remark that the syntax and semantics of χ, and the formal translation of a subset of χ to hybrid automata and vice versa have been developed by both authors.In addition, K.L. Man has provided proofs for the semantics of χ, the correctness of the translations and tool support, and he developed the elimination theorems for a number of χ operators.The tools and examples have been developed by R.R.H. Schiffelers. v vi SummaryIn this research, the hybrid χ (Chi) formalism has been developed.The hybrid χ formalism is suited to modeling, simulation and verification of hybrid systems.The semantics of hybrid χ is defined by means of deduction rules (in SOS style) that associate a hybrid transition system with a χ process.A set of axioms is presented for a notion of equivalence (bisimilation).The hybrid χ formalism integrates concepts from dynamics and control theory with concepts from computer science, in particular from process algebra and hybrid automata.It integrates ease of modeling with a straightforward semantics.Its 'consistent equation semantics' enforces state changes to be consistent with delay predicates, that combine the invariant and flow clauses of hybrid automata.Ease of modeling is ensured by means of the following concepts: 1) different classes of variables: discrete and continuous, of subclass jumping or non-jumping, and algebraic; 2) strong time determinism of alternative composition in combination with delayable guards; 3) integration of urgent and non-urgent actions; 4) differential algebraic equations as a process term as in mathematics; 5) steadystate initialization; and 6) several user-friendly syntactic extensions.Furthermore, the hybrid χ formalism incorporates several concepts for complex system specification: 1) process terms for scoping that integrate abstraction, local variables, local channels and local recursion definitions; 2) process definition and instantiation that enable process reuse, encapsulation, hierarchical and/or modular composition of processes; and 3) different interaction mechanisms: handshake synchronization and synchronous communication that allow interaction between processes without sharing variables, and shared variables that enable modular composition of continuous-time or hybrid processes.In process algebra, linearization is a transformation of a recursive specification into a linear representation, i.e., a kind of normal form that is convenient for many forms of analysis.A first step towards the linearization of a reasonable subset of the hybrid χ language has been carried out in the form of elimination theorems for a number of χ operators. SamenvattingIn dit onderzoek is het hybride χ (Chi) formalisme ontworpen.Dit formalisme is geschikt voor het modelleren, simuleren en verifiëren van hybride systemen.De semantiek van hybride χ is definiëerd met behulp van deductieregels (in SOS stijl) die een hybride transitiesysteem associëren met een χ process.Een set van axioma's is gedefinieerd voor een notie van gelijkheid (bisimulatie).Het hybride χ formalisme integreert concepten uit de dynamica en regeltheorie met concepten uit de informatica, in het bijzonder concepten uit de proces algebra en de theorie van hybride automaten.Het formalisme integreert de eenvoud van modelleren met een duidelijke semantiek.De 'consistente vergelijking semantiek' zorgt ervoor dat toestandsveranderingen consistent zijn met delay predicaten, die de invariant en flow clauses van hybride automaten omvatten.De eenvoud van modelleren is gegarandeerd door de volgende concepten: 1) verschillende klassen van variabelen: discreet en continu, met sub-klassen jumping en niet-jumping, en algebraisch; 2) sterk tijddeterminisme van de alternative compositie operator in combinatie met delayable guards; 3) integratie van urgente en niet-urgente acties; 4) algebraische differentiaalvergelijkingen als procestermen zoals in de wiskunde; 5) steady-state initializatie; en 6) verschillende gebruiksvriendelijke syntactische extensies.Verder omvat het hybride χ formalisme verschillende concepten voor de specificatie van complexe systemen: 1) procestermen voor scoping die abstractie, lokale variabelen, lokale kanalen en lokale recursiedefinities integreren; 2) procesdefinitie en procesinstantiatie die het hergebruiken van processen, encapsulatie, hierarchische en/of modulaire compositie van processen mogelijk maken; en 3) verschillende interactiemechanismen: handshake synchronizatie en handshake communicatie die interactie tussen processen zonder shared variabelen mogelijk maken, en shared variabelen die modulaire compositie van continue-tijd of hybride processen mogelijk maken.In de proces algebra is linearizatie een tranformatie van een recursieve specificatie naar een lineaire representatie, ofwel een soort van normaalvorm die handig is voor veel vormen van analyse.Een eerste stap in de richting van linearizatie van een redelijke subset van het hybride χ formalisme is genomen in de vorm van eliminatietheorema's voor een aantal χ operators.Verder is een formele translatie van een subset van χ naar hybride automaten en visa versa gedefinieerd.Het is bewezen dat iedere transitie van een χ model nagebootst kan ix worden door een transitie van het corresponderende hybride automaten model en visa versa.Dit geeft aan dat de gedefinieerde translatie correct is.De translatie van χ naar hybride automaten maakt verificatie van χ modellen gebruik makend van bestaande verificatiegereedschappen voor hybride automaten mogelijk.Voor simulatie en verificatie van χ modellen zijn gereedschappen ontwikkeld.Het 'stepper gereedschap' genereert gegeneralizeerde transities gegeven een χ proces.Gebaseerd op het stepper gereedschap is een symbolische simulator ontwikkeld.Verder is de translatie van χ naar hybride automaten geautomatiseerd.Het χ formalisme is geillustreerd met behulp van voorbeelden uit verschillende toepassingsgebieden.Case studies zijn uitgevoerd om de ontwikkelde gereedschappen te testen. SommarioIn questa ricerca è stato sviluppato il formalismo dell'hybrid χ (Chi).Tale formalismo adatto per modellare, simulare e verificare i sistemi ibridi.Le semantiche dell'hybrid χ sono definite per mezzo di regole deduttive (in stile SOS) che associano un sistema a transizione ibrida con un processo Chi.È stato presentato un insieme di assiomi, per un concetto di bisimilarità.Il formalismo hybrid χ integra concetti della dinamica e della teoria dei controlli con concetti informatici, in particolare dell'algebra dei processi e degli automi ibridi.Presenta facilità di modellizzazione insieme ad una semantica lineare.Le sue semantiche di equazioni consistenti obbligano i cambi di stato ad essere consistenti con i predicati di ritardo, che combinano gli invarianti e le proposizioni di flusso invarianti degli automi ibridi.La facilità di modellizzazione è garantita dai seguenti concetti: 1) differenti classi di variabili: discrete e continue, di jumping e non-jumping di sottoclassi, e algebriche; 2) forte determinismo temporale della composizione alternativa in combinazioni con guards ritardabili; 3) integrazione di azioni urgenti e non urgenti; 4) equazioni algebriche differenziali come un termine di processo, come in matematica; 5) inizializzazione steady-state; e 6) numerose espressioni sintattiche user-friendly.Inoltre, il formalismo dell'hybrid χ incorpora diversi concetti per la specifica di sistemi complessi: 1) termini di processo per scoping che integrano l'astrazione, le variabili locali, canali locali e definizioni di ricorsione locale; 2) definizione ed istanziazione dei processi che permette il riutilizzo dei processi, l'incapsulamento, la composizione gerarchica e/o modulare dei processi; e 3) differenti meccanismi di interazione: sincronizzazione handshake e comunicazione sincrona, che permettono l'interazione tra processi senza condivisione di variabili, e variabili condivise che permettono la composizione modulare dei processi continui nel tempo o ibridi.Nell'algebra dei processi, la linearizzazione è una trasformazione di una specifica ricorsiva in una rappresentazione lineare, cioè un tipo di forma normale che è vantaggiosa per molte analisi.Un primo passo verso la linearizzazione di un ragionevole sottoinsieme del linguaggio χ è stato messo in pratica nella forma dei teoremi di eliminazione, per alcuni operatori di χ.Inoltre, è stata definita la traduzione formale di un sottoinsieme di χ agli automi ibridi e vice versa.È stato provato che ogni transizione di un modello χ può essere "mimicked" da una transizione nel corrispondente automa ibrido e vice versa, il che indica la correttezza xi della traduzione per come è stata definita.La traduzione del χ agli automi ibridi permette la verifica dei modelli χ usando gli strumenti di verifica esistenti basati sugli automi ibridi.Sono stati sviluppati degli strumenti informatici per la simulazione e verifica dei modelli χ.Lo strumento Stepper genera transizioni generalizzate.Basato Stepper, sono stati sviluppati due simulatori: un simulatore simbolico e un simulatore numerico basato sull'interfaccia Simulink delle funzioni S. Infine, è stata automatizzata la transizione da χ agli automi ibridi.Il formalismo χ è illustrato attraverso esempi tratti da parecchi campi di applicazione.Gli strumenti sviluppati sono stati validati per mezzo di alcuni casi di studio.