Towards Verification of Java Programs in perICS

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Zbrzezny, Andrzej | Woźna, Bożena

Affiliations: IMCS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland. a.zbrzezny@ajd.czest.pl, b.wozna@ajd.czest.pl

Note: [] Address for correspondence: IMCS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland

Abstract: VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java.

Journal: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 533-548, 2008