Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: VerICS

Sortuj według:

Ogranicz wyniki do:

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

Rataj A.

Theoretical and Applied Informatics

2009

Vol. 21, No. 2

107-114

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.

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.

UML Verification with Verics

Niewiadomski A., Penczek W.

Studia Informatica : systems and information technology

2007

Vol. 1(8)

19--31

We show how to verify UML specifications against properties expressed by CTL-like formulas using the symbolic model checker Verics. Our method is illustrated with an example showing a verification of Alternating Bit Protocol.

Towards verification of Java programs in VerICS

Orzechowski M., Woźna B., Siwiak T.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2006

Nr 997

1-33

VerICS has been designed as a tool for automated verification of timed automata, and protocols written in both Intermediate Language and a specification language Estelle. Recently, the tool has been extended to work with so called Timed Automata with Discrete Data and multi-agent systems. The paper presents a prototype of a translator from a subset of the Java programming language to Intermediate Language and Time Automata with Discrete Data, the modeling languages of the VerICS model checker.

Verics został zaprojektowany jako narzędzie do automatycznej weryfikacji automatów czasowych oraz protokołów zapisanych zarówno w języku pośrednim jaki i języku Estelle. Ostatnimi czasy Verics został rozbudowany i obecnie pozwala również na automatyczną weryfikację systemów wieloagentowych oraz protokołów zapisanych za pomocą formalizmu rozszerzonych automatów czasowych. Praca ta opisuje translator z pewnego podzbioru Javy, popularnego ostatnio języka programistycznego, do rozszerzonych automatów czasowych i do języka pośredniego, formalizmów będących językami wejściowymi dla werifikatora Verics.