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.
The FS in music was used in a variety of ways throughout the 20th century, primarily focusing on durations and overall structure in its use. Examples of this are found in Béla Bartók’s Music for Strings, Percussion, and Celeste (1936), Allegro barbaro (1911), Karlheinz Stockhausen’s Klavierstück IX (1955), and Luigi Nono’s il canto sospeso (1955). These works are analyzed in detail within my research, and I found every example to have a natural feel to them even if its use of the FS is carefully planned out by the composer. Bartók’s works are the least precise of my examples but perhaps the most natural ones. This imprecision in composition may be considered a more natural use of the FS in music, since nature is not always perfect either. However, in works such as Stockhausen’s, the structure is meticulously formatted in such that the precision is masked by a cycle as to appear more natural.
The conclusion of my research was a commissioned work for my instrument, the viola. I provided my research to composer Jacob Miller Smith, a DMA Music Composition student at ASU, and together we built the framework for the piece he wrote for me. We utilized the life cycle of the Black-Eyed Susan, a flower that uses the FS in its number of petals. The life cycle of a flower is in seven parts, so the piece was written to have seven separate sections in a palindrome within an overall ABA’ format. To utilize the FS, Smith used Fibonacci number durations for rests between notes, note/gesture groupings, and a mapping of 12358 as the set (01247). I worked with Smith during the process to make sure that the piece was technically suitable for my capabilities and the instrument, and I premiered the work in my defense.
The Fibonacci Series and Golden Mean in music provides a natural feel to the music it is present in, even if it is carefully planned out by the composer. More work is still to be done to develop the FS’s use in music, but the examples presented in this project lay down a framework for it to take a natural place in music composition.