ecms_neu_mini.png

Digital Library

of the European Council for Modelling and Simulation

 

Title:

Modelling And Verification Of Concurrent Programs Using UPPAAL

Authors:

Franco Cicirelli, Libero Nigro, Francesco Pupo

Published in:

 

(2011).ECMS 2011 Proceedings edited by: T. Burczynski, J. Kolodziej, A. Byrski, M. Carvalho. European Council for Modeling and Simulation. doi:10.7148/2011 

 

ISBN: 978-0-9564944-2-9

 

25th European Conference on Modelling and Simulation,

Jubilee Conference

Krakow, June 7-10, 2011

 

Citation format:

Cicirelli, F., Nigro, L., & Pupo, F. (2011). Modelling And Verification Of Concurrent Programs Using Uppaal. ECMS 2011 Proceedings edited by: T. Burczynski, J. Kolodziej, A. Byrski, M. Carvalho (pp. 525-533). European Council for Modeling and Simulation. doi:10.7148/2011-0525-0533

DOI:

http://dx.doi.org/10.7148/2011-0525-0533

Abstract:

This paper describes the design and implementation of a library of reusable UPPAAL template processes which support reasoning and property checking of concurrent programs, e.g. to be realized in the Java programming language. The stimulus to the development of the library originated in the context of a systems programming undergraduate course. The library, though, can be of help to general practitioners of concurrent programming   which  nowadays        are challenged to exploiting the potentials of modern multi- core architectures. The paper describes the library and demonstrates its usage to modelling and exhaustive verification of mutual exclusion and common concurrent structures and synchronizers. UPPAAL was chosen because it is a popular and continually improved toolbox based on timed automata and model checking and it is provided of a user-friendly graphical interface which proves very important for debugging and property assessment of concurrent models. Java was considered as target implementation language because of its diffusion among application developers.

Full text: