Matching Items (2)
Description
Autonomous Vehicles (AV) are inevitable entities in future mobility systems thatdemand safety and adaptability as two critical factors in replacing/assisting human
drivers. Safety arises in defining, standardizing, quantifying, and monitoring requirements
for all autonomous components. Adaptability, on the other hand, involves
efficient handling of uncertainty and inconsistencies in models and data. First, I address
safety by presenting a search-based test-case generation framework that can be
used in training and testing deep-learning components of AV. Next, to address adaptability,
I propose a framework based on multi-valued linear temporal logic syntax and
semantics that allows autonomous agents to perform model-checking on systems with
uncertainties. The search-based test-case generation framework provides safety assurance
guarantees through formalizing and monitoring Responsibility Sensitive Safety
(RSS) rules. I use the RSS rules in signal temporal logic as qualification specifications
for monitoring and screening the quality of generated test-drive scenarios. Furthermore,
to extend the existing temporal-based formal languages’ expressivity, I propose
a new spatio-temporal perception logic that enables formalizing qualification specifications
for perception systems. All-in-one, my test-generation framework can be
used for reasoning about the quality of perception, prediction, and decision-making
components in AV. Finally, my efforts resulted in publicly available software. One
is an offline monitoring algorithm based on the proposed logic to reason about the
quality of perception systems. The other is an optimal planner (model checker) that
accepts mission specifications and model descriptions in the form of multi-valued logic
and multi-valued sets, respectively. My monitoring framework is distributed with the
publicly available S-TaLiRo and Sim-ATAV tools.
ContributorsHekmatnejad, Mohammad (Author) / Fainekos, Georgios (Thesis advisor) / Deshmukh, Jyotirmoy V (Committee member) / Karam, Lina (Committee member) / Pedrielli, Giulia (Committee member) / Shrivastava, Aviral (Committee member) / Yang, Yezhou (Committee member) / Arizona State University (Publisher)
Created2021
Description
Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations. Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials. In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes. Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software. Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties.
ContributorsBanerjee, Ayan (Author) / Gupta, Sandeep K.S. (Thesis advisor) / Poovendran, Radha (Committee member) / Fainekos, Georgios (Committee member) / Maciejewski, Ross (Committee member) / Arizona State University (Publisher)
Created2012