Abstraction and Verification of Properties of a Real-Time JavaReportar como inadecuado

Abstraction and Verification of Properties of a Real-Time Java - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 IRIT - Institut de recherche en informatique de Toulouse

Abstract : We present a tool for analysing resource sharing conflicts in multithreaded Java programs. Java programs are translated to timed automata models verified afterwards by the Uppaal model checker. Analysed programs are annotated with timing information indicating the execution duration of a particular statement. Based on the timing information, the analysis of execution paths is performed, which gives an answer whether resource sharing conflicts are possible in a multithreaded Java program. If the analysis succeeds, resource locks may be eliminated from the Java program.

Keywords : Timed automaton Java Multithreading Deadlock Resource sharing conflict Uppaal

Autor: Nadezhda Baklanova - Martin Strecker -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados