Fine grained error or failure detection is often indispensable for precise, effective, and efficient reactions to runtime problems. In this chapter we describe an approach that facilitates automatic generation of efficient runtime detectors for relevant classes of functional problems. The technique targets failures that commonly manifest at the boundaries between the components that form the system. It employs a model-based specification language that developers use to capture system-level properties extracted from requirements specifications. These properties are automatically translated into assertion-like checks and inserted in all relevant locations of the systems code.
The main goals of our research are to define useful classes of system-level properties, identify errors and failures related to the violations of those properties, and produce assertions capable of detecting such violations. To this end we analyzed a wide range of available software specifications, bug reports for implemented systems, and other sources of information about the developers intent, such as test suites. The collected information is organized in a catalog of requirements-level property descriptions. These properties are used by developers to annotate their system design specifications, and serve as the basis for automatic assertion generation.