Translation of Timed Promela to Timed Automata with Discrete Data

• Autorzy: Nabiałek W. , Janowska A. , Janowski P.
• Języki publikacji: EN

Abstrakty

EN

The aim of the work is twofold. In order to face the problem of modeling time constraints in Promela, a timed extension of the language is presented. Next, timed Promela is translated to timed automata with discrete data, that is timed automata extended with integer variables. The translation enables verification of Promela specifications via tools accepting timed automata as input, such as VerICS or Uppaal. The translation is illustrated with a well known example of Fischer's mutual exclusion protocol. Some experimental results are also presented.

Słowa kluczowe

EN

promela; spin; Timed Automata; timed systems; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 409--424
• Opis fizyczny: bibliogr. 12 poz., tab., wykr.

Twórcy

autor

Nabiałek W.

autor

Janowska A.

autor

Janowski P.

• Institut of Computer Science, University of Podlasie ul. Sienkiewicza 51, 08-110 Siedlce, Poland,

Bibliografia

• [1] 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 Computer Society, 1992.
• [2] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the 17th Int. Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [3] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998.
• [4] D. Bosnacki and D. Dams. Discrete-time Promela and Spin. In FTRTFT '98: Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 307-310. Springer-Verlag, 1998.
• [5] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia,M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NUSMV2: An open-source tool for symbolic model checking. In Proc. of the 14th Int. Conf. on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 359-364. Springer-Verlag, 2002.
• [6] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, volume 1066 of LNCS, pages 208-219. Springer-Verlag, 1995.
• [7] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, 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.
• [8] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110-122, 1997.
• [9] G. J. Holzmann. SPIN Model Checker, The: Primer and Reference Manual. AddisonWesley, 2003.
• [10] A. Janowska and P. Janowski. Slicing timed automata with discrete data. Fundamenta Informaticae, 72(1-3):181-195, 2006.
• [11] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [12] S. Tripakis and C. Courcoubetis. Extending Promela and SPIN for real time. In Proc. of the 2nd Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of LNCS, pages 329-348. Springer-Verlag, 1996.