This paper describes an approach for modeling and verification of mobile systems. Mobile systems are multi-threaded programs that are characterized by 1) the explicit notion of locations (e.g., sites where they run), 2) the ability to create and execute (possibly infinite) threads at multiple locations (e.g., sites), and 3) the capability to withstand network failures. We give formal semantics to mobile systems as Labeled Kripke Structures (LKSs), which encapsulate the notion of location and unbounded thread creation. This notation allows for the modeling of both data and communication structures of the multi-threaded systems and, thus, outperforms the traditional process algebra approach which captures only the communication behavior. We describe how mobile programs can be exhaustively analyzed by using model checking techniques. The LSKs are readily usable from within the SATABS toolset. SATABS implements the SAT-based counterexample-guided abstraction refinement framework (CEGAR for short) for ANSI-C programs, and supports verification of multi-threaded programs with unbounded thread creation. We are currently developing a front-end to SATABS that allows for languages with explicit location features, such as mobile agents. To the best of our knowledge, this is the first approach that allows modeling and verification of the full spectrum of mobile systems properties.

Modeling and verification of mobile systems / C. Braghin, N. Sharygina - In: TV'06 : multithreading in hardware and software : formal approaches to design and verification : august 21-22, 2006 : proceedings / [a cura di] Ganesh Gopalakrishnan, John O'Leary. - [s.l] : null, 2006. - pp. 28-39 (( Intervento presentato al 1. convegno Multithreading in Hardware and Software: Formal Approaches to Design and Verification (TV) tenutosi a Seattle, USA nel 2006.

Modeling and verification of mobile systems

C. Braghin;
2006

Abstract

This paper describes an approach for modeling and verification of mobile systems. Mobile systems are multi-threaded programs that are characterized by 1) the explicit notion of locations (e.g., sites where they run), 2) the ability to create and execute (possibly infinite) threads at multiple locations (e.g., sites), and 3) the capability to withstand network failures. We give formal semantics to mobile systems as Labeled Kripke Structures (LKSs), which encapsulate the notion of location and unbounded thread creation. This notation allows for the modeling of both data and communication structures of the multi-threaded systems and, thus, outperforms the traditional process algebra approach which captures only the communication behavior. We describe how mobile programs can be exhaustively analyzed by using model checking techniques. The LSKs are readily usable from within the SATABS toolset. SATABS implements the SAT-based counterexample-guided abstraction refinement framework (CEGAR for short) for ANSI-C programs, and supports verification of multi-threaded programs with unbounded thread creation. We are currently developing a front-end to SATABS that allows for languages with explicit location features, such as mobile agents. To the best of our knowledge, this is the first approach that allows modeling and verification of the full spectrum of mobile systems properties.
2006
Microsoft, Cadence, IBM, Nec, Intel
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/26968
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact