Julio Mariño, Researcher, BABEL, UPM
“Shared resources” is the term we use to refer to the notation and companion methodology used to teach concurrent programming at undergraduate level in our university for the last 15 years.
Originally conceived as a gentle extension of a formal notation for teaching abstract data types – just adding the extra synchronization component – they have recently proved useful out of the classroom to model and analyze complex, real world systems.
From the point of view of software design, shared resources can be used to fill a gap in widely used modeling notations regarding concurrency. At the code level, they have been used for semi-automatic generation of correct-by-construction code. Finally, wrt. analysis and validation, they can be seen as automata generators.
The talk will introduce the formalism from the different points of view mentioned above, and will present current and future research lines. If time permits, the talk will include a short demo on the use of shared resources and model checking for validation of concurrency requirements.
This is joint work with Manuel Carro, Angel Herranz and Juanjo Moreno-Navarro.