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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.