Automatic abstraction for worst-case analysis of discrete systems
F. Balarin · Proceedings Design, Automation and Test in Europe Conference and Exhibition 2000 (Cat. No. PR00537) · 2002
Recently a methodology for worst-case analysis of discrete systems has been proposed by the author. The methodology relies on a user-provided abstraction of system components. In this paper the author proposes a procedure to automatically generate such abstractions for system components with Boolean transition functions. She use a binary decision diagram (BDD) of the transition function to generate a formula in Presburger arithmetic representing the desired abstraction. The author's experiments indicate that the approach can be applied to control-dominated embedded systems.