|
|
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: |
|
