Software systems rely on events for logging, coordination, handling unusual situations, and more. Monitoring events from systems that provide services can ensure that the service complies with policies, regulations, and other business rules. Notably, detecting violations of rules as early as possible is much desired as, for example, the service may reclaim resources from erring enactments. The primary goal of this paper is to develop techniques for detecting rule violations as early as possible. We formalize a model for events and a language to specify constraints on event timing and data. We develop algorithms to detect violations of individual rules at the earliest possible time, then use a chase process to detect violations of acyclic sets of rules. We also present optimization techniques to reduce monitoring overhead. Finally, we implement and evaluate our algorithms through experiments to demonstrate our approach is feasible and beneficial.

Business services are provided by enacting interrelated business processes. Service providers must ensure enactments comply with policies, regulations, and business rules, including rules with quantitative time constraints. Enforcing such rules at design-time may be too restrictive, so effective service provisioning includes expressing rules in a formal specification language and detecting violations of these rules at runtime. Many specification languages do not include quantitative time constraints; for languages with such constraints, it is often unknown if they have runtime monitors whose auxiliary data storage is of bounded size. In this paper, we formulate a technical model of services, a logic language with quantitative time constraints for specifying rules, and develop techniques for automatically generating monitors to detect rule violations. This approach involves two steps, translating: (1) rules to formulas in linear temporal logic (LTL) on finite traces, and (2) LTL formulas to finite state machines. Since algorithms exist for step (2), we focus on step (1), i.e., mapping rules to equivalent LTL formulas. We present and establish the correctness of two translation techniques for “singly-linked” rules. We also compare the size of formulas produced by these techniques with a method of translation derived from Kamp’s Theorem, showing an improvement from hyper-exponential to exponential size.