Predictive Intelligent Transportation: Alleviating Traffic Congestion in the Internet of Vehicles.

Due to the limitations of data transfer technologies, existing studies on urban traffic control mainly focused on isolated dimension control such as traffic signal control or vehicle route guidance to alleviate traffic congestion. However, in real traffic, the distribution of traffic flow is the result of multiple dimensions whose future state is influenced by each dimension's decisions. Presently, the development of the Internet of Vehicles enables an integrated intelligent transportation system. This paper proposes an integrated intelligent transportation model that can optimize predictive traffic signal control and predictive vehicle route guidance simultaneously to alleviate traffic congestion based on their feedback regulation relationship. The challenges of this model lie in that the formulation of the nonlinear feedback relationship between various dimensions is hard to describe and the design of a corresponding solving algorithm that can obtain Pareto optimality for multi-dimension control is complex. In the integrated model, we introduce two medium variables-predictive traffic flow and the predictive waiting time-to two-way link the traffic signal control and vehicle route guidance. Inspired by game theory, an asymmetric information exchange framework-based updating distributed algorithm is designed to solve the integrated model. Finally, an experimental study in two typical traffic scenarios shows that more than 73.33% of the considered cases adopting the integrated model achieve Pareto optimality.

UTM-Chain: Blockchain-Based Secure Unmanned Traffic Management for Internet of Drones.

Unmanned aerial systems (UAVs) are dramatically evolving and promoting several civil applications. However, they are still prone to many security issues that threaten public safety. Security becomes even more challenging when they are connected to the Internet as their data stream is exposed to attacks. Unmanned traffic management (UTM) represents one of the most important topics for small unmanned aerial systems for beyond-line-of-sight operations in controlled low-altitude airspace. However, without securing the flight path exchanges between drones and ground stations or control centers, serious security threats may lead to disastrous situations. For example, a predefined flight path could be easily altered to make the drone perform illegal operations. Motivated by these facts, this paper discusses the security issues for UTM's components and addresses the security requirements for such systems. Moreover, we propose UTM-Chain, a lightweight blockchain-based security solution using hyperledger fabric for UTM of low-altitude UAVs which fits the computational and storage resources limitations of UAVs. Moreover, UTM-Chain provides secure and unalterable traffic data between the UAVs and their ground control stations. The performance of the proposed system related to transaction latency and resource utilization is analyzed by using cAdvisor. Finally, the analysis of security aspects demonstrates that the proposed UTM-Chain scheme is feasible and extensible for the secure sharing of UAV data.

Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets.

This work deals with the language-based opacity verification and enforcement problems in discrete event systems modeled with labeled Petri nets. Opacity is a security property that relates to privacy protection by hiding secret information of a system from an external observer called an "intruder". A secret can be a subset of a system's language. In this case, opacity is referred to as language-based opacity. A system is said to be language-based opaque if an intruder, with a partial observation on the system's behavior, cannot deduce whether the sequences of events corresponding to the generated observations are included in the secret language or not. We propose a novel and efficient approach for language-based opacity verification and enforcement, using the concepts of basis markings and basis partition. First, a sufficient condition is formulated to check language-based opacity for labeled Petri nets by solving an integer-programming problem. A unique graph, called a modified basis reachability graph (MBRG), is then derived to verify different language-based opacity properties. The proposed method relaxes the acyclicity assumption of the unobservable transition subnet thanks to the basis partition notion. A new embedded insertion function technique is also provided to deal with opacity enforcement. This technique ensures that no new observed behavior is created. A verification algorithm is developed to check the enforceability of a system. Finally, once a system is proved to be enforceable, an algorithm is given to construct a new structure, called an insertion automaton, which synthesizes all possible insertion functions that ensure opacity.

Most permissive liveness-enforcing Petri net supervisors for discrete event systems via linear monitors.

This paper proposes a deadlock prevention method to design a maximally permissive liveness-enforcing pure Petri net supervisor for a discrete event system, if such a supervisor exists; otherwise, it obtains the most permissive one in the sense that no other pure liveness-enforcing supervisors via linear monitors can be more permissive than it. This paper exploits an iterative method. At each iteration, a first-met bad marking (FBM) is singled out and an integer linear programming problem (ILPP) is configured. If a feasible solution can be found for the ILPP, then a place invariant (PI) is designed to prohibit the FBM from being reached while no legal marking is forbidden. If the ILPP has no solution, we collect all these FBMs that cannot be optimally controlled. For each of such FBMs, another ILPP is designed to find the least number of legal markings whose reachability conditions contradict the current considered FBM and enumerate all the optimal solutions of this ILPP. Based on it, we develop a 0-1 linear programming problem to find the maximal number of legal markings after removing all the contradictory legal markings. Then, the new sets of legal markings and FBMs are obtained, and we return to the iteration stage to redesign a PI to control each FBM if the ILPP has a feasible solution. Repeat the above process until no FBM can be reached. Finally, a most permissive pure liveness-enforcing supervisor via linear monitors is derived. Two Petri net models are used to illustrate the proposed method.

BROMETH: Methodology to design safe reconfigurable medical robotic systems.

BACKGROUND: This research paper deals with the development of a medical robotized control system for supracondylar humeral fracture treatment. Concurrent access to shared resources and applying reconfiguration scenarios can jeopardize the safety of the system. METHODS: A new methodology is proposed in this paper, termed BROMETH, to guarantee the safety of such critical systems from their specification to their deployment, and passing through certification and implementation. The solution is applied to a real case study named Browser-based Reconfigurable Orthopedic Surgery (abbrev. BROS), a robotized platform dedicated to the treatment of supracondylar fractures, to illustrate the paper's contribution. This work starts from a medical issue, namely supracondylar humeral fracture treatment, to establish a new informatics solution, namely a new methodology to design safe reconfigurable medical robotic systems. RESULTS: The results of the experiments performed on real SCH fracture radiographies were quite satisfactory. CONCLUSIONS: Clinical experiments can then be performed after deploying the system on real hardware.