Verificación formal de un sistema distribuido, utilizando un modelo ejecutable desarrollado en C (Formal verification of distributed system using an executable C model)

Francisco Cifuentes (francisco@niclabs.cl)1, Javier Bustos Jiménez (jbustos@niclabs.cl)1, Jocelyn Simmonds (jsimmond@dcc.uchile.cl)2


1NIC Chile Research Labs
2Universidad de Chile

This paper appears in: Revista IEEE América Latina

Publication Date: June 2016
Volume: 14,   Issue: 6 
ISSN: 1548-0992


Abstract:
Formal verification means to rigorously explore the correctness of system designs expressed as mathematical models, most likely with the assistance of modern computers. Original approaches were to model and express a distributed system using existing theoretical tools such as Petri Nets. Nevertheless the main problems of such approaches are the restrictions imposed by formal tools and the human factor of simplify and model a distributed system. We propose a way to do formal verification of a distributed system by modeling the communication of the system as a concurrent program, instantiating the distributed system using threads and atomic queues and testing/verifying directly to the source code with specialized verifiers for concurrent programs. As an example, we show the verification of a distributed threshold signer using CBMC verifying properties such as memory leaks, index out of bounds, and data races.

Index Terms:
formal verification,distributed systems,concurrency,model checking,symbolic execution   


Documents that cite this document
This function is not implemented yet.


[PDF Full-Text (323)]