Timing is a key issue in reactive programming, a development paradigm suited to the design and implementation of safety-critical systems such as control and navigation devices that closely interact with their environment. While integrating some time specifications is possible in unified modeling language 2 (UML2), its time model is too limited to deal with the asynchronous and synchronous behaviors found in real-life situations. The Object Management Group (OMG)-sanctioned MARTE UML profile is an extension of the time model and comes with a powerful time specification framework: clock constraint specification language (CCSL). This paper provides a formal specification and one simple use case for CCSL.

CCSL is based on time structures, which are sets of clocks seen as discrete or dense sets of instants, and sets of precedence relations between them. One can use CCSL to specify the constraints that such clocks must satisfy, such as sub-clocking or synchronization relationships. These constraints can be either synchronous or asynchronous. One can run a given CCSL specification on the TimeSquare simulator that generates sets of possible instant histories. To illustrate CCSL, a digital video filtering application is used throughout the paper. In particular, the authors show how its Esterel implementation can be verified against its CCSL specification, by adding observer code that generates exceptions if one clock constraint is not satisfied at a particular time.

This paper, although lacking in focus, can be of use to readers interested in learning more about timing considerations in current advanced development environments for reactive systems.