Analyzing refinements of state based specifications: the case of TB nets

ABSTRACT

We describe how formal specifications given in terms of a high-level timed Petri net formalism (TB nets) can be analyzed to check the temporal properties of bounded invariance (the systems stays in a given state until time &tgr;) and bounded response (the system will enter a given state within time &tgr;). In particular, we concentrate on specifications given in a hierarchical, top-down manner, where one specification level refines a more abstract level. Our goal is to define the conditions under which the properties that are proven to hold at a given abstraction level are preserved at the next refined level. To do so, we define the concept of correct refinement, and we show that bounded invariance and bounded response are preserved by a correct refinement. We also provide a set of constructive rules that may be applied to refine a net in such a way that the resulting net is a correct refinement.

REFERENCES

• AH: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• Aiz: Jacob Itzhack Aizikowitz, Designing distributed services using refinement mappings, Cornell University, Ithaca, NY, 1990
• Apt: Krzysztof R. Apt, A Static Analysis of CSP Programs, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.1-17, June 06-08, 1983
• DDGJ: Datum W., Dohmen G., Volker G., Josko B.: "Modular verification of Petri nets, the temporal logic approach" Proceedings of CAV 1990, LNCS 430.
• GG: R. van Glabbeek , U. Goltz, Refinement of actions in causality based models, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.267-300, May 1990, Mook, The Netherlands
• GMMP: 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]
• GMP: Ghezzi C., Morasca S., Pezzd M.: "Timing analysis of time basic nets", submitted for publication.
• Hen: Thomas A. Henzinger, Sooner is safer than later., Stanford University, Stanford, CA, 1991
• HMP: Tom Henzinger , Zohar Manna , Amir Pnueli, Temporal proof methodologies for real-time systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.353-366, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99629]
• JRT: The Journal of Real-Time Systems, Special issue on the Esprit IPTES project, 5, 235-248 (1993), Kluwer Academic Publisher.
• MF: Merlin P.M., Farber D.J.: "Recoverability of Communication Protocols: Implications of a Theoretical Study", IEEE Transactions on Communications, Vol. COM-24, September 1976.
• Rei: Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
• Sof: IEEE Software, Special Issue on Formal Methods, Vol. 7, No. 5, September 1990.
• Tay: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• TSE: N. G. Leveson, Guest Editor's Introduction: Formal Methods in Software Engineering, IEEE Transactions on Software Engineering, v.16 n.9, p.929-931, September 1990
• Vog: Walter Vogler, Failures semantics based on interval semiwords is a convergence for refinement, Proceedings of the seventh annual symposium on Theoretical aspects of computer science, p.285-297, February 1990, Rouen, France
• YY: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Design, Verification