Blockchain-based applications are basically built on smart contracts, which are widely different in regards of the encoded logic and the used standards. When talking about Ethereum standards, ERC-721 is a well-known standard interface developed for Non-Fungible Tokens. Even though it is standard-based contracts that are more and more exploited, prior work on smart contracts verification mostly investigates efforts in regards of specific vulnerabilities. To address this gap, this paper introduces a formal modeling and verification approach for Ethereum smart contracts including the standard-based ones. We propose a model checking framework that, according to a Solidity smart contract provided as an input, uses ERC guidelines as a standard template to extract the related security properties. Another added benefit of our proposal consists on modeling ERC contracts using the extended finite state machine formalism. As a proof of concept, we illustrate our model checking approach through an NFT contract.

Focusing on important features in blockchain applications, smart contracts are one of the most studied in the literature. Despite the trusted implementations that smart contracts offer, different security problems and vulnerabilities are rising during their development and execution. Trying to deal with such issues, different researches are proposed to give eventual solutions. Such studies focus on the verification of smart contracts and adopt different techniques. While various formal methods are considered significant effective to ensure the trustworthiness and correctness of smart contracts, this work deals with formal verification of smart contracts using model checking. In this survey, we conduct an overview on smart contracts verification using model checking. We analyze and classify each study according to four main aspects; the adopted formalism, the verified properties, the system under verification and to which blockchain platform the contribution is dedicated. Finally, we suggest some promising future directions to stir research efforts into this area.

Current communication systems restrict user affordances in terms of expressiveness and interaction. Complex Event Processing (CEP) have gained much importance to overcome these shortcomings. It allows users to interact with powerful expressiveness when defining logical and temporal patterns of exchanged events. This expressiveness allows cleaning network traffic by eliminating the routing of useless events and consequently reducing the overall consumed energy. However, handling the expressiveness of desired events, filtering coming events still challenging features, especially with the growth of data size encapsulated as events in the network. In this work, we rely on Publish/Subscribe system based on Distributed Hash Tables (DHT), which offers intrinsically flexible event routing, scalability and load balancing in order to manage distributed composite events routing. For efficient event filtering, we propose a three dimensional indexing hash space named CECube as a smart data structure for rapid CEP over DHT. The CECube indexes firstly composite subscriptions, then basing on a simple binary search, it serves as publications filter and helps making the right decision for what events should be aggregated and forwarded to the adequate subscribers. The performance of our solution is evaluated using Free Pastry simulator. The results demonstrate firstly that our approach is efficient in terms of filtering process and that the average number of routing nodes is decreased. Secondly, we prove the superiority of our approach as compared to another existing work.

Opportunistic real time mobile crowdsensing pertains to the instantaneous monitoring of large scale phenomena by leveraging human mobility and smartphones' sensors. However, while urban applications concern more about coverage quality and timeliness of detected data, mobile users should care about their consumed energy for performing a sensing task. In this paper, we introduce the Real time OPportunistic Scheduler Framework for Energy aware mobile Crowdsensing (Re-OPSEC). Especially, we present in deep the off-line tasks allocation approach operating on top of energy saving model. The methodology consists of two main processes. Re-OPSEC builds firstly connectivity patterns called online episodes and extracts mobility information jointly with those patterns. Secondly, it allocates, in an off-line mode, online episodes to send jointly sensing tasks in real time. Allocated patterns should increase the total expected sensing revenue and protect volunteers from embarassed situations such as their smartphones turning off. The performance of the approach is evaluated using realistic mobility datasets. The results demonstrate firstly the superiority of our approach as compared to an other existing work. Secondly, they prove that coverage rate can achieve a high level in spite of energy saving mechanisms restriction.

In professional or home settings, the usage of Machine-to-Machine (M2M) technology is desired and often enforced for its ability to reduce the total cost and to expose ubiquitous networks services. However, due to the unpredictability of M2M network mobility, connection and disconnection, a lot of problems can attend services availability and cause path loss or change service selection parameters, making services discovery more difficult than ever. In this paper, we present an approach based on knowledge for ensuring discovery and invocation of available services. The approach firstly leverages semantic data from user regularity of movement by extracting knowledge jointly from the mobility data and underlying geographic domain information. Then, it analyzes those data in order to prepare a pre-planned list of available services ranked not only according to their relevance but also according to their degree of availability. To illustrate the feasibility of our approach, we adopt an illustrative scenario highlighting the importance of exploiting the daily life of a mobile user for service discovery enhancements.