scholarly journals A Survey of Smart Contract Formal Specification and Verification

2021 ◽  
Vol 54 (7) ◽  
pp. 1-38
Author(s):  
Palina Tolmach ◽  
Yi Li ◽  
Shang-Wei Lin ◽  
Yang Liu ◽  
Zengxiang Li
Keyword(s):  
Formal Specification ◽  
Verification And Validation ◽  
Smart Contracts ◽  
Formal Models ◽  
Supply Chain Finance ◽  
Smart Contract ◽  
Formal Specification And Verification ◽  
The Common ◽  
Future Work ◽  
Industry Sectors

A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

scholarly journals Verification of HotStuff BFT Consensus Protocol With TLA+/TLC in an Industrial Setting

2021 ◽  
Vol 93 ◽  
pp. 01006
Author(s):  
Vladimir Kukharenko ◽  
Kirill Ziborov ◽  
Rafael Sadykov ◽  
Ruslan Rezin
Keyword(s):  
Formal Verification ◽  
Formal Specification ◽  
Fault Tolerant ◽  
Software Implementation ◽  
Actual Behavior ◽  
Smart Contracts ◽  
Consensus Protocol ◽  
Verification Methods ◽  
Formal Specification And Verification ◽  
Specification And Verification

The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts, which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.

scholarly journals Blockchain Smart Contract Meta-modeling

2021 ◽  
Author(s):  
Nicolás Sánchez-Gómez ◽  
Jesus Torres-Valderrama ◽  
Manuel MEJÍAS RISOTO ◽  
Alejandra GARRIDO
Keyword(s):  
Smart Contracts ◽  
Meta Model ◽  
Business Environments ◽  
Blockchain Technology ◽  
Collaborative Processes ◽  
Requirements Specifications ◽  
Smart Contract ◽  
Meta Modeling ◽  
Software Engineers ◽  
Future Work

One of the key benefits of blockchain technology is its ability to keep a permanent, unalterable record of transactions. In business environments, where companies interact with each other without a centralized authority to ensure trust between them, this has led to blockchain platforms and smart contracts being proposed as a means of implementing trustworthy collaborative processes. Software engineers must deal with them to ensure the quality of smart contracts in all phases of the smart contract lifecycle, from requirements specifications to design and deployment. This broad scope and criticality of smart contracts in business environments means that they have to be expressed in a language that is intuitive, easy-to-use, independent of the blockchain platform employed, and oriented towards software quality assurance. In this paper we present a key component: a first outline of a UML-based smart contract meta-model that would allow us to achieve these objectives. This meta-model will be enriched in future work to represent blockchain environments and automated testing.

scholarly journals Integrating formal specifications into applications: the ProB Java API

2020 ◽  
Author(s):  
Philipp Körner ◽  
Jens Bendisposto ◽  
Jannik Dunkelau ◽  
Sebastian Krings ◽  
Michael Leuschel
Keyword(s):  
Model Checking ◽  
Case Studies ◽  
Formal Specification ◽  
Formal Specifications ◽  
Formal Models ◽  
Model Checker ◽  
Enabling Technology ◽  
Code Generators ◽  
Proof Techniques ◽  
The Common

Abstract The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.

scholarly journals Supply chain finance based on smart contract

2021 ◽  
Vol 187 ◽  
pp. 12-17
Author(s):  
TianLin Zhang ◽  
JinJiang Li ◽  
XINBO JIANG
Keyword(s):  
Supply Chain ◽  
Supply Chain Finance ◽  
Smart Contract

The New Reinforcement Sensitivity Theory: Implications for Personality Measurement

2006 ◽  
Vol 10 (4) ◽  
pp. 320-335 ◽  
Author(s):  
Luke D. Smillie ◽  
Alan D. Pickering ◽  
Chris J. Jackson
Keyword(s):  
Formal Models ◽  
Personality Measurement ◽  
Reinforcement Sensitivity Theory ◽  
Sensitivity Theory ◽  
Interdependent System ◽  
Reinforcement Sensitivity ◽  
Psychometric Measures ◽  
Trait Impulsivity ◽  
Psychometric Measurement ◽  
Future Work

In this article, we review recent modifications to Jeffrey Gray's (1973, 1991) reinforcement sensitivity theory (RST), and attempt to draw implications for psychometric measurement of personality traits. First, we consider Gray and McNaughton's (2000) functional revisions to the biobehavioral systems of RST. Second, we evaluate recent clarifications relating to interdependent effects that these systems may have on behavior, in addition to or in place of separable effects (e.g., Corr, 2001; Pickering, 1997). Finally, we consider ambiguities regarding the exact trait dimension to which Gray's “reward system” corresponds. From this review, we suggest that future work is needed to distinguish psychometric measures of (a) fear from anxiety and (b) reward-reactivity from trait impulsivity. We also suggest, on the basis of interdependent system views of RST and associated exploration using formal models, that traits that are based upon RST are likely to have substantial intercorrelations. Finally, we advise that more substantive work is required to define relevant constructs and behaviors in RST before we can be confident in our psychometric measures of them.

Legally Enforceable Smart-Contract Languages

2021 ◽  
Vol 54 (5) ◽  
pp. 1-34
Author(s):  
Vimal Dwivedi ◽  
Vishwajeet Pattanaik ◽  
Vipin Deval ◽  
Abhishek Dixit ◽  
Alex Norta ◽  
...  
Keyword(s):  
Literature Review ◽  
Systematic Literature Review ◽  
State Of The Art ◽  
Grey Literature ◽  
Smart Contracts ◽  
Smart Contract ◽  
Decentralized Autonomous Organizations

Smart contracts are a key component of today’s blockchains. They are critical in controlling decentralized autonomous organizations (DAO). However, smart contracts are not yet legally binding nor enforceable; this makes it difficult for businesses to adopt the DAO paradigm. Therefore, this study reviews existing Smart Contract Languages (SCL) and identifies properties that are critical to any future SCL for drafting legally binding contracts. This is achieved by conducting a Systematic Literature Review (SLR) of white- and grey literature published between 2015 and 2019. Using the SLR methodology, 45 Selected and 28 Supporting Studies detailing 45 state-of-the-art SCLs are selected. Finally, 10 SCL properties that enable legally compliant DAOs are discovered, and specifications for developing SCLs are explored.

Sign in / Sign up

Export Citation Format

Share Document