An Executable Semantics of Clock Constraint Specification Language and Its Applications

The Clock Constraint Specification Language (CCSL) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in CCSL, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of CCSL in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: (1) to automatically find bounded or periodic schedules that satisfy all the given constraints; (2) to simulate the execution of schedules with customized simulation policies; and (3) to verify LTL properties of CCSL constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of CCSL are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.