A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties
Most mainstream specification languages primarily deal with a program's functional behavior. However, for many common problems, besides the system's functionality, it is necessary to be able to express its temporal properties, such as the necessity of calling methods in a certain order. The authors have developed temporaljmlc, a tool that performs run-time assertion checking of temporal properties specified in an extension of the Java Modeling Language (JML). The benefit of temporaljmlc is that it allows succinct specification of temporal properties that would otherwise be tedious and difficult to specify.