Abstract
The increasing use of advanced smart contract structures in finance necessitates rigor and scalability in ensuring their correctness. Traditional auditing methods fall short in providing comprehensive security, but formal verification offers a robust and scalable approach to constructing secure-by-design models and implementing smart contracts. In this paper, we introduce a B-method framework for modeling and verifying smart contracts based on the ACTUS standard for financial instruments. We start by converting ACTUS specifications into B-method constructs to bring a systematic approach to model, analyze, and verify financial contracts’ implementations within the blockchain context.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Boudi, Z., Collart-Dutilleul, S., et al.: Safety critical software construction using CPN modeling and b method’s proof. In: SESA 2014, Software Engineering and Systems Architecture, p. 4p (2014)
Brammertz, W., Mendelowitz, A.I.: From digital currencies to digital finance: the case for a smart financial contract standard. J. Risk Finance 19(1), 76–92 (2018)
Britsiani, N.: Smart contracts: Legal aspects (2022). https://repository.ihu.edu.gr//xmlui/handle/11544/30033. Accepted 2022-09-30T08:47:30Z
Buchs, D., Klikovits, S., Linard, A.: Petri Nets: A Formal Language to Specify and Verify Concurrent Non-Deterministic Event Systems. Foundations of Multi-Paradigm Modelling for Cyber-Physical Systems, pp. 177–208 (2020)
Buchs, D., Klikovits, S., Linard, A.: Petri Nets: a formal language to specify and verify concurrent non-deterministic event systems. In: Foundations of Multi-Paradigm Modelling for Cyber-Physical Systems, pp. 177–208. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-43946-0_7
Clack, C.D.: Design discussion on the ISDA common domain model. J. Digital Banking 3(2), 165–187 (2018)
Colin, S., Mariano, G.: Coq, l’alpha et l’omega de la preuve pour B? (2009)
Cornelius, K.B.: Smart contracts as evidence: trust, records, and the future of decentralized transactions. In: Hunsinger, J., Allen, M.M., Klastrup, L. (eds.) Second International Handbook of Internet Research, pp. 627–646. Springer, Dordrecht (2020). https://doi.org/10.1007/978-94-024-1555-1_28
FeverTokens: FeverTokens’ open-source Package-Oriented Framework (2023). https://github.com/FeverTokens/ft-package-oriented-framework. Accessed Dec 2023
Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, 109–125 (2016)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Springer Science & Business Media (1996). https://doi.org/10.1007/978-3-662-03241-1
Khan, S.N., Loukil, F., Ghedira-Guegan, C., Benkhelifa, E., Bani-Hani, A.: Blockchain smart contracts: applications, challenges, and future trends. Peer-to-peer Netw. Appl. 14, 2901–2925 (2021)
Lahbib, A., Ait Wakrime, A., Laouiti, A., Toumi, K., Martin, S.: An event-B based approach for formal modelling and verification of smart contracts. In: Barolli, L., Amato, F., Moscato, F., Enokido, T., Takizawa, M. (eds.) AINA 2020. AISC, vol. 1151, pp. 1303–1318. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44041-1_111
Treharne, H., Schneider, S.: How to drive a b machine. In: ZB 2000: Formal Specification and Development in Z and B: First International Conference of B and Z Users York, UK, August 29–September 2, 2000 Proceedings 1. pp. 188–208. Springer (2000)
Van Vulpen, P., Heijnen, H., Kroon, T., Mens, S., Jansen, S.: Decentralized Autonomous Organization Governance By Upgradeable Diamond Smart Contracts. SSRN 4634762 (2023)
Zou, W., et al.: Smart contract development: challenges and opportunities. IEEE Trans. Software Eng. 47(10), 2084–2106 (2019)
Acknowledgments
This research was supported by funding from the Casper Association and Bpifrance. We acknowledge their contributions, which have facilitated the foundational aspects of our study and set the stage for future developments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Boudi, Z., Mohamed, T. (2024). Towards a B-Method Framework for Smart Contract Verification: The Case of ACTUS Financial Contracts. In: Ait Wakrime, A., Navarro-Arribas, G., Cuppens, F., Cuppens, N., Benaini, R. (eds) Risks and Security of Internet and Systems. CRiSIS 2023. Lecture Notes in Computer Science, vol 14529. Springer, Cham. https://doi.org/10.1007/978-3-031-61231-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-61231-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-61230-5
Online ISBN: 978-3-031-61231-2
eBook Packages: Computer ScienceComputer Science (R0)