Using Formal Languages to Elicit Requirements for Healthcare Blockchain Applications

  • Bella Pavita
  • Vinitha Hannah SubburajEmail author
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 1069)


Specifying requirements for complex systems has an important role during software development. At times, the importance of the specification stage gets neglected by software engineers while developing software systems. Software engineering life cycle models are improved for better software quality and reliability. Even though powerful implementation strategies exist, if the requirements of a system to be developed are unclear and not specified properly, then the product can fail to satisfy user needs. Traditional methods use natural language for specifying the requirements of the software systems. The use of formal specifications to specify software systems remains a challenging research problem that needs to be addressed. In this research effort, several healthcare applications that are implemented using Blockchain are studied. Blockchain is a recent invention that uses the idea of decentralization to enforce security. Such applications come with complexity and specifying requirements for such systems using formal specification languages gets even more challenging. The challenges involved in writing formal specifications for such complex applications has been studied in this research effort. The Descartes specification language, a formal executable formal specification language, is used to specify the blockchain healthcare applications under study. Case study examples are used to illustrate the specification of Blockchain healthcare application requirements using the Descartes specification language.


Blockchain applications Security Formal specifications 


  1. 1.
    Manyika, J., Chui, M., Brown, B., Bughin, J., Dobbs, R., Roxburgh, C., Byers, A.H.: Big data: the next frontier for innovation, competition, and productivity (2011)Google Scholar
  2. 2.
    Iansiti, M., Lakhani, K.R.: The truth about blockchain. Harvard Bus. Rev. 95(1), 118–127 (2017)Google Scholar
  3. 3.
    Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Lüttgen, G.: Using formal specifications to support testing. ACM Comput. Surv. (CSUR) 41(2), 9 (2009)CrossRefGoogle Scholar
  4. 4.
    Pandey, Tulika, Srivastava, Saurabh: Comparative analysis of formal specification languages Z, VDM and B. Int. J. Current Eng. Technol. 5(3), 2086–2091 (2015)Google Scholar
  5. 5.
    Subburaj, V.H., Urban, J.E.: Formal specification language and agent applications. In: Intelligent Agents in Data-intensive Computing, pp. 99–122. Springer, Cham (2016). Scholar
  6. 6.
    Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-Béguelin, S.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91–96. ACM, October 2016Google Scholar
  7. 7.
    Abdellatif, T., Brousmiche, K.L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1–5. IEEE, February 2018Google Scholar
  8. 8.
    Singh, I., Lee, S.W.: Comparative requirements analysis for the feasibility of blockchain for secure cloud. In: Asia Pacific Requirements Engineering Conference, pp. 57–72. Springer, Singapore, November 2017Google Scholar
  9. 9.
    Ekblaw, A., Azaria, A., Halamka, J.D., Lippman, A.: A case study for blockchain in healthcare: “MedRec” prototype for electronic health records and medical research data. In: Proceedings of IEEE Open & Big Data Conference, vol. 13, p. 13, August 2016Google Scholar
  10. 10.
    Eid, M.: Requirement Gathering Methods (2015)Google Scholar
  11. 11.
    Etherscan Homepage.
  12. 12.
    Kasampalis, T., Guth, D., Moore, B., Serbănută, T., Serbănută, V., Filaretti, D., Rosu, G., Johnson, R.: IELE: an intermediate-level blockchain language designed and implemented using formal semantics, pp. 1–25 (2018)Google Scholar
  13. 13.
    Leiding, B., Norta, A.: Mapping requirements specifications into a formalized blockchain-enabled authentication protocol for secured personal identity assurance. In: Dang, T.K., Wagner, R., Kung, J., Thoai, N., Takizawa, M., Neuhold, E.J. (eds.) Future Data and Security Engineering, pp. 181–196. Springer International Publishing (2017)Google Scholar
  14. 14.
    Urban, J.E.: A Specification Language and its Processor, Ph.D. Dissertation, Computer Science Department, University of Southwestern Louisiana, pp. 35–59 (1977)Google Scholar
  15. 15.
    Subburaj, V.H., Urban, J.E.: A formal specification language for modeling agent systems. In: 2013 Second International Conference on Informatics & Applications (ICIA), Lodz, pp. 300–305 (2013).
  16. 16.
    Subburaj, V.H., Urban, J.E.: Specifying security requirements in multi-agent systems using the descartes-agent specification language and AUML. In: Information Technology for Management: Emerging Research and Applications, pp. 93–111. Springer, Cham (2018)Google Scholar
  17. 17.
    Brouwer, W.D., Borda, M.: NeuRoN: decentralized artificial intelligence, distributing deep learning to the edge of the network, pp. 1–17 (2017)Google Scholar
  18. 18.
    Grishin, D., Obbad, K., Estep, P., Cifric, M., Zhao, Y., Church, G.: Nebula genomics: blockchain-enabled genomic data sharing and analysis platform, pp. 1–28 (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.School of Engineering, Computer Science and MathematicsWTAMUCanyonUSA
  2. 2.West Texas A&M UniversityCanyonUSA

Personalised recommendations