Abstract
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 automaton(PTIA), which is a subset of a parametric timed automaton[1]. 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[2]. 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[3]. We also apply our proposed equivalence checking algorithm to vulnerability checking for timing attack on web privacy.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proc. 25th ACM Annual Symp. on the Theory of Computing (STOC 1993), pp. 592–601 (1993)
de Frutos, D., López, N., Núñez, M.: Global timed bisimulation: An introduction. In: Proc. of FORTE/PSTV 1999, pp. 401–416 (1999)
Nakata, A., Higashino, T., Taniguchi, K.: Time-action alternating model for timed LOTOS and its symbolic verification of bisimulation equivalence. In: Proc. of FORTE/PSTV 1996, IFIP, pp. 279–294. Chapman & Hall, Boca Raton (1996)
Xu, J.: On inspection and verification of software with timing requirements. IEEE Trans. on Software Engineering 29, 705–720 (2003)
Sifakis, J., Tripakis, S., Yovine, S.: Building models of real-time systems from application software. Proceedings of the IEEE 91, 100–111 (2003)
Wang, F.: Parametric timing analysis for real-time systems. Information and Computation 130, 131–150 (1996)
Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138, 353–389 (1995)
Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)
Li, Z., Chen, H.: Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes. In: Proc. of Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 300–314 (1999)
Larsen, K.G., Wang, Y.: Time abstracted bisimulation: Implicit specifications and decidability. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 160–175. Springer, Heidelberg (1994)
Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)
Felten, E.W., Schneider, M.A.: Timing attacks on web privacy. In: 7th ACM Conference in Computer and Communication Security, pp. 25–32 (2000)
Focardi, R., Gorrieri, R., Lanotte, R., Maggiolo-Schettini, A., Martinelli, F., Tini, S., Tronci, E.: Formal models of timing attacks on web privacy. Electronic Notes in Theoretical Computer Science 62 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tanimoto, T., Sasaki, S., Nakata, A., Higashino, T. (2004). A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive