Monitoring software requirements using instrumented code

Ideally, software is derived from requirements whose properties have been established as good. However, it is difficult to define and analyze requirements. Moreover derivation of software from requirements is error prone. Finally, the installation and use of compiled software can introduce errors. Thus, it can be difficult to provide assurances about the state of a software\´s execution. We present a framework to monitor the requirements of software as it executes. The framework is general, and allows for automated support. The current implementation uses a combination of assertion and model checking to inform the monitor. We focus on two issues: (1) the expression of "suspect requirements", and (2) the transparency of the software and its environment to the monitor. We illustrate these issues with the widely known problems of the Dining Philosophers and the CCITT X.509 authentication. Each are represented as Java programs which are then instrumented and monitored.