A Formal Monitoring-Based Framework for Software Development and Analysis

A formal framework for software development and analysis is presented, which aims at reducing the gap between formal specification 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 fundamental principle. Monitors are automatically synthesized from formal specifications and integrated at appropriate places in the program, according 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 exceptions. The major novelty of MOP is its generality w.r.t. logical formalisms: it allows users to insert their favorite or domain-specific specification formalisms via logic plug-in modules. A WWW repository has been created, allowing MOP users to download and upload logic plugins. An experimental p...

• Type: Conference
• Year: 2004
• Where: ICFEM
• Authors: Feng Chen, Marcelo d'Amorim, Grigore Rosu
• Keywords: Formal Framework, Formal Specifications, ICFEM 2004, Violations And/or Validations