Formal Verification of Distributed System Using an Executable C Model
Artículo

Open/ Download
Access note
Acceso a solo metadatos
Publication date
2016Metadata
Show full item record
Cómo citar
Cifuentes, F.
Cómo citar
Formal Verification of Distributed System Using an Executable C Model
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.
Indexation
Artículo de publicación ISI
Quote Item
IEEE Latin America Transactions. Volumen: 14 Número: 6 Páginas: 2874-2878 Número especial: SI
Collections