Specification mining frameworks for complex software systems

Software specifications define system behavior, usage guidelines, requirements and act as a tool for debugging. However, quite often, such specification documentation is either missing or carries outdated information due to the evolutionary nature of the software development process. As a result, system operators, developers, and users face difficulties during the production phase due to limited or no information. The problems get even more serious in safety-critical systems. Safety-critical systems are used in many important tasks such as automotive, disaster relief operations, monitoring patient's medical health, and more. In this thesis, we attempt to address the problem of mining missing or outdated software requirement specifications from system traces. We present several approaches to enable system operators to better understand software behavior. We present three tools QMine, MMTQ, and MINTS for mining software specifications from system traces. QMine and MMTQ perform template-based mining for a quantitative regular expression and timed quantitative regular expression with linear time complexity respectively. We propose a novel formalism of timed-quantitative regular expressions that incorporate both events, quantitative values, and time constraints all within a single specification. We realize the limitations of QMine and MMTQ with the need for a human-crafted template as their basis. In an attempt to alleviate this issue, we propose, MINTS a framework that extracts system behavior using traces from the system in an unsupervised approach. MINTS is capable of revealing various system states and the relationship among the state transitions. It then extracts dominant temporal patterns from the extracted relationship model. We use system traces from a custom-built Hexacopter that uses QNX operating system for extracting the dominant temporal patterns. We subsequently mine the quantitative properties using the templates extracted by MINTS for validation. We discuss the soundness and completeness of our frameworks along with their applicability in various industrial settings. Our frameworks are scalable and have been deployed on various industry strength traces.Science, Irving K. Barber Faculty of (Okanagan)Computer Science, Mathematics, Physics and Statistics, Department of (Okanagan)Graduat