ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre

Abstract—We present an approach to connect the Real-Time Calculus (RTC) method to the syn-chronous data-flow language Lustre, and its associ-ated tool-chain, allowing the use of techniques like SMT-solving and abstract interpretation which were not previously available for use with RTC. The ap-proach 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 evalu-ate 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