Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Intermediate Language

Sortuj według:

Ogranicz wyniki do:

Translation of Intermediate Language to Timed Automata with Discrete Data

Janowska A., Janowski P., Wróblewski D.

Fundamenta Informaticae

2008

Vol. 85, nr 1-4

235-248

The aim of this work is to describe the translation from Intermediate Language, one of the input formalisms of the model checking platform VerICS, to timed automata with discrete data and to compare it with the translation to classical timed automata. The paper presents syntax and semantics of both formalisms, the translation rules as well as a simple example.

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.