RETRACTED: Calculus-based Runtime Verification (Retracted Article)

In this paper, a uniform calculus-based approach for synthesizing monitors checking correctness properties specified by a large variety of logics at runtime is provided, including future and past time logics, interval logics, state machine and parameterized temporal logics. Thus we can synthesize monitors from the logical specification in an uniform fashion to incrementally analysis the current execution traces during test and real run. The monitor detects both good and bad prefix of a particular kind, namely those that are informative for the property under investigation.