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.

Felder, M., Ghezzi, C., Pezze', M. (1993). Analyzing refinements of state based specifications: the case of TB nets. In Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis (pp.28-39). Association for Computing Machinery.

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

PEZZE', MAURO
1993

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.
paper
Software Analysis, Software Refinements, Petri Nets
English
International Symposium on Software Testing and Analysis
Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis
0-89791-608-5
1993
28
39
none
Felder, M., Ghezzi, C., Pezze', M. (1993). Analyzing refinements of state based specifications: the case of TB nets. In Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis (pp.28-39). Association for Computing Machinery.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/15740
Citazioni
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
Social impact