A formal monitoring-based framework for software development and analysis

Abstract. A formal framework for software development and analysis is presented, which aims at reducing the gap between formal specifi-cation and implementation by integrating the two and allowing them together to form a system. It is called monitoring-oriented programming (MOP), since runtime monitoring is supported and encouraged as a fun-damental principle. Monitors are automatically synthesized from formal specifications and integrated at appropriate places in the program, ac-cording to user-configurable attributes. Violations and/or validations of specifications can trigger user-defined code at any points in the program, in particular recovery code, outputting/sending messages, or raising ex-ceptions. The major novelty of MOP is its generality w.r.t. logical for-malisms: it allows users to insert their favorite or domain-specific spec-ification formalisms via logic plug-in modules. A WWW repository has been created, allowing MOP users to download and upload logic plug-ins. An experimental prototype tool, called Java-MOP, is also discussed, which currently supports most but not all of the desired MOP features.