Model checking of smart contracts using logic programs

Bueso de Barrio, Luis Eduardo (2020). Model checking of smart contracts using logic programs. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).

Description

Title: Model checking of smart contracts using logic programs
Author/s:
  • Bueso de Barrio, Luis Eduardo
Contributor/s:
  • Mariño Carballo, Julio
Item Type: Thesis (Master thesis)
Masters title: Métodos Formales en Ingeniería Informática
Date: 30 October 2020
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (385kB) | Preview

Abstract

The popularity of blockchain platforms has drastically increased in the past years. It seems that this trend will continue with the emergence of smart contract technologies. Smart contracts are programs stored inside the blockchain. Blockchain platforms offer means for the secure execution of procedures. These procedures cannot be modified or manipulated after being uploaded to the blockchain. Like every program they are susceptible to present bugs. Avoiding bugs in these programs is of great importance for two main reasons. First, they constantly perform money transfers so a faulty implementation can cause money losses. Second, once a contract is uploaded to the chain it cannot be modified or changed in any way. Therefor their implementation must be heavily checked before they are uploaded to the blockchain. In this master’s thesis we present a new approach of model checking of smart contracts using logic programming. To achieve this we use the theoretical framework of transition systems and Linear Temporal Logic (LTL). We use transition systems to formally define the behaviour of the smart contracts and LTL to describe properties and invariants that must be preserved during the execution of the models. From each transition system we write a Prolog program that implements its behaviour. Finally we check that the properties defined in LTL hold by asking queries to the Prolog engine.

More information

Item ID: 68768
DC Identifier: https://oa.upm.es/68768/
OAI Identifier: oai:oa.upm.es:68768
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 07 Oct 2021 12:55
Last Modified: 07 Oct 2021 12:55
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM