-
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.
-
Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software
Authors:
L. Besnard,
T. Gautier,
J. Ouy,
J. -P. Talpin,
J. -P. Bodeveix,
A. Cortier,
M. Pantel,
M. Strecker,
G. Garcia,
A. Rugina,
J. Buisson,
F. Dagnat
Abstract:
The SPaCIFY project, which aims at bringing advances in MDE to the satellite flight software industry, advocates a top-down approach built on a domain-specific modeling language named Synoptic. In line with previous approaches to real-time modeling such as Statecharts and Simulink, Synoptic features hierarchical decomposition of application and control modules in synchronous block diagrams and s…
▽ More
The SPaCIFY project, which aims at bringing advances in MDE to the satellite flight software industry, advocates a top-down approach built on a domain-specific modeling language named Synoptic. In line with previous approaches to real-time modeling such as Statecharts and Simulink, Synoptic features hierarchical decomposition of application and control modules in synchronous block diagrams and state machines. Its semantics is described in the polychronous model of computation, which is that of the synchronous language Signal.
△ Less
Submitted 2 March, 2010;
originally announced March 2010.
