Analysis of real-time programs with simple time Petri nets

ABSTRACT

We present a first report on our PARTS toolset for the automated static analysis of real-time systems. The PARTS toolset is based upon a timed extension of Petri nets.Our simple time Petri nets or STP nets are specifically aimed at facilitating real-time analysis. Our analysis approach uses the state space of an STP net in order to answer queries about the concurrency and timing behavior of the corresponding system. An attractive feature of STP nets is that they support a variety of techniques for controlling the number of states that must be explicitly enumerated. These techniques were originally defined for the analysis of concurrency properties of untimed systems, and in this paper we discuss the extension of each to the timed domain.We also report on some preliminary experimental results that we obtained by running our toolset on examples of real-time systems.

REFERENCES

• 1: Gérard Berthelot, Checking properties of nets using transformation, Advances in Petri Nets 1985, covers the 6th European Workshop on Applications and Theory in Petri Nets-selected papers, p.19-40, June 01, 1985
• 2: Bernard Berthomieu , Michel Diaz, Modeling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE Transactions on Software Engineering, v.17 n.3, p.259-273, March 1991 [doi>10.1109/32.75415]
• 3: Ugo Buy , Robert Sloan, A Petri-net-based approach to real-time program analysis, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
• 4: J. Corbett , G. Avrunin, A practical technique for bounding the time between events in concurrent real-time systems, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.110-116, June 28-30, 1993, Cambridge, Massachusetts, United States
• 5: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 6: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Using state space reduction methods for deadlock analysis in Ada tasking, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.51-60, June 28-30, 1993, Cambridge, Massachusetts, United States
• 7: Carlo Ghezzi , Dino Mandrioli , Sandro Morasca , Mauro Pezzè, A Unified High-Level Petri Net Formalism for Time-Critical Systems, IEEE Transactions on Software Engineering, v.17 n.2, p.160-172, February 1991 [doi>10.1109/32.67597]
• 8: Patrice Godefroid , Pierre Wolper, Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.332-342, July 01-04, 1991
• 9: C. L. Heitmeyer , R. D. Jeffords , B. G. Labaw, Comparing different approaches for specifying and verifying real-time systems, Proceedings of the tenth IEEE workshop on Real-time operating systems and software, p.122-129, March 1993, New York, New York, United States
• 10: N. D. Jones, L. H. Landweber, and Y. E Lien. Complexity of some problems in Petri nets. Theoretical Comput. Sci., 4:277-299, 1977.
• 11: P. Merlin and D. Faber. Recoverability of communication protocols~implicafions of a theoretical study. IEEE Trans. Communications, COM-24(9):381-404, Sept. 1976.
• 12: Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Compiling Real-Time Specifications into Extended Automata, IEEE Transactions on Software Engineering, v.18 n.9, p.794-804, September 1992 [doi>10.1109/32.159837]
• 13: C. Ramchandani, ANALYSIS OF ASYNCHRONOUS CONCURRENT SYSTEMS BY TIMED PETRI NETS, Massachusetts Institute of Technology, Cambridge, MA, 1974
• 14: R. H. Sloan and U. Buy. Reduction rules for time Petri nets, 1994. Submitted for publication to/aformation Pros/rig Letters.
• 15: R. H. Sloan and U. Buy. Stubborn sets for real-time Petri nets. Submitted to 15th ~ Real-Time Systems Symposium, 1994.
• 16: P. H. Starke, Reachability analysis of Petri nets using symmetries, Systems Analysis Modelling Simulation, v.8 n.4-5, p.293-303, 1991
• 17: R.N. Taylor. Complexity of analyzing the synchronization structure ofconon'rent programs. Acta Informatica, 19:57-84, 1983.
• 18: S. Tu, S. M. Shatz, and T. Murata. Applying Petri net reduction to support Ada-tasking deadl~ analysis. In Proc. Eleventh lnternat. Conference on Distributed Computing Systems, pages 96-103, Paris, France, 1990,
• 19: A. Valmari. Error detection by reduced reac~bility graph generation. In Proc. of the Ninth European Workshop on the Application and Theory of Petri Nets, pages 95-112, Venice, Italy, 1988.
• 20: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 21: Tomohiro Yoneda , Atsufumi Shibayama , Bernd-Holger Schlingloff , Edmund M. Clarke, Efficient Verification of Parallel Real-Time Systems, Proceedings of the 5th International Conference on Computer Aided Verification, p.321-346, June 28-July 01, 1993
• 22: W. M. Zuberek. Timed Petri nets: Definitions, properties, and applications. Microelectronics and Reliability, 31(4):627-644, 1991.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Routing and layout; Computations on discrete structures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Path and circuit problems

General Terms:
Algorithms, Experimentation, Performance, Reliability