Abstract
The emergence of Distributed Ledger Technologies and Cryptocurrencies impacts on how transactions of various assets between parties in highly dynamical settings – such as the Internet of Things or Smart Cities – are modelled and implemented in several ways. We study this transition from centralized accounts with explicit owners towards distributed ledgers with challenge-based transaction access control. We capture the transition in a series of linked formal specifications in Z, enabling the comparison between the two settings. In particular, we provide a reference model and then refine it for the respective settings.
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
Notes
- 1.
We remark that the preconditions and postconditions of a transaction are not to be confused with the preconditions and postconditions of a Z schema. Identifying the set \(pre\) with \(pre\_ Transaction\) would require to know the preconditions at specification.
- 2.
Technically, we can imagine preconditions referencing postconditions which are not stored in the distributed ledger. We assume such ‘external’ preconditions to be stored in the data part of the transaction.
- 3.
This is well-defined because every n-ary partial function
can be conceived as the set of all tuples \((a_1,\dots ,a_n,f(a))\) with \(a_i\in A_i\) for each \(1\le i\le n\). - 4.
In Blockchain-jargon, these transactions are part of the ‘genesis block’.
can be conceived as the set of all tuples References
Abrial, J., Schuman, S.A., Meyer, B.: Specification language. In: McKeag, R.M., Macnaughlen, A.M. (eds.) On the Construction of Programs, pp. 343–410. Cambridge University Press, Cambridge (1980)
Androulaki, E., et al.: Hyperledger fabric: a distributed operating system for permissioned blockchains. In: Proceedings of the Thirteenth EuroSys Conference, EuroSys 2018, pp. 30:1–30:15. ACM, New York (2018). https://doi.org/10.1145/3190508.3190538, http://doi.acm.org/10.1145/3190508.3190538
Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. IACR Cryptology ePrint Archive 2017, 1124 (2017). http://eprint.iacr.org/2017/1124
Bonneau, J., Miller, A., Clark, J., Narayanan, A., Kroll, J.A., Felten, E.W.: SoK: research perspectives and challenges for Bitcoin and cryptocurrencies. In: IEEE Symposium on Security and Privacy, pp. 104–121. IEEE Computer Society (2015)
Bures, T., Plasil, F., Kit, M., Tuma, P., Hoch, N.: Software abstractions for component interaction in the Internet of Things. Computer 49(12), 50–59 (2016). https://doi.org/10.1109/MC.2016.377
Cachin, C., Caro, A.D., Moreno-Sanchez, P., Tackmann, B., Vukolic, M.: The transaction graph for modeling blockchain semantics. IACR Cryptology ePrint Archive 2017, 1070 (2017). http://eprint.iacr.org/2017/1070
Easley, D.A., Kleinberg, J.M.: Networks, Crowds, and Markets - Reasoning About a Highly Connected World. Cambridge University Press, Cambridge (2010). http://www.cambridge.org/gb/knowledge/isbn/item2705443/?site_locale=en_GB
Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof systems. SIAM J. Comput. 18(1), 186–208 (1989)
Lindman, J., Tuunainen, V.K., Rossi, M.: Opportunities and risks of blockchain technologies-a research agenda. In: Proceedings of the 50th Hawaii International Conference on System Sciences (2017)
Mainelli, M., Smith, M.: Sharing ledgers for sharing economies: an exploration of mutual distributed ledgers (aka blockchain technology). J. Financ. Perspect. 3(3), 38–58 (2015)
Marc, P.: Blockchain technology: principles and applications. In: Xavier Olleros, F., Zhegu, M. (eds.) Handbook of Research on Digital Transformations. Edward Elgar, Cheltenham (2016)
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). http://bitcoin.org/bitcoin.pdf
Spivey, J.M.: The Z Notation - A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)
Swanson, T.: Consensus-as-a-service: a brief report on the emergence of permissioned, distributed ledger systems (2015)
Tschorsch, F., Scheuermann, B.: Bitcoin and beyond: a technical survey ondecentralized digital currencies. IEEE Commun. Surv. Tutor. 18(3), 2084–2123 (2016). https://doi.org/10.1109/COMST.2016.2535718
Walport, M.: Distributed ledger technology: beyond block chain (2016)
Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.): Software Engineering for Collective Autonomic Systems - The ASCENS Approach. LNCS, vol. 8998. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2018). https://ethereum.github.io/yellowpaper/paper.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Sürmeli, J., Jähnichen, S., Sanders, J.W. (2018). Modelling the Transition to Distributed Ledgers. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018. Lecture Notes in Computer Science(), vol 11246. Springer, Cham. https://doi.org/10.1007/978-3-030-03424-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-03424-5_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03423-8
Online ISBN: 978-3-030-03424-5
eBook Packages: Computer ScienceComputer Science (R0)