STARS of MPEG decoder: a case study in worst-case analysis of discrete-event systems

ABSTRACT

STARS (STatic Analysis of Reactive Systems) is a methodology for worst-case analysis of discrete systems. Theoretical foundations of STARS have been laid down [1, 2, 3], but no implementation has been presented so far. We introduce an implementation of STARS as an extension of YAPI, a programming interface used to model signal processing applications as process networks [7]. We apply STARS to a YAPI model of an MPEG decoder. We show that worst-case bounds computed by STARS are quite close to simulated values (within 15%). We also show that additional effort by the designer required to build STARS models is very small compared to effort of building the YAPI simulation model, and that the run times of STARS are negligible compared to the simulation run times.

REFERENCES

• 1: Felice Balarin, Worst-case analysis of discrete systems, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.347-353, November 07-11, 1999, San Jose, California, United States
• 2: Felice Balarin, Worst-case analysis of discrete systems based on conditional abstractions, Proceedings of the seventh international workshop on Hardware/software codesign, p.115-119, March 1999, Rome, Italy [doi>10.1145/301177.301502]
• 3: Felice Balarin, Automatic abstraciton for worst-case analysis of discrete systems, Proceedings of the conference on Design, automation and test in Europe, p.494-501, March 27-30, 2000, Paris, France [doi>10.1145/343647.343830]
• 4: J. Buck, S. Ha, E.A. Lee, and D.G. Masesrhmltt. Ptolemy: a framework for simulating and prototyping heterogeneous systems. Interntionai Journal of Computer Simulation, special issue on Simulation So,ware Development, January 1990.
• 5: Cadence virtual component co-design (VCC) environment http://www.cadence.com/datasheete/vcc-environment. html.
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: E. A. de Kock , W. J. M. Smits , P. van der Wolf , J.-Y. Brunel , W. M. Kruijtzer , P. Lieverse , K. A. Vissers , G. Essink, YAPI: application modeling for signal processing systems, Proceedings of the 37th conference on Design automation, p.402-405, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337511]
• 8: Pieter van der Wolf , Paul Lieverse , Mudit Goel , David La Hei , Kees Vissers, An MPEG-2 decoder case study as a driver for a system level design methodology, Proceedings of the seventh international workshop on Hardware/software codesign, p.33-37, March 1999, Rome, Italy [doi>10.1145/301177.301196]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING

General Terms:
Documentation, Experimentation, Management

Keywords:
static analysis, system verification, worst-case analysis