Insurance claims processing involves multi-domain entities and multi-source data, along with a number of human-agent interactions. Use of Blockchain technology-based platform can significantly improve scalability and response time for processing of claims which are otherwise manually-intensive and time-consuming. However, the chaincodes involved within the processes that issue claims, approve or deny them as required, need to be formally verified to ensure secure and reliable processing of transactions in Blockchain. In this paper, we use a formal modeling approach to verify various processes and their underlying chaincodes relating to different stages in insurance claims processing viz., issuance, approval, denial, and flagging for fraud investigation by using linear temporal logic (LTL). We simulate the formalism on the chaincodes and analyze the breach of chaincodes via model checking.

翻译：保险理赔涉及多领域实体与多源数据，同时包含大量人机交互。基于区块链技术的平台能显著提升理赔处理的可扩展性和响应速度——传统理赔流程高度依赖人工且耗时巨大。然而，业务过程中用于发起、批准或拒绝理赔的链码（chaincode），必须经过形式化验证以确保区块链交易处理的安全性与可靠性。本文采用形式化建模方法，通过线性时序逻辑（LTL）对理赔处理各阶段（发起、批准、拒绝及欺诈调查标记）的相关流程及底层链码进行验证。我们基于链码对形式化模型进行仿真，并通过模型检验分析链码的违规行为。