More flexible models using a new version of the translator of Java sources to timed automatons J2TADD

• Autorzy: Rataj A.

Warianty tytułu

PL

Bardziej elastyczne modele z użyciem nowej wersji translatora źródeł Javy do automatów czasowych J2TADD

• Języki publikacji: EN

Abstrakty

EN

Several extensions to the translator J2TADD of Java source code to timed automatons with discrete data are discussed. The changes include support for arrays, reference comparisons, abstract classes and methods, interfaces, the instanceof operator and the so–called experiments. Also, more types of statements can be interpreted.

PL

W artykule omawiane jest kilka rozszerzeń w nowej wersji translatora źródeł Javy do automatów czasowych, J2TADD. Zmiany te to między innymi możliwość używania tablic, porównań referencji, abstrakcyjnych klas i metod, interfejsów, operatora instanceof oraz porównań referencji obiektów. Możliwe jest również opisywanie tak zwanych eksperymentów. Nowa wersja J2TADD umożliwia definiowanie bardziej elastycznych modeli z użyciem bardziej klarownego kodu źródłowego.

Słowa kluczowe

EN

model checking; programming language; timed automatons; J2TADD; Uppaal; VerICS

• Wydawca: Instytut Informatyki Teoretycznej i Stosowanej Polskiej Akademii Nauk
• Czasopismo: Theoretical and Applied Informatics
• Rocznik: 2009
• Tom: Vol. 21, No. 2
• Strony: 107--114
• Opis fizyczny: Bibliogr. 8 poz., rys.

Twórcy

autor

Rataj A.

• Institute of Theoretical and Applied Informatics of the Polish Academy of Sciences, Bałtycka 5, Gliwice, Poland

Bibliografia

• 1. Behrmann G., David A., Larsen K. G.: A Tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, pages 200–236, 2004.
• 2. Hinton A., Kwiatkowska M., Norman G., Parker D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. Lecture Notes in Computer Science, 3920, pp. 441-444,2006.
• 3. Janowska A., Janowski P.: Slicing of timed automata with discrete data, Fundamenta Informaticae, vol. 72(1-3), pp. 181-195, 2006.
• 4. Kacprzak M., NabiałekW., Niewiadomski A., PenczekW., Półrola A., Szreter M.,Woźna B., Zbrzeźny A.: VerICS 2007 – a Model Checker for Knowledge and Real-Time, Fundamenta Informaticae, vol. 85(1–4), pp. 313–328, 2008.
• 5. Rataj A., Woźna B., Zberźny A.: A translator of Java programs to TADD, Concurrency, Specification and Programming (CS&P’08), Groß Väter near Berlin, Deutschland, pp. 524–535, 2008.
• 6. Rataj A., Woźna B., Zbrzeźny A.: A translator of Java programs to TADDs, Fundamenta Informaticae, vol. 93(1–3), pp. 305–324, 2009.
• 7. Woźna B., Zbrzeźny A.: Towards verification of Java programs in VerICS, Fundamenta Informaticae, vol. 85(1–4), pp. 533–548, 2008.
• 8. Zbrzeźny A., Woźna B., Orzechowski M., Raimondi F.: Towards verification of Java programs in VerICS, Concurrency, Specification and Programming (CS&P’07), pp. 580–593, Lagow, Poland 2007.