Monitoring and testing based on multi-level program specifications

Research on formal methods of software development and verification focuses on building specifications using incremental and iterative development methodologies. The presence of several levels of specifications simplifies proving of properties, since it is possible to reuse the proofs that were performed for more abstract layers of the model. It is desirable to use the same models that were used for formal verification also in testing of real systems for compliance with the requirements set by these models. In practice, large software systems are described by multi-level models. There was no experience of using such models as the basis for testing and monitoring. The paper discusses various methods for developing multi-level models, new opportunities that can be obtained through a combination of functional specifications and implementation-level refinements, limitations that must be considered during testing and monitoring of real systems for compliance with multi-level models.