Edinburgh Research Archive

View Item 
  •   DSpace Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  •   DSpace Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
    • Login
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Direct methods for deductive verification of temporal properties in continuous dynamical systems

    Download
    Sogokon2016.pdf (10.62Mb)
    Date
    2016-06-27
    Author
    Sogokon, Andrew
    Metadata
    Show full item record
    Abstract
    This thesis is concerned with the problem of formal verification of correctness specifications for continuous and hybrid dynamical systems. Our main focus will be on developing and automating general proof principles for temporal properties of systems described by non-linear ordinary differential equations (ODEs) under evolution constraints. The proof methods we consider will work directly with the differential equations and will not rely on the explicit knowledge of solutions, which are in practice rarely available. Our ultimate goal is to increase the scope of formal deductive verification tools for hybrid system designs. We give a comprehensive survey and comparison of available methods for checking set invariance in continuous systems, which provides a foundation for safety verification using inductive invariants. Building on this, we present a technique for constructing discrete abstractions of continuous systems in which spurious transitions between discrete states are entirely eliminated, thereby extending previous work. We develop a method for automatically generating inductive invariants for continuous systems by efficiently extracting reachable sets from their discrete abstractions. To reason about liveness properties in ODEs, we introduce a new proof principle that extends and generalizes methods that have been reported previously and is highly amenable to use as a rule of inference in a deductive verification calculus for hybrid systems. We will conclude with a summary of our contributions and directions for future work.
    URI
    http://hdl.handle.net/1842/20952
    Collections
    • Informatics thesis and dissertation collection

    Privacy & Cookies | Takedown Policy | Accessibility | Contact
    Privacy & Cookies
    Takedown Policy
    Accessibility
    Contact
     

     

    Browse

    All of DSpaceCommunities & CollectionsIssue DateAuthorsTitlesSubjectsPublication TypeSponsorThis CollectionIssue DateAuthorsTitlesSubjectsPublication TypeSponsor

    My Account

    LoginRegister

    Privacy & Cookies | Takedown Policy | Accessibility | Contact
    Privacy & Cookies
    Takedown Policy
    Accessibility
    Contact