-
Notifications
You must be signed in to change notification settings - Fork 0
RuntimeVerification
Welcome to the Wiki section for our paper on "Runtime Verification of Cross-Organizational Smart Contracts". This paper proposes a practical approach for runtime verification of smart contracts on Hyperledger Fabric (HLF), a leading cross-organizational blockchain technology. Our research focuses on demonstrating the feasibility of applying runtime verification in consortial blockchain settings.
We introduce a model-based system engineering methodology and architecture for developing enterprise smart contracts emphasizing on reusable domain-specific data models. Our approach facilitates runtime verification using the Java Modelling Language (JML) and the OpenJML tool. We evaluate our approach on a HLF implementation of the TPC-C benchmark, demonstrating its effectiveness in detecting common software faults and its acceptable overhead.
Our HLF data mapper library called 'Hypernate' is available open source under the ftsrg/hypernate GitHub repository.
The TPC-C implementation using Hypernate and the associated artifacts and datasets are available under ftsrg/blockchain-benchmarks-tpcc repository. Our TPC-C implementation is in the form of a Hyperledger Fabric v2 chaincode, written in Java and available at smart-contract/hyperledger-fabric/v2/java, ported from the original JavaScript implementation.
We used Sparx Systems’ Enterprise Architect (EA) (version 16.1) for UML modeling and code generation.
EA provides a templating engine for model transformation and code generation for several programming languages. We significantly extended the built-in Java code templates and defined two new target languages: JavaHypernate, which generates Java classes that are, in fact, Hypernate entities, and JavaJML, which generates the JML specifications for the same classes based on the constraints defined in the model.
To generate the Hypernate entity classes, one has to select the JavaHypernate language and select the target .java file paths. To generate the JML specs, the language has to be changed to JavaJML, and another path (usually inside a specs/ subdirectory) should be selected for the .jml files.
For instructions on how to utilize Hypernate and replicate our experiments, please refer to the documentation provided HERE on how to configure Fablo test network and invoking the chaincode.
This project uses Gradle as its build system. Refer to this documentation for build instructions.