Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Ristori G. Model checking a mobile telephone system. In: ERCIM - Second International Ercim Workshop on Formal Methods for Industrial Critical System (Cesena, 4-5 July 1997). Proceedings, pp. 113 - 123. S. Gnesi, D. Latella (eds.). ERCIM, 1997.
In this paper we present a logic verification environment for mobile system specified by p-calculus terms. Properties of mobile system espressed by using an action-based temporal logic. Exploting a feature of the environment, we can generate finite state automata for a wide class of p-calculus agents, by preserving a notion of bisimulation equivalence. Hence, the formulae can be verified by applying a classical model check-in approach. In particular, we present as casa study, the verification of some propeties of a GSM protocol for mobile telephones, specified using a p-calculus.
Subject Mobile telephone system

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional