| For high-assurance cyber-physical systems (CPS), such as the onboard features in modern transportation systems (e.g., automobiles, trains, and flight systems), ensuring acceptable and safe behavior is of paramount importance. Furthermore, the increasing complexity and the number of onboard features for autonomous vehicles further exacerbates the challenge of guaranteeing safe behavior. The operation of these high-assurance cyber-physical systems depends on the specification, implementation, and verification of those systems. Obstacles to assessing and ensuring assurance for cyber-physical system requirements may occur in many forms, but two significant sources of specification errors are incomplete requirements specifications and undesired feature interactions. In the case of incomplete requirements, it can be challenging to enumerate all the decomposed requirements necessary to satisfy a requirement (i.e., ensuring completeness), especially when considering different combinations of environmental conditions. A feature interaction occurs when two or more features satisfy specific properties in isolation, but no longer satisfy those properties when they are composed together. It may be necessary to analyze an exponential number of feature combinations to detect all possible interactions, resulting in a potentially exponential number of feature interaction results presented to the system developer. Furthermore, the uncertainty created by unexpected system and environmental scenarios exacerbates already difficult requirements specifications problems, many of which involve an exhaustive search for errors and their causes. That is, the exponential number of possibilities represents not only computational growth but also growth in the effort it takes the system designer to assess the results. This doctoral research tackles two key requirements assurance problems that exhibit these characteristics: requirements incompleteness and undesired feature interactions. The work explores how formal analysis and search-based techniques can be used in a complementary and synergistic fashion to address the assurance of cyber-physical systems facing environmental and system uncertainty, both at design time and run time. Industrial applications are used to demonstrate the respective techniques. |
