Logical Clock Constraint Specification in PVS
Xu, Qingguo, Robert de Simone, Julien Deantoni · HAL (Le Centre pour la Communication Scientifique Directe) · 2015
The Clock Constraint Specification Language (CCSL), first introduced as a companion language for Modeling andAnalysis of Real-Time and Embedded systems (MARTE), has now evolved beyond the time specification of MARTE, and hasbecome a full-fledged domain specific modeling language widely used in many domains. This report demonstrates the encodedPVS (Prototype Verification System) theories for interpreting clock relation and clock expression based on schedules as asequence of clock set. In order to ensure the correctness of the encodings, we prove some interesting properties about the clockconstraint. Finally, we give an example to illustrate the approach.