System and software verification is a vital component in the development and reliability of cyber-physical systems - especially in critical domains where the margin of error is minimal. In the case of autonomous driving systems (ADS), the vision perception subsystem is a necessity to ensure correct maneuvering of the environment and identification of objects. The challenge posed in perception systems involves verifying the accuracy and rigidity of detections. The use of Spatio-Temporal Perception Logic (STPL) enables the user to express requirements for the perception system to verify, validate, and ensure its behavior; however, a drawback to STPL involves its accessibility. It is limited to individuals with an expert or higher-level knowledge of temporal and spatial logics, and the formal-written requirements become quite verbose with more restrictions imposed. In this thesis, I propose a domain-specific language (DSL) catered to Spatio-Temporal Perception Logic to enable non-expert users the ability to capture requirements for perception subsystems while reducing the necessity to have an experienced background in said logic. The domain-specific language for the Spatio-Temporal Perception Logic is built upon the formal language with two abstractions. The main abstraction captures simple programming statements that are translated to a lower-level STPL expression accepted by the testing monitor. The STPL DSL provides a seamless interface to writing formal expressions while maintaining the power and expressiveness of STPL. These translated equivalent expressions are capable of directing a standard for perception systems to ensure the safety and reduce the risks involved in ill-formed detections.
Motor learning is the process of improving task execution according to some measure of performance. This can be divided into skill learning, a model-free process, and adaptation, a model-based process. Prior studies have indicated that adaptation results from two complementary learning systems with parallel organization. This report attempted to answer the question of whether a similar interaction leads to savings, a model-free process that is described as faster relearning when experiencing something familiar. This was tested in a two-week reaching task conducted on a robotic arm capable of perturbing movements. The task was designed so that the two sessions differed in their history of errors. By measuring the change in the learning rate, the savings was determined at various points. The results showed that the history of errors successfully modulated savings. Thus, this supports the notion that the two complementary systems interact to develop savings. Additionally, this report was part of a larger study that will explore the organizational structure of the complementary systems as well as the neural basis of this motor learning.