Static analysis of synchronous programs in multi-clocked embedded systems - Embedded.com

Static analysis of synchronous programs in multi-clocked embedded systems

In this paper, we propose a sound abstraction for an efficient static analysis of synchronous programs describing multi-clock embedded systems. This abstraction combines the Boolean theory and numeric interval approximation to adequately address clock relations defined as combinations of logical and numerical expressions.

Through a few examples, we show how the proposed solution is used to determine absence of reaction captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of component activations via clock inclusion.

We also show this analysis improves the quality of the code generated automatically by the SIGNAL compiler, e.g., a code with smaller footprint, or a code executed more efficiently thanks to optimizations enabled by the new abstraction.

We propose a sound Boolean-interval abstraction for the static analysis of synchronous programs defining multi-clocked embedded systems in SIGNAL. Our solution permits an analysis that significantly enhances the quality of the subsequent code generated automatically by the compiler, e.g., a code with smaller footprint, or a code executed more efficiently thanks to further optimizations.

In the new abstraction, every signal in a program is associated with a pair of the form (clock, value), where clock is a Boolean function and value is a Boolean or numeric function, abstracted as an interval.

Given the level of performance reached by recent progress in Satisfiability Modulo Theory (SMT), we use an SMT solver to implement the reasoning on the new abstraction.

We show through a few examples, how relations between abstract clocks defined with numerical and logical expressions can be adequately analyzed, to determine for instance absence of reactivity captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of computation node activations via clock inclusion.

To read this external content in full, download the paper from the author archives.

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.