Verification of Hybrid Systems using Satisfiability Modulo Theories

Mover, Sergio (2014) Verification of Hybrid Systems using Satisfiability Modulo Theories. PhD thesis, University of Trento, Fondazione Bruno Kessler.

[img]PDF - Doctoral Thesis
Restricted to Repository staff only until 9999.



Embedded systems are formed by hardware and software components that interact with the physical environment and thus may be modeled as Hybrid Systems. Due to the complexity the system,there is an increasing need of automatic techniques to support the design phase, ensuring that a system behaves as expected in all the possible operating conditions.In this thesis, we propose novel techniques for the verification and the validation of hybrid systems using Satisfiability Modulo Theories (SMT). SMT is an established technique that has been used successfully in many verification approaches, targeted for both hardware and software systems. The use of SMT to verify hybrid systems has been limited, due to the restricted support of complex continuous dynamics and the lack of scalability. The contribution of the thesis is twofold. First, we propose novel encoding techniques, which widen the applicability and improve the effectiveness of the SMT-based approaches. Second, we propose novel SMT-based algorithms that improve the performance of the existing state of the art approaches. In particular we show algorithms to solve problems such as invariant verification, scenario verification and parameter synthesis. The algorithms fully exploit the underlying structure of a network of hybrid systems and the functionalities of modern SMT-solvers. We show and discuss the effectiveness of the the proposed techniques when applied to benchmarks from the hybrid systems domain.

Item Type:Doctoral Thesis (PhD)
Doctoral School:Information and Communication Technology
PhD Cycle:25
Subjects:Area 01 - Scienze matematiche e informatiche > INF/01 INFORMATICA
Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Area 01 - Scienze matematiche e informatiche > MAT/01 LOGICA MATEMATICA
Uncontrolled Keywords:Formal Verification, Hybrid Systems, Cyber-Physical Systems, Hybrid Automata, Model Checking, Satisfiability Modulo Theory, Scenario Verification, Parameter Synthesis
Repository Staff approval on:26 Mar 2014 14:52

Repository Staff Only: item control page