The radically increasing amount and enormous types of data generated by vehicles have brought in the innovated application of data trading in the Internet of Vehicles (IoV). However, the trustless environment in IoV enabled data trading faces conflicting interests and disputes of trading parties. To build trust, we exploit consortium blockchain for secure data trading with information transparency. In addition, a hash list of traded data is maintained by roadside units accompanied by bloom filters for fast lookup, to avoid data duplication. The reliability and integrity of trading data are ensured by using the digital signature scheme based on elliptic curve bilinear pairing. For long term availability of traded data, an external distributed storage, i.e., InterPlanetary File System (IPFS) can provide reliable, high capacity storage resources. The experimental results verified that our proposed solution is efficient for data trading in IoV and reliable for long term availability of data storage.

The existing concurrency model for Java (or C) requires programmers to design and implement thread-safe classes by explicitly acquiring locks and releasing locks. Such a model is error-prone and is the reason for many concurrency bugs. While there are alternative models like transactional memory, manually writing locks remains prevalent in practice. In this work, we propose AutoLock, which aims to solve the problem by fully automatically generating thread-safe classes. Given a class which is assumed to be correct with sequential clients, AutoLock automatically generates a thread-safe class which is linearizable, and does it in a way without requiring a specification of the class. AutoLock takes three steps: (1) infer access annotations (i.e., abstract information on how variables are accessed and aliased), (2) synthesize a locking policy based on the access annotations, and (3) consistently implement the locking policy. AutoLock has been evaluated on a set of benchmark programs and the results show that AutoLock generates thread-safe classes effectively and could have prevented existing concurrency bugs.

This paper presents Sip4J, a fully automated, scalable and effective tool to automatically generate access permission contracts for a sequential Java program. The access permission contracts, which represent the dependency of code blocks, have been frequently used to enable concurrent execution of sequential programs. Those permission contracts, unfortunately, need to be manually created by programmers, which is known to be time-consuming, laborious and error-prone. To mitigate those manual efforts, Sip4J performs inter-procedural static analysis of Java source code to automatically extract the implicit dependencies in the program and subsequently leverages them to automatically generate access permission contracts, following the Design by Contract principle. The inferred specifications are then used to identify the concurrent (immutable) methods in the program. Experimental results further show that Sip4J is useful and effective towards generating access permission contracts for sequential Java programs. The implementation of Sip4J has been published as an open-sourced project at https://github.com/Sip4J/Sip4J and a demo video of Sip4J can be found at https://youtu.be/RjMTIxlhHTg.

The research work in this paper discusses an improved Petri net model of railway crossing regions which are important and critical components of a railway networks. A control algorithm has been developed showing the interaction of the controller to other component of the system. A formal approach viz. Petri net (PN) is applied to model the safety requirement of trains along the crossing regions in railway networks. For the modeling, the component based modeling and the state-oriented modeling approaches have been integrated. First the track components and the control component are identified. The interaction of identified components, satisfying the safety requirements, is also defined in the high level architecture. Finally, state-oriented modeling approach has been adopted to design the detailed model of crossing region. Further, this paper uses the coverability tree to verify the specifications of crossing regions. By taking the crossing point as center, a circular region is introduced for safety purpose. Further, safety properties have been defined in term of place-invariants which have been verified by the state-space analysis.

It is expected that muti-core systems will become the dominant computing platform in the next few years. However, the current programming models (such as Java, .Net etc.) do not scale well to exploit the computing power of such multi-core systems. In primitive programming paradigms there exist implicit dependencies between code and program states, and compilers cannot exploit the potential concurrency present in the program unless the programmer introduces concurrency manually using multi-threading, which is prone to errors such as race conditions and deadlocks. The goal of this research is to help programmers achieve concurrency without mastering the intricacies of this domain. We propose a formal technique and a high-level algorithm to extract implicit dependencies from a sequential Java program in the form of access permission rights. The proposed technique performs static analysis of the source code on a modular basis. The inferred permissions can potentially be used by runtime engines such as Java Virtual Machine (JVM) to automatically parallelize sequential programs on multi-core systems and to reason about concurrency.