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}
^{1}NIC Chile Research Labs ^{2}Universidad de Chile
This paper appears in: Revista IEEE América Latina
Publication Date: June 2016
Volume: 14, Issue: 6
ISSN: 15480992
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 FullText (323)]
