Towards a compositional approach for automatic monitoring of software systems

The need for reliable software is evident. Despite rigorous use of model checking, testing, and other technological innovations in software development, there exist faults which elude those detection efforts and do not surface until the software is operational. These faults may lead to software failures with serious consequences. Given that, it is very important to have tools that can be used for online monitoring of software systems during their operations.;A nondeterministically specified target system may show different, nevertheless legal behaviors for the same set of stimuli from the environment. To monitor such a system, the monitor must be able to consider all possible legal behavioral alternatives to avoid erroneous reports. The large number of behavioral alternatives required to be considered by the monitor result in large computational costs for error/failure detection. This work presents a monitoring technique which alleviates the state explosion problem by avoiding the construction of a global state graph from the parallel composition of individual component specifications of a concurrent system.;Compositional reasoning has been employed successfully for the task of specification and verification to handle the complexity of large concurrent systems. However, compositional reasoning has not been investigated extensively for the operational stage monitoring of software. The fundamental principle of compositionality is to show that the whole implementation behaves correctly (according to its specification) if all of its components behave correctly in isolation (according to the component specifications). This thesis presents a compositional approach to automatic monitoring of software systems. The monitoring approach incorporates the modularity and compositionality concepts of verification into the operational stage of software. Compositional monitoring achieves global system monitoring by analyzing the behaviors of the components of a system individually, and then combining the results obtained from the independent component analyses.;The compositional monitor described in the thesis is stable state driven. It passively observes the external inputs and outputs, receives partial state information of the target system, and reports certain kinds of errors and failures. Reasoning about errors or failures requires knowledge about the expected behavior of the target system. The thesis considers the case where the requirements specification of the target system is, or could be expressed in a formalism based on communicating finite state machines with addressing variables. The monitor utilizes the target system's specification information and determines whether an error or failure has occurred in the target system. It can also be used for test support, fault localization, and software reliability instrumentation. The monitor is suitable for concurrent, reactive, discrete, real-time, and failure sensitive software systems.;The thesis presents an assume-guarantee paradigm for software monitoring. The basic idea of the assume-guarantee (A/G) monitor is to reason about a component by stating the assumptions about its environment, and then prove that these assumptions are satisfied by the environment. (Abstract shortened by UMI.).