A Sampling Semantics of Duration Calculus

 In the paper, the problem of discretization of continuous time in Duration Calculus (DC) is addressed. For a DC formula $D$, for a sampling step $h$, a sampling semantics of $D$ is defined to express the properties of discrete observations of its models, while original semantics of $D$ expresses the properties of the models. In practice, only sampling semantics is implemented. So, an implementation $D$ of a system specified by $S$, both are assumed to be written in DC, is correct iff sampling semantics of $D$ implies original semantics of $S$. Some rules for proving the correctness of an implementation are given. The problem of digitization is also considered in the paper. Some forms of digitizable DC formulae are shown. Then we apply the obtained results for a non-trivial example, namely, a Biphase Mark Protocol. That protocol uses 18-cycle cell for a bit of message. A cell is formed by 5-cycle mark subcell followed by 13-cycle code subcell. We adopt the same assumptions about physical environment as in the literature. However, we are able to show stronger property: The protocol works correctly provided clock rate between writer's and reader's is within $30\%$.