Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs
- 499 Downloads
Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system.
KeywordsTime Petri nets Quantitative robustness Parameter synthesis
Unable to display preview. Download preview PDF.
- 4.André, É., Soulat, R.: The Inverse Method. FOCUS Series in Computer Engineering and Information Technology. ISTE Ltd and John Wiley & Sons Inc. (2013)Google Scholar
- 7.Fribourg, L., Kühne, U.: Parametric verification and test coverage for hybrid automata using the inverse method. IJFCS 24(2), 233–249 (2013)Google Scholar
- 9.Markey, N.: Robustness in real-time systems. In: SIES, pp. 28–34. IEEE Computer Society Press (2011)Google Scholar
- 10.Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA, USA (1974)Google Scholar
- 11.Sankur, O.: Shrinktech: A tool for the robustness analysis of timed automata. In: CAV. LNCS. Springer (to appear, 2013)Google Scholar
- 12.Traonouez, L.-M.: A parametric counterexample refinement approach for robust timed specifications. In: FIT. EPTCS, vol. 87, pp. 17–33 (2012)Google Scholar