Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software

摘要: We report on a successful preliminary experience in the design and implementation of special-purpose Abstract Interpretation based static program analyzer for verification safety critical embedded real-time software. The is both precise (zero false alarm considered experiment) efficient (less than one minute analysis 10,000 lines code). Even if it simple interval analysis, many features have been added to obtain desired precision: expansion small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between counters other variables. efficiency tool mainly comes from clever representation abstract environments balanced binary search trees.