View in EDS

IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale.

Saved in:
Bibliographic Details
Title: IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale.
Authors: Huerta y Munive, Jonathan Julián1 (AUTHOR) huertjon@cvut.cz, Foster, Simon2 (AUTHOR), Gleirscher, Mario3 (AUTHOR), Struth, Georg4 (AUTHOR), Pardillo Laursen, Christian2 (AUTHOR), Hickman, Thomas2 (AUTHOR)
Source: Journal of Automated Reasoning. Dec2024, Vol. 68 Issue 4, p1-50. 50p.
Abstract: We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 180380786
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Huerta+y+Munive%2C+Jonathan+Julián%22">Huerta y Munive, Jonathan Julián</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> huertjon@cvut.cz</i><br /><searchLink fieldCode="AR" term="%22Foster%2C+Simon%22">Foster, Simon</searchLink><relatesTo>2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Gleirscher%2C+Mario%22">Gleirscher, Mario</searchLink><relatesTo>3</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Struth%2C+Georg%22">Struth, Georg</searchLink><relatesTo>4</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Pardillo Laursen%2C+Christian%22">Pardillo Laursen, Christian</searchLink><relatesTo>2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Hickman%2C+Thomas%22">Hickman, Thomas</searchLink><relatesTo>2</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Dec2024, Vol. 68 Issue 4, p1-50. 50p.
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=180380786
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10817-024-09709-2
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 50
        StartPage: 1
    Titles:
      – TitleFull: IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Huerta y Munive, Jonathan Julián
      – PersonEntity:
          Name:
            NameFull: Foster, Simon
      – PersonEntity:
          Name:
            NameFull: Gleirscher, Mario
      – PersonEntity:
          Name:
            NameFull: Struth, Georg
      – PersonEntity:
          Name:
            NameFull: Pardillo Laursen, Christian
      – PersonEntity:
          Name:
            NameFull: Hickman, Thomas
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 12
              Text: Dec2024
              Type: published
              Y: 2024
          Identifiers:
            – Type: issn-print
              Value: 01687433
          Numbering:
            – Type: volume
              Value: 68
            – Type: issue
              Value: 4
          Titles:
            – TitleFull: Journal of Automated Reasoning
              Type: main
ResultId 1