ACKNOWLEDGEMENTS | CONTACT US | PARTNERS | PEOPLE | PUBLICATIONS | RECOGNITION | TECHNOLOGY | FRAMEWORKS
TIMEC-TIME TRACT
TimeC/Time-Tract
TimeC is a light-weight notation for specifying
timing-constraints in common imperative and
object-oriented languages. In other words, TimeC is
notation for expressing temporal relationships between
program points. This notation has been designed
explicitly to provide an easy mechansim for specifying
timing relationships. It is not dependent on the base
language being used to develop the application. Thus, it
can be used, for example, with C, C++ or Java. Most
importantly, the TimeC notation enables a programmer to
easily and definitively decide whether a given embedded
program meets given timing constraints -- commonly
referred to as timing analysis. By contrast, other
mechanisms for specifying timing relationships require
much more complex procedures for performing this
analysis.
The general syntax of TimeC constraints and assertions is
as follows:
| <arg-list> | ::== | <expression> | <expression>, <arg-list> |
| <marker-ref> | ::== | <marker-id> | <marker-id>[<side-condition>] | <marker-ref> (<arg-list>) |
| <ref-list> | ::== | time(<marker-ref>) | time(<marker-ref>), <ref-list> |
| <first-last> | ::== | first | last |
| <basic-ref> | ::== | <marker-ref> | <first-last>(<ref-list>) |
| <present-ref> | ::== | time(<basic-reference>) |
| <next-ref> | ::== | time(next.<marker-ref>) |
| <prev-ref> | ::== | time(prev.<marker-ref>) |
| <diff> | ::== | <present-ref> - <present-ref> | <next-ref> - <present-ref> | <present-ref> - <prev-ref> |
| <timing-constraint> | ::== | <diff> <= | <diff> >= t |
| <requirement-list> | ::== | <timing-constraint> | <timing constraint>; <requirement-list> |
| <requirements> | ::== | Requirements: <requirement-list> |
Program Assumptions
| <constrained-var> | ::== | <program-cariable> | <counter> |
| <program-assumption> | ::== | a <= <constrained-var> | <constrained-var> <= b a, b element of N |
| <assumption> | ::== | <timing-constraint> | <program-assumption> |
| <assumption-list> | ::== | <assumption> | <assumption>; <assumption-list> |
| <assumptions> | ::== | Assumption: <assumption-list> |
| <specifications> | ::== | <requirements> | <assumptions> <requirements> |
Using TimeC, a programmer annotates the application
program being developed between markers which indicate
events of interest in the program. The start of the
execution of a loop is an example of such an event. TimeC
constraints can be used to specify minimum and maximum
amounts of time that can elapse between the events
associated with the markers.
An Example Embedded Program
Consider a program that controls a typical Cardiac
Arrythmia monitor in a modern ICU. The points of the
program of interest will denoted by markers M1, M2,...,
M6 , between which timing relationships are to be
enforced. Markers are associated with "events"
of interest.
The two typical constraints of interest are :
1.. Data is sampled every 30msec (two consecutive
sampling points are never more than 30 msec apart), and
2. Whenever an abnormality (arrythmia) is detected,
software sounds an alarm within 500msec.