Information extraction for run -time formal analysis

The rapid increase in the significance of software systems has made software assurance a critical requirement in the information age. Formal verification of system design and testing system implementation with a variety of inputs have been used for this purpose. However, verifying a design cannot guarantee the correctness of an implementation. Although testing is performed on an implementation, it does not give formal guarantees because it is impossible to test exhaustively. We propose a complementary solution to the weaknesses of formal verification and testing by monitoring execution of a program and checking its correctness against formally specified properties at run-time. We call this methodology run-time formal analysis. Run-time formal analysis aims to assure the correctness of the current execution at run-time. Run-time formal analysis is performed based on a formal specification of system requirements. We investigate general issues for run-time formal analysis. We show that the set of properties that run-time formal analysis can detect is a subset of safety properties. Furthermore, we show that the checking of a property written in an expressive specification language such as CCS is NP-complete due to nondeterminism. Finally, we discuss the abstraction of the program execution for reducing the amount of data being monitored and analyzed. We have designed a Monitoring and Checking (MaC) architecture for run-time formal analysis. A salient aspect of the MaC architecture is the use of a formal requirement specification to check run-time execution of the target program. For specifying formal requirements, we have designed the Primitive Event Definition Language (PEDL) and the Meta Event Definition Language (MEDL). Another important aspect of the MaC architecture is its flexibility. The architecture clearly separates monitoring implementation-dependent low-level behavior and checking high-level behavior with regard to formal requirement specifications. This modularity allows the architecture to be extended for broad target application areas. In addition, the architecture instruments the target program and analyzes the execution of the target program automatically based on given formal requirement specifications. We have implemented a MaC prototype for Java programs called Java-MaC and showed the effectiveness of the MaC architecture through several case studies. The main thesis of this dissertation is that run-time formal analysis can assure users of the correctness of software systems in a practical manner that is flexible, automatic, and easy to use. This dissertation describes the issues and design solution of the MaC architecture to support this thesis