ac2lus: Bringing SMT-Solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre

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 variable of the components, like buffer sizes. Compared to existing approaches to connect RTC to other formalisms, we believe that the use of Lustre, a real programming language, and the synchronous hypothesis make the task easier to write models, and we show that it allows a great flexibility of the tool itself, with many variants to fine-tune the performances.