JAIST Logic@JAIST

Toward a Rewriting-based Semantics of Clock Constraint Specification Language and its Applications

  • Zhang Min
Date: 2015/08/27 (Thu) 14:00 to 17:00
Place: JAIST IS school seminar room 9F
Group: Research Center for Software Verification
In UML profile for modelling and analysis of real-time and embedded systems, time model is introduced, where clocks are used to observe and enforce the occurrences of events in systems. The time model comes with a companion language called Clock Constraint Specification Language (CCSL), which is 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 present a rewriting-based semantics of CCSL in Maude and demonstrate three applications of the formal semantics: 1) to find bounded schedules and periodic schedules that can satisfy all the given constraints; 2) to simulate customised schedules by Maude meta-level programming; and 3) to verify desired LTL properties of CCSL constraints by Maude model checking.
Contact Nao Aoki