A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata

摘要

In the development of real-time (communicating) hardware or embedded-software systems, it is frequently the case that we want to refine/optimize the system's internal behavior while preserving the external timed I/O behavior (that is, the interface protocol). In such a design refinement, modification of the systems' internal branching structures, as well as re-scheduling of internal actions, may frequently occur. Our goal is, then, to ensure that such branch optimization and re-scheduling of internal actions preserve the systems' external timed behavior, which is typically formalized by the notion of (timed) failure equivalence since it is less sensitive to the difference of internal branching structures than (timed) weak bisimulation. In order to know the degree of freedom of such re-scheduling, parametric analysis is useful. The model suitable for such an analysis is a parametric time-interval au-tomaton(PTIA), which is a subset of a parametric timed automaton. It has only a time interval with upper- and lower-bound parameters as a relative timing constraint between consecutive actions. In this paper, at first, we propose an abstraction algorithm of PTIA which preserves global timed bisimulation. Global timed bisimulation is weaker than timed weak bisimulation and a sufficient condition for timed failure equivalence. Then, we also show that after applying our algorithm, the reduced PTIA has no internal actions, and thus the problem deriving a parameter condition in order that given two models are global timed bisimilar can be reduced to the existing parametric strong bisimulation equivalence checking. We also apply our proposed equivalence checking algorithm to vulnerability checking for timing attack on web privacy.