We present an approach to connect the Real-Time Calculus (RTC) method to the
synchronous data-flow language Lustre, and its associated tool-chain, allowing the use of
techniques like SMT-solving and abstract interpretation which were not previously available
for use with RTC. The approach is supported by a tool called ac2lus. It allows to model the
system to be analyzed as general Lustre programs with inputs specified by arrival curves,
the tool can compute output arrival curves or evaluate upper and lower bounds on any …

We present an approach to connect the Real-Time Calculus (RTC) method to the
synchronous data-flow language Lustre, and its associated tool-chain, allowing the use of
techniques like SMT-solving and abstract interpretation which were not previously available
for use with RTC. The approach is supported by a tool called ac2lus. It allows to model the
system to be analyzed as general Lustre programs with inputs specified by arrival curves;
the tool can compute output arrival curves or evaluate upper and lower bounds on any …