Min Zhang (ECNU)

Title: An SMT-based Approach to the Formal Analysis of Clock
Constraints Specification Language

Abstract: Clock Constraint Specification Language (CCSL) is a
formal language used to specify the constraints of clocks. Given a
set of clock constraints specified in CCSL, it is desired to know
if there exists a schedule that satisfies all the constraints, if
the constraints are valid or not, and if the constraints satisfy
some expected properties. In this talk, we will explain an
SMT-based approach to the formal analysis of Clock Constraints
Specification Language. In our approach, we encode CCSL
constraints into an SMT problem, and use an SMT solver Z3 to check
if there exists a desired schedule to a set of CCSL constraints.
We also show how the approach can be used to check the existence
of periodic schedules of CCSL constraints.