Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce theVeriSolidframework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction.VeriSolidallows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (calleddeployment diagrams) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability ofVeriSolid, we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by usingVeriSolid. We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.

Summary The design of software for networked systems with nodes running an Internet of things operating system faces important challenges due to the heterogeneity of interacting things and the constraints stemming from the often limited amount of available resources. In this context, it is hard to build confidence that a design solution fulfills the application's requirements. This paper introduces a design flow for web service applications of the representational state transfer style that is based on a formal modeling language, the behaviour, interaction, priority (BIP) component framework. The proposed flow applies the principles of separation of concerns in a component‐based design process that supports the modular design and reuse of model artifacts. The BIP tools for state‐space exploration allow verifying qualitative properties for service responsiveness, ie, the timely handling of events. Moreover, essential quantitative properties are validated through statistical model checking of a stochastic BIP model. All properties are preserved in actual implementation by ensuring that the deployed code is consistent with the validated model. We illustrate the design of a representational state transfer sense‐compute‐control application for a Wireless Personal Area Network architecture with nodes running the Contiki operating system. The results validate qualitative and quantitative properties for the system and include the study of error behaviours.

The focus of this work is the on-demand resource provisioning in cloud computing, which is commonly referredto as cloud elasticity. Although a lot of effort has been invested in developing systems and mechanisms that enable elasticity, the elasticity decision policies tend to be designed without quantifying or guaranteeing the quality of their operation. We present an approach towards the development of more formalized and dependable elasticity policies. We make two distinct contributions. First, we propose an extensible approach to enforcing elasticity through the dynamic instantiation and online quantitative verification of Markov Decision Processes(MDP) using probabilistic model checking. Second, various concrete elasticity models and elasticity policies are studied. We evaluate the decision policies using traces from a realNoSQL database cluster under constantly evolving externalload. We reason about the behaviour of different modelling and elasticity policy options and we show that our proposal can improve upon the state-of-the-art in significantly decreasing under-provisioning while avoiding over-provisioning.

Behavioral correctness of service compositions refers to the absence of service interaction flaws, so that essential service properties like deadlock freedom are preserved and correctness properties related to safety and liveness are assured. Model checking is a widespread technique and it is based on extracting an abstract model representation of the program defining a service orchestration or choreography. During model extraction, the original structure of the service composition cannot be preserved and backwards traceability of the verification findings is not possible. We propose a rigorous analysis within the BIP component framework. Being rigorous means that the analyst is able to reason on which properties hold and why. The BIP language offers a sound execution semantics for a minimal set of primitives and constructs for modeling and composing layered components. We formally define the WS-BPEL 2.0 execution semantics and we provide a structure-preserving translation (embedding) of WS-BPEL to BIP. Structure preservation is feasible, due to the formally grounded expressiveness properties of BIP. As a proof of concept, we apply the developed embedding to a sample BPEL program and present the analysis results for a safety property. By exploiting the BIP model structure we interpret the analysis findings in terms of the service interactions stated in the BPEL source code. A significant benefit of BIP is that it applies compositional reasoning on the model structure to guarantee essential correctness properties and avoid, as much as possible, the scalability limitations of conventional model checking.

Getting an overview of a large online social net-work and deciding which communities to join is a challenging task for a new user. We propose a method that maps a large network into a smaller graph with two kinds of nodes: a node of the first kind is representative of a community, a node of the second kind is neighbor to a representative and rejects the semantics of that community. Our approach encompasses a learning and ranking algorithm that derives this smaller graph from the original one, and a visualization algorithm that returns a graph layout to the observer. We report on our results on inspecting the network of a folksonomy.