Karine Altisen and Matthieu Moy
ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre (2010)
ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre (2010)
TR-2010-2.pdf
Keywords: Real-Time Calculus, Lustre, Modular Performance Analysis, Observer, Formal methods
Abstract: We present an approach to connect the Real-Time Calculus 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, that relies on Nbac and Kind proof engines. This allows to find upper and lower bounds on arbitrary values of a component (like its buffer size), or to compute output arrival curves, allowing a modular analysis of a system made of multiple components. 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 for the user to write models, and we show that it allows a great flexibility of the tool itself, which already implements 6 variants of adapters with different performance results.
