On timed components and their abstraction

ABSTRACT

We develop a new technique for generating small-complexity abstractions of timed automata that provide an approximation of their timed input-output behavior. This abstraction is obtained by first augmenting the automaton with additional input clocks, computing the "reachable" timed automaton that corresponds to the augmented model and finally "hiding" the internal variables and clocks of the system. As a result we obtain a timed automaton that does not allow any qualitative behavior which is infeasible due to timing constraints, and which maintains a relaxed form of the timing constraints associated with the feasible behaviors. We have implemented this technique and applied it to several examples from different application domains.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Timed regular expressions, Journal of the ACM (JACM), v.49 n.2, p.172-206, March 2002 [doi>10.1145/506147.506151]
• 3: R. Ben Salah, M. Bozga and O. Maler, On Timing Analysis of Combinational Circuits, FORMATS'03, 204--219, LNCS 2003.
• 4: Marius Bozga , Susanne Graf , Laurent Mounier, IF-2.0: A Validation Environment for Component-Based Real-Time Systems, Proceedings of the 14th International Conference on Computer Aided Verification, p.343-348, July 27-31, 2002
• 5: Conrado Daws , Stavros Tripakis, Model Checking of Real-Time Reachability Properties Using Abstractions, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.313-329, March 28-April 04, 1998
• 6: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
• 7: Oded Maler , Amir Pnueli, Timing analysis of asynchronous circuits using timed automata, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.189-205, October 02-04, 1995
• 8: O. Maler, D. Nickovic and A. Pnueli, Real Time Temporal Logic: Past, Present, Future, FORMATS'05, 2--16, LNCS 3829, Springer, 2005.
• 9: Joseph Sifakis , Sergio Yovine, Compositional Specification of Timed Systems (Extended Abstract), Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science, p.347-359, February 22-24, 1996
• 10: Ernesto Wandeler , Alexander Maxiaguine , Lothar Thiele, Quantitative Characterization of Event Streams in Analysis of Hard Real-Time Applications, Real-Time Systems, v.29 n.2-3, p.205-225, March 2005 [doi>10.1007/s11241-005-6885-x]
• 11: H. Zheng, E. Mercer, and C. J. Myers, Modular verification of timed circuits using automatic abstraction, IEEE Trans. on CAD 22, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.13 Reusable Software
            Subjects: Reuse models

General Terms:
Verification

Keywords:
abstraction, components, timed automata