Reachability Analysis for Timed Automata Based on Partitioning

• Autorzy: Półrola, A. , Penczek, W. , Szreter, M.

Warianty tytułu

PL

Testowanie osiągalności dla automatów czasowych bazujące na algorytmach podziału

• Języki publikacji: EN

Abstrakty

EN

Model checking is an approach commonly applied for automated verification of reachability properties. Given a system $S$ and a property $p$, reachability model checking consists in an exploration of the state space of $S$, checking whether there exists a state where $p$ holds. Since concrete state spaces (models) of timed systems are usually infinite, they cannot be directly applied to model checking. One of the solution to this problem is to exploit finite abstract models, preseving the properties of interest. The paper presents a new method of buildng abstract models for Timed Automata, based on a partitioning algorithm. Our pseudo-bisimulating models are often smaller than forward-reachability graphs , commonly used in reachability analysis. The method enables verification on-the-fly, i.e., generating of the model can be stopped as soon as a state satisfying $p$ is found.

PL

Automatyczne testowanie osiągalności wykonywane jest zazwyczaj za pomocą metod weryfikacji modelowej. Dla danego systemy S i właściwości p polega ono na przejrzeniu przestrzeni stanów S i sprawdzeniu, czy zawiera ona stan w którym p zachodzi. Istotne znaczenie ma zatem rozmiar przeglądanej przestrzeni (modelu), który w wielu przypadkach (np. dla systemów z czasem) może być nawet nieskończony. Jednym z możliwych rozwiązań jest zastosowanie skończonych modeli abstrakcyjnych zachowujących żądane własności. Praca przedstawia nową metodę generowania modeli abstrakcyjnych dla automatów czasowych, bazujących na algorytmie minimalizacji (podziału). Otrzymywane modele pseudobisymulacyjne zachowują osiągalność, a przy tym są często mniejsze niż używane zwykle do jej testowania tzw. grafy forward-reachability. Metoda pozawala też na wykonywanie weryfikacji "w locie", tj. przerywanie budowania modelu gdy wygenerowany zostanie stan spełniający p.

Słowa kluczowe

EN

model checking; Timed Automata; reachability; abstract models; minimization

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2003
• Tom: Nr 961
• Strony: 1-23

Twórcy

autor

Półrola, A.

• Faculty of Mathematics, University of Lodz, Banacha 22, 90-238 Łódź, Poland,

autor

Penczek, W.

• Institute of Computer Science, PAS Ordona 21, 01-237 Warsaw, Poland ,

autor

Szreter, M.

• Institute of Computer Science, PAS Ordona 21 01-237 Warsaw, Poland ,

Bibliografia

• [ACD+92a] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of the 13th IEEE Real- Time Systems Symposium (RTSS’92), pages 157-166. IEEE Comp. Soc. Press, 1992.
• [ACD+92b] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proc. of the Int. Conf. on Concurrency Theory (CONCUR’92), volume 630 of LNCS, pages 340-354. Springer-Verlag, 1992.
• [ACKS02] G. Audemard, A. Cimatti, A. Korniłowicz, and R. Sebastiani. Bounded model checking for timed systems. Technical Report 0201-05, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy, January 2002.
• [Bey02] D. Beyer. Improvements in BDD-based reachability analysis of Timed Automata. In Proc. of Int. Symp. of Formal Methods Europe (FME’01), volume 2021 of LNCS, pages 318-343. Springer-Verlag, 2002.
• [BFH+92] A. Bouajjani, J-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247-269, 1992.
• [BTY97] A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS’97), pages 232-243. IEEE Comp. Soc. Press, 1997.
• [Dil89] D. Dill. Timing assumptions and verification of finite state concurrent systems. In Automatic Verification Methods for Finite-State Systems, volume 407 of LNCS, pages 197 - 212. Springer- Verlag, 1989.
• [DJJ+03] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, and A. Zbrzezny. Verics: A tool for verifying Timed Automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [DT98] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• [GL91] O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of the Int. Conf. on Concurrency Theory (CONCUR’91), volume 527 of LNCS, pages 250-265. Springer-Verlag, 1991.
• [KL96] I. Kang and I. Lee. An efficient state space generation for the analysis of real-time systems. In Proc. of Int. Symposium on Software Testing and Analysis, 1996.
• [LLPY97] K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structures and state-space reduction. In Proc. of the 18th IEEE Real-Time System Symposium (RTSS’97), pages 14-24. IEEE Comp. Soc. Press, 1997.
• [NTY00] P. Niebert, S. Tripakis, and S. Yovine. Minimum-time reachability for Timed Automata. In Proc.of the 8th IEEE Mediterranean Conf. on Control and Automation (MED’2000), Patros, Greece, July 2000. IEEE Comp. Soc. Press.
• [Pnu77] A. Pnueli. The temporal logic of programs. In Proc. of the 18th Int. Symp. Foundations of Computer Science (FOCS’77), pages 46-57, 1977.
• [PPS02] A. Półrola, W. Penczek, and M. Szreter. Towards refining partitioning for checking reachability in Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), volume 161(2) of Informatik-Berichte, pages 278-291. Humboldt University, 2002.
• [PWZ02] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [Tri98] S. Tripakis. Minimization of timed systems, http://verimag.imag.fr/~tripakis/dea.ps.gz, 1998.
• [TY96] S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Proc. of the 8th Int. Conf. on Computer Aided Verification (CAV’96), volume 1102 of LNCS, pages 232-243. Springer-Verlag, 1996.
• [TY01] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(l):25-68, 2001.
• [WPZ02a] B. Woźna, W. Penczek, and A. Zbrzezny. Checking reachability properties for Timed Automata via SAT. Technical Report 949, ICS PAS, Ordona 21, 01 - 237 Warsaw, October 2002.
• [WPZ02b] B. Woźna, W. Penczek, and A. Zbrzezny. Reachability for timed systems based on SAT-solvers. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02), volume 161(2) of Informatik-Berichte, pages 380-395. Humboldt University, 2002.
• [Yov97] S. Yovine. KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1(1/2):123—133, 1997.