TY - JOUR
T1 - Towards monitoring-oriented programming
T2 - A paradigm combining specification and implementation
AU - Chen, Feng
AU - Roşu, Grigore
N1 - This work has been partially supported by the European Union under the ESPRIT III Basic Research Project 8820-AMATIST and by the U.K. government funded EPSRC TEMSA project, GR/K32692. Special thanks to Jordi Perez whose work with the IFA techniques and tools was invaluable.
PY - 2003/10
Y1 - 2003/10
N2 - With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.
AB - With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.
UR - http://www.scopus.com/inward/record.url?scp=18944375047&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=18944375047&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(04)81045-4
DO - 10.1016/S1571-0661(04)81045-4
M3 - Article
AN - SCOPUS:18944375047
SN - 1571-0661
VL - 89
SP - 108
EP - 127
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 2
ER -