Towards modelling and verification of mobile agent systems

International audienceThe aim of this case study is to show the feasibility of the translation from a description of a system based on mobile agents to a prototype satisfying suitable properties. We address here the behavioural part of mobile agents by expressing them using a process algebra including mobility. This description allows to obtain formal semantics which may be automatically analysed thanks to model-checking or simulation techniques