CaltechAUTHORS
  A Caltech Library Service

Osiris: A Tool for Abstraction and Verification of Control Software with Lookup Tables

Aréchiga, Nikos and Dathathri, Sumanth and Vernekar, Shashank and Kathare, Nagesh and Gao, Sicun and Shiraishi, Shinichi (2017) Osiris: A Tool for Abstraction and Verification of Control Software with Lookup Tables. In: Proceedings of the 1st International Workshop on Safe Control of Connected and Autonomous Vehicles. Association for Computing Machinery , New York, NY, pp. 11-18. ISBN 978-1-4503-4976-5. http://resolver.caltech.edu/CaltechAUTHORS:20170313-163356916

[img] PDF - Accepted Version
See Usage Policy.

768Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20170313-163356916

Abstract

Some industrial systems are difficult to formally verify due to their large scale. In particular, the widespread use of lookup tables in embedded systems across diverse industries, such as aeronautics and automotive systems, create a critical obstacle to the scalability of formal verification. This paper presents Osiris, a tool that automatically computes abstractions of lookup tables. Osiris uses these abstractions to verify a property in first order logic. If the verification fails, Osiris uses a falsification heuristic to search for a violation of the specification. We validate our technique on a public benchmark of an adaptive cruise controller with lookup tables.


Item Type:Book Section
Related URLs:
URLURL TypeDescription
http://dx.doi.org/10.1145/3055378.3055384DOIArticle
http://dl.acm.org/citation.cfm?doid=3055378.3055384PublisherArticle
Additional Information:© 2017 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Subject Keywords:Abstraction, Lookup Tables, Verification, Formal Methods
Record Number:CaltechAUTHORS:20170313-163356916
Persistent URL:http://resolver.caltech.edu/CaltechAUTHORS:20170313-163356916
Official Citation:Nikos Arechiga, Sumanth Dathathri, Shashank Vernekar, Nagesh Kathare, Sicun Gao, and Shinichi Shiraishi. 2017. Osiris: A Tool for Abstraction and Verification of Control Software with Lookup Tables. In Proceedings of Safe Control of Connected and Autonomous Vehicles, Pittsburgh, Pennsylvania, USA, April 2017 (SCAV’17), 8 pages. DOI: http://dx.doi.org/10.1145/3055378.3055384
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:75079
Collection:CaltechAUTHORS
Deposited By: Sumanth Dathathri
Deposited On:05 Apr 2017 21:16
Last Modified:06 Jun 2017 17:35

Repository Staff Only: item control page