-
Formal Verification of Solidity contracts in Event-B
Authors:
Jian Zhu,
Kai Hu,
Mamoun Filali,
Jean-Paul Bodeveix,
Jean-Pierre Talpin
Abstract:
Smart contracts are the artifact of the blockchain that provide immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as the Ethereum. However, Solidity contracts need to adher…
▽ More
Smart contracts are the artifact of the blockchain that provide immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as the Ethereum. However, Solidity contracts need to adhere safety and security requirements that require formal verification and certification. This paper proposes a method to meet such requirements by translating Solidity contracts to Event-B models, supporting certification. To that purpose, we define a restrained Solidity subset and a transfer function which translates Solidity contracts to Event-B models. Then we take advantage of Event-B method capabilities to refine models at different levels of abstraction to verify Solidity contracts' properties. And we can verify the generated proof obligations of the Event-B model with the help of the Rodin platform.
△ Less
Submitted 13 May, 2020; v1 submitted 4 May, 2020;
originally announced May 2020.
-
An Event-B framework for the validation of Event-B refinement plugins
Authors:
Jean-Paul Bodeveix,
Mamoun Filali,
Mohamed Tahar Bhiri,
Badr Siala
Abstract:
We propose an Event-B framework for modeling the underlying theoretical foundations of Event-B. The aim of this framework is to reuse, for Event-B itself, the refinement development process. This framework introduces first, a functional kernel through an Event-B context, then, it defines Event-B projects, their static and dynamic semantics through Event-B machines. We intend to use this framework…
▽ More
We propose an Event-B framework for modeling the underlying theoretical foundations of Event-B. The aim of this framework is to reuse, for Event-B itself, the refinement development process. This framework introduces first, a functional kernel through an Event-B context, then, it defines Event-B projects, their static and dynamic semantics through Event-B machines. We intend to use this framework for the validation of Event-B plugins related to distribution and for Event-B extensions related to composition and decomposition.
△ Less
Submitted 4 January, 2017;
originally announced January 2017.
-
Real-Time Model Checking Support for AADL
Authors:
B Berthomieu,
J. -P Bodeveix,
S Dal Zilio,
M Filali,
D Le Botlan,
G Verdier,
F Vernadat
Abstract:
We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the AADL Behavioral Annex. We give a high-level view of the tools and transformations involved in the verification process and focus on the support offered by our framework for checking user-defined properties. We also desc…
▽ More
We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the AADL Behavioral Annex. We give a high-level view of the tools and transformations involved in the verification process and focus on the support offered by our framework for checking user-defined properties. We also describe the experimental results obtained on a significant avionic demonstrator, that models a network protocol in charge of data communications between an airplane and ground stations.
△ Less
Submitted 2 March, 2015;
originally announced March 2015.
