Assertion-Based Flow Monitoring of SystemC Models

SystemC is the de facto system modeling language, and verification of SystemC models is a major research direction. Assertion-Based Monitoring is a dynamic verification technique that allows the user to dynamically verify formal properties of the system by automatically generating runtime monitors from them. A typical hardware-software system is concurrent and reactive. Examples of such systems can be a computer, an ATM server etc. Such systems perform multiple jobs of different types during their execution. For example, different types of jobs in a computer can be ‘launching a web browser’, ‘searching the file system’ etc. A job can be submitted by an external user or generated by an internal component of the system. A job can begin at any point in time during the execution of the system, the beginning time being completely unknown beforehand. A job begins with a set of inputs, travels from one system component to another to generate a set of outputs and ends after a finite amount of time. Since a job “flows” among the system components, we call it a flow. In a concurrent system multiple flows can begin and travel though the system at the same time. This work focuses on verifying formal properties about these dynamic and concurrent flows (called flow properties) in a concurrent reactive system, modeled in SystemC. The contribution of this thesis is three fold: First, a light-weight C++ library, called iii Flow Library, that enables modeling of flows in SystemC in a structured manner. Second, an algorithm, implemented in the FlowMonGen tool, to generate C++ monitor class from a flow property, which is an LTL formula interpreted over the finite trace of a flow. Third, a dynamic and decentralized algorithm to monitor the concurrent flows in a SystemC model. Our completely automated and efficient Flow Monitoring Framework implements this algorithm