Automatic Abstraction for Worst-Case Analysis of Discrete Systems

c Abstraction for Worst-Case Analysis of Discrete Systems Felice Balarin Cadence Berkeley Laboratories Recently, a methodology for worst-case analysis of discrete systems has been proposed [1, 2]. The methodology relies on a user-provided abstraction of system components. In this paper we propose a procedure to autoy generate such abstractions for system components with Boolean transition functions. We use a binary decision diagram (BDD) of the transition function to generate a formula in Presburger arithmetic representing the desired abstraction. Our experiments indicate that the approach can be applied to control-dominated embedded systems.

• Type: Conference
• Year: 2000
• Where: DATE
• Authors: Felice Balarin
• Keywords: Abstractions, DATE 2000, Discrete Systems, Hardware, Worst-case Analysis