Automatic timeliness verification of a public mobile network

Ester Ciancamerla, Michele Minichino, Stefano Serro, Enrico Tronci

Research output: Contribution to journalArticle

3 Citations (Scopus)


This paper deals with the automatic verification of the timeliness of Public Mobile Network (PMN), consisting of Mobile Nodes (MNs) and Base Stations (BSs). We use the Murphi Model Checker to verify that the waiting access time of each MN, under different PMN configurations and loads, and different inter arrival times of MNs in a BS cell, is always below a preassigned threshold. Our experimental results show that Model Checking can be successfully used to generate worst case scenarios and nicely complements probabilistic methods and simulation which are typically used for performance evaluation. © Springer-Verlag Berlin Heidelberg 2003.
Original languageEnglish
Pages (from-to)35 - 48
Number of pages14
JournalLecture Notes in Computer Science
Publication statusPublished - 2003


All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this