Logical Clock Constraint Specication in PVS
Qingguo Xu, Robert de Simone, Julien Deantoni · 2015
Abstract: The Clock Constraint Specification Language (CCSL), first introduced as a companion language for Modeling and Analysis of Real-Time and Embedded systems (MARTE), has now evolved beyond the time specification of MARTE, and has become a full-fledged domain specific modeling language widely used in many domains. This report demonstrates the encoded PVS (Prototype Verification System) theories for interpreting clock relation and clock expression based on schedules as a sequence of clock set. In order to ensure the correctness of the encodings, we prove some interesting properties about the clock constraint. Finally, we give an example to illustrate the approach. Key-words: CCSL, Syntax & semantics, PVS 1 School of Computer Engineering and Science, Shanghai University – [email protected] 2 INRIA Sophia Antipolis Mediterranee AOSTE – [email protected] 3 University of Nice Sophia Antipolis, University of Nice Sophia Antipolis, – [email protected] † This work is partially supported by the Natural Science Foundation of China (Grant No. 61170044).