Mohammad Hekmatnejad

Mohammad Hekmatnejad, Bardh Hoxha, Jyotirmoy V. Deshmukh et al.

Automated vehicles (AV) heavily depend on robust perception systems. Current methods for evaluating vision systems focus mainly on frame-by-frame performance. Such evaluation methods appear to be inadequate in assessing the performance of a perception subsystem when used within an AV. In this paper, we present a logic -- referred to as Spatio-Temporal Perception Logic (STPL) -- which utilizes both spatial and temporal modalities. STPL enables reasoning over perception data using spatial and temporal operators. One major advantage of STPL is that it facilitates basic sanity checks on the functional performance of the perception system, even without ground-truth data in some cases. We identify a fragment of STPL which is efficiently monitorable offline in polynomial time. Finally, we present a range of specifications for AV perception systems to highlight the types of requirements that can be expressed and analyzed through offline monitoring with STPL.

Mohammad Hekmatnejad, Bardh Hoxha, Georgios Fainekos

The safety of Automated Vehicles (AV) as Cyber-Physical Systems (CPS) depends on the safety of their consisting modules (software and hardware) and their rigorous integration. Deep Learning is one of the dominant techniques used for perception, prediction, and decision making in AVs. The accuracy of predictions and decision-making is highly dependant on the tests used for training their underlying deep-learning. In this work, we propose a method for screening and classifying simulation-based driving test data to be used for training and testing controllers. Our method is based on monitoring and falsification techniques, which lead to a systematic automated procedure for generating and selecting qualified test data. We used Responsibility Sensitive Safety (RSS) rules as our qualifier specifications to filter out the random tests that do not satisfy the RSS assumptions. Therefore, the remaining tests cover driving scenarios that the controlled vehicle does not respond safely to its environment. Our framework is distributed with the publicly available S-TALIRO and Sim-ATAV tools.

Mohammad Hekmatnejad, Andrew M. Simms, Georgios Fainekos

Individual clinical Knowledge Artifacts (KA) are designed to be used in Clinical Decision Support (CDS) systems at the point of care for delivery of safe, evidence-based care in modern healthcare systems. For formal authoring of a KA, syntax verification and validation is guaranteed by the grammar. However, there are no methods for semantic verification. Any semantic fallacy may lead to rejection of the outcomes by care providers. As a first step toward solving this problem, we present a framework for translating the logical segments of KAs into Satisfiability Modulo Theory (SMT) models. We present the effectiveness and efficiency of our work by automatically translating the logic fragment of publicly available KAs and verifying them using Z3 SMT solver.