The smart contract technology has increasingly attracted the attention of different industries. However, a significant number of smart contracts deployed in practice suffer from several bugs, which enable malicious users to cause damage. The research community has shifted their focus to verifying the correctness of smart contracts using model checkers and formal verification methods. The majority of the research investigates the correctness of systems built on one smart contract. This paper proposes a verification approach for systems composed of interacting smart contracts developed and controlled by different entities. We use the NuSMV model checker and the Behavioral Interaction Priority tool to model the behaviors of smart contracts and their interactions with the aim of verifying their compliance with the systems' functional requirements. These requirements are formalized by Linear Temporal Logic propositions. The applicability of our approach is illustrated using a case study from The American Petroleum Institute and implemented using Hyperledger Fabric.

Pipeline control systems often incorporate thousands of widely dispersed sensors and actuators, many of them in remote locations. Information about the operational aspects (functionality) and integrity (state) of these field devices is critical because they perform vital measurement and control functions. This paper describes a distributed scanner for remotely verifying the functionality and state of field devices in Modbus networks. The scanner is designed for the Modbus protocol and, therefore, accommodates the delicate TCP/IP stacks of field devices. Furthermore, field device scanning and data storage and retrieval operations are scheduled so as not to impact normal pipeline control operations. Experimental results and simulations demonstrate that the distributed scanner is scalable, distributable and operates satisfactorily in low bandwidth networks.