OpenRaiser/Intern-Atlas huggingface dataset:
EVSO: Environment-aware Video Streaming Optimization of Power Consumption
Venue: arXiv cs.MM 2019
Year: 2019

Streaming services gradually support high-quality videos for better user experience. However, streaming high-quality video on mobile devices consumes a considerable amount of energy. This paper presents the design and prototype of EVSO, which achieves power saving by applying adaptive frame rates to parts of videos with a little degradation of the user experience. EVSO utilizes a novel perceptual similarity measurement method based on human visual perception specialized for a video encoder. We also extend the media presentation description, in which the video content is selected based only on the network bandwidth, to allow for additional consideration of the user's battery status. EVSO's streaming server preprocesses the video into several processed videos according to the similarity intensity of each part of the video and then provides the client with the processed video suitable for the network bandwidth and the battery status of the client's mobile device. The EVSO system was implemented on the commonly used H.264/AVC encoder. We conduct various experiments and a user study with nine videos. Our experimental results show that EVSO effectively reduces energy consumption when mobile devices use streaming services by 22% on average and up to 27% while maintaining the quality of the user experience.
Learning Robust 3D Face Reconstruction and Discriminative Identity Representation
Venue: arXiv cs.CV 2019
Year: 2019

3D face reconstruction from a single 2D image is a very important topic in computer vision. However, the current reconstruction methods are usually non-sensitive to face identities and over-sensitive to facial poses, which may result in similar 3D geometries for faces of different identities, or obtain different shapes for the same identity with different poses. When such methods are applied practically, their 3D estimates are either changeable for different photos of the same subject or over-regularized and generic to distinguish face identities. In this paper, we propose a robust solution to solve this problem by carefully designing a novel Siamese Convolutional Neural Network (SCNN). Specifically, regarding the 3D Morphable face Model (3DMM) parameters of the same individual as the same class, we employ the contrastive loss to enlarge the inter-class distance and meanwhile reduce the intra-class distance for the output 3DMM parameters. We also propose an identity loss to preserve the identity information for the same individual in the feature space. Training with these two losses, our SCNN could learn representations that are more discriminative for face identity and generalizable for pose variants. Experiments on the challenging database 300W-LP and AFLW2000-3D have shown the effectiveness of our method by comparing with state-of-the-arts.
Extending OCaml's 'open'
Venue: arXiv cs.PL 2019
Year: 2019

We propose a harmonious extension of OCaml's 'open' construct. OCaml's existing construct 'open M' imports the names exported by the module 'M' into the current scope. At present 'M' is required to be the path to a module. We propose extending 'open' to instead accept an arbitrary module expression, making it possible to succinctly address a number of existing scope-related difficulties that arise when writing OCaml programs.
Making Agile Development Processes fit for V-style Certification Procedures
Venue: arXiv cs.SE 2019
Year: 2019

We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an "agile development" in terms of evolutionary flexibility and continuous improvement. Yet, it enforces the overall coherence of the development artifacts (ranging from proofs over tests to code) by a particular environment (CVCE). In particular, the validation process is built around a formal development based on the interactive theorem proving system Isabelle/HOL, by linking the business logic of the application to the operating system model, down to code and concrete hardware models thanks to a series of refinement proofs. We apply both the process and its support in CVCE to a case-study that comprises a model of an odometric service in a railway-system with its corresponding implementation integrated in seL4 (a secure kernel for which a comprehensive Isabelle development exists). Novel techniques implemented in Isabelle enforce the coherence of semi-formal and formal definitions within specific certification processes in order to improve their cost-effectiveness . This paper has been published at ERTS2018.
Machine Learning based English Sentiment Analysis
Venue: arXiv cs.CL 2019
Year: 2019

Sentiment analysis or opinion mining aims to determine attitudes, judgments and opinions of customers for a product or a service. This is a great system to help manufacturers or servicers know the satisfaction level of customers about their products or services. From that, they can have appropriate adjustments. We use a popular machine learning method, being Support Vector Machine, combine with the library in Waikato Environment for Knowledge Analysis (WEKA) to build Java web program which analyzes the sentiment of English comments belongs one in four types of woman products. That are dresses, handbags, shoes and rings. We have developed and test our system with a training set having 300 comments and a test set having 400 comments. The experimental results of the system about precision, recall and F measures for positive comments are 89.3%, 95.0% and 92,.1%; for negative comments are 97.1%, 78.5% and 86.8%; and for neutral comments are 76.7%, 86.2% and 81.2%.
Robust Real-time Pedestrian Detection in Aerial Imagery on Jetson TX2
Venue: arXiv cs.CV 2019
Year: 2019

Detection of pedestrians in aerial imagery captured by drones has many applications including intersection monitoring, patrolling, and surveillance, to name a few. However, the problem is involved due to continuouslychanging camera viewpoint and object appearance as well as the need for lightweight algorithms to run on on-board embedded systems. To address this issue, the paper proposes a framework for pedestrian detection in videos based on the YOLO object detection network [6] while having a high throughput of more than 5 FPS on the Jetson TX2 embedded board. The framework exploits deep learning for robust operation and uses a pre-trained model without the need for any additional training which makes it flexible to apply on different setups with minimum amount of tuning. The method achieves ~81 mAP when applied on a sample video from the Embedded Real-Time Inference (ERTI) Challenge where pedestrians are monitored by a UAV.
Optimal Status Updating with a Finite-Battery Energy Harvesting Source
Venue: arXiv cs.IT 2019
Year: 2019

We consider an energy harvesting source equipped with a finite battery, which needs to send timely status updates to a remote destination. The timeliness of status updates is measured by a non-decreasing penalty function of the Age of Information (AoI). The problem is to find a policy for generating updates that achieves the lowest possible time-average expected age penalty among all online policies. We prove that one optimal solution of this problem is a monotone threshold policy, which satisfies (i) each new update is sent out only when the age is higher than a threshold and (ii) the threshold is a non-increasing function of the instantaneous battery level. Let $τ_B$ denote the optimal threshold corresponding to the full battery level $B$, and $p(\cdot)$ denote the age-penalty function, then we can show that $p(τ_B)$ is equal to the optimum objective value, i.e., the minimum achievable time-average expected age penalty. These structural properties are used to develop an algorithm to compute the optimal thresholds. Our numerical analysis indicates that the improvement in average age with added battery capacity is largest at small battery sizes; specifically, more than half the total possible reduction in age is attained when battery storage increases from one transmission's worth of energy to two. This encourages further study of status update policies for sensors with small battery storage.
On the Cost of Cyber Security in Smart Business
Venue: arXiv cs.CR 2019
Year: 2019

In a world, as complex and constantly changing as ours cloud computing is a driving force for shaping the IT landscape and changing the way we do business. Current trends show a world of people, things and services all digitally interconnected via the Internet of Things (IoT). This applies in particular to an industrial environment where smart devices and intelligent services pave the way for smart factories and smart businesses. This paper investigates in a use case driven study the potential of making use of smart devices to enable direct, automated and voice-controlled smart businesses. Furthermore, the paper presents an initial investigation on methodologies for measuring costs of cyber security controls for cloud services.
RGB-T Image Saliency Detection via Collaborative Graph Learning
Venue: arXiv cs.CV 2019
Year: 2019

Image saliency detection is an active research topic in the community of computer vision and multimedia. Fusing complementary RGB and thermal infrared data has been proven to be effective for image saliency detection. In this paper, we propose an effective approach for RGB-T image saliency detection. Our approach relies on a novel collaborative graph learning algorithm. In particular, we take superpixels as graph nodes, and collaboratively use hierarchical deep features to jointly learn graph affinity and node saliency in a unified optimization framework. Moreover, we contribute a more challenging dataset for the purpose of RGB-T image saliency detection, which contains 1000 spatially aligned RGB-T image pairs and their ground truth annotations. Extensive experiments on the public dataset and the newly created dataset suggest that the proposed approach performs favorably against the state-of-the-art RGB-T saliency detection methods.
A New Hierarchical Software Architecture Towards Safety-Critical Aspects of a Drone System
Venue: arXiv cs.SE 2019
Year: 2019

In this paper, a new hierarchical software architecture is proposed to improve the safety and reliability of a safety-critical drone system from the perspective of its source code. The proposed architecture uses formal verification methods to ensure that the implementation of each module satisfies its expected design specification, so that it prevents a drone from crashing due to unexpected software failures. This study builds on top of a formally verified operating system kernel, certified kit operating system (CertiKOS). Since device drivers are considered the most important parts affecting the safety of the drone system, we focus mainly on verifying bus drivers such as the serial peripheral interface and the inter-integrated circuit drivers in a drone system using a rigorous formal verification method. Experiments have been carried out to demonstrate the improvement in reliability in case of device anomalies.
Predicting Dynamic Modulus of Asphalt Mixture Using Data Obtained from Indirect Tension Mode of Testing
Venue: arXiv cs.CE 2019
Year: 2019

Understanding stress-strain behavior of asphalt pavement under repetitive traffic loading is of critical importance to predict pavement performance and service life. For viscoelastic materials, the stress-strain relationship can be represented by the dynamic modulus. The dynamic modulus test in indirect tension mode can be used to measure the modulus of each specific layer of asphalt pavements using representative samples. Dynamic modulus is a function of material properties, loading, and environmental conditions. Developing predictive models for dynamic modulus is efficient and cost effective. This article focuses on developing an accurate Finite Element (FE) model using mixture elastic modulus and asphalt binder properties to predict dynamic modulus of asphalt mix in indirect tension mode. An Artificial Neural Network (ANN) is used to back-calculate the elastic modulus of asphalt mixtures. The developed FE model was verified against experimental results of field cores from nine different pavement sections from five districts in the State of Minnesota. It is demonstrated that the ANN modeling is a powerful tool to back-calculate the elastic modulus and FE model is capable of accurately predicting dynamic modulus.
Modern theory of hydraulic fracture modeling with using explicit and implicit schemes
Venue: arXiv cs.CE 2019
Year: 2019

The paper presents novel results, obtained on the basis of the modified theory of hydraulic fractures (HF). The theory underlines significance of the speed equation. When applied to numerical simulation of HF, the theory reveals three distinct issues: (i) modeling the central part of a HF; (ii) modeling the near-front zone; and (iii) tracing changes in the shape of a fracture contour. Modeling the central part leads to a stiff system of ODE in time, what strongly complicates its integration. For explicit schemes, it requires small time steps to meet the CFL condition. For implicit schemes, it requires proper preconditioners. The gains and flaws of the two strategies are discussed. It is noted that a rough spatial mesh may be used in the central part. Modeling the near-front zone reveals the vital role of the speed equation for HF modeling by any method. Its asymptotic analysis has resulted in the fundamental concept of the universal asymptotic umbrella. For the near-front zone, it is also established that a notable part of the zone adjacent to the front propagates virtually as a simple wave. This implies that the CFL condition of stability for this zone is much less restrictive than for the central part of the fracture. Of essence is also that the wave-like propagation of the near front zone makes preferable upwind schemes of time stepping. On whole, the analysis implies that explicit time stepping may be complementing, competitive and even superior over implicit integration. Tracing changes in the front shape appears merely in 3D problems when the contour changes its form. The problem, being essentially geometrical, it may be solved separately by various methods, including fast marching, level set and the simplest string/marker methods. In 1D cases, it does not arise at all. Quantitative estimations and numerical examples illustrate the theoretical conclusions.
Towards Interlingua Neural Machine Translation
Venue: arXiv cs.CL 2019
Year: 2019

Common intermediate language representation in neural machine translation can be used to extend bilingual to multilingual systems by incremental training. In this paper, we propose a new architecture based on introducing an interlingual loss as an additional training objective. By adding and forcing this interlingual loss, we are able to train multiple encoders and decoders for each language, sharing a common intermediate representation. Translation results on the low-resourced tasks (Turkish-English and Kazakh-English tasks, from the popular Workshop on Machine Translation benchmark) show the following BLEU improvements up to 2.8. However, results on a larger dataset (Russian-English and Kazakh-English, from the same baselines) show BLEU loses if the same amount. While our system is only providing improvements for the low-resourced tasks in terms of translation quality, our system is capable of quickly deploying new language pairs without retraining the rest of the system, which may be a game-changer in some situations (i.e. in a disaster crisis where international help is required towards a small region or to develop some translation system for a client). Precisely, what is most relevant from our architecture is that it is capable of: (1) reducing the number of production systems, with respect to the number of languages, from quadratic to linear (2) incrementally adding a new language in the system without retraining languages previously there and (3) allowing for translations from the new language to all the others present in the system
Reconfigurable Hardware Implementation of the Successive Overrelaxation Method
Venue: arXiv cs.DC 2019
Year: 2019

In this chapter, we study the feasibility of implementing SOR in reconfigurable hardware. We use Handel-C, a higher level design tool, to code our design, which is analyzed, synthesized, and placed and routed using the FPGAs proprietary software (DK Design Suite, Xilinx ISE 8.1i, and Quartus II 5.1). We target Virtex II Pro, Altera Stratix, and Spartan3L, which is embedded in the RC10 FPGA-based system from Celoxica. We report our timing results when targeting Virtex II Pro and compare them to software version results written in C++ and running on a general purpose processor (GPP).
Inferring Concise Specifications of APIs
Venue: arXiv cs.SE 2019
Year: 2019

Modern software relies on libraries and uses them via application programming interfaces (APIs). Correct API usage as well as many software engineering tasks are enabled when APIs have formal specifications. In this work, we analyze the implementation of each method in an API to infer a formal postcondition. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. Our key idea is an algorithm that converts such exponentially large specifications into a form that is more concise and thus more usable. This is done by leveraging the structure of the specifications that result from the use of SP. We applied our technique to infer postconditions for over 2,300 methods in seven popular Java libraries. Our technique was able to infer specifications for 75.7% of these methods, each of which was verified using an Extended Static Checker. We also found that 84.6% of resulting specifications were less than 1/4 page (20 lines) in length. Our technique was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.
Switches in Eulerian graphs
Venue: arXiv cs.DS 2019
Year: 2019

We show that the graph transformation problem of turning a simple graph into an Eulerian one by a minimum number of single edge switches is NP-hard. Further, we show that any simple Eulerian graph can be transformed into any other such graph by a sequence of 2-switches (i.e., exchange of two edge pairs), such that every intermediate graph is also Eulerian. However, finding the shortest such sequence also turns out to be an NP-hard problem.
Target Set in Threshold Models
Venue: arXiv cs.DS 2019
Year: 2019

Consider a graph $G$ and an initial coloring, where each node is blue or red. In each round, all nodes simultaneously update their color based on a predefined rule. In a threshold model, a node becomes blue if a certain number or fraction of its neighbors are blue and red otherwise. What is the minimum number of nodes which must be blue initially so that the whole graph becomes blue eventually? We study this question for graphs which have expansion properties, parameterized by spectral gap, in particular the Erdős-Rényi random graph and random regular graphs.
A Correctness Result for Synthesizing Plans With Loops in Stochastic Domains
Venue: arXiv cs.AI 2019
Year: 2019

Finite-state controllers (FSCs), such as plans with loops, are powerful and compact representations of action selection widely used in robotics, video games and logistics. There has been steady progress on synthesizing FSCs in deterministic environments, but the algorithmic machinery needed for lifting such techniques to stochastic environments is not yet fully understood. While the derivation of FSCs has received some attention in the context of discounted expected reward measures, they are often solved approximately and/or without correctness guarantees. In essence, that makes it difficult to analyze fundamental concerns such as: do all paths terminate, and do the majority of paths reach a goal state? In this paper, we present new theoretical results on a generic technique for synthesizing FSCs in stochastic environments, allowing for highly granular specifications on termination and goal satisfaction.
Vector Field Neural Networks
Venue: arXiv cs.LG 2019
Year: 2019

This work begins by establishing a mathematical formalization between different geometrical interpretations of Neural Networks, providing a first contribution. From this starting point, a new interpretation is explored, using the idea of implicit vector fields moving data as particles in a flow. A new architecture, Vector Fields Neural Networks(VFNN), is proposed based on this interpretation, with the vector field becoming explicit. A specific implementation of the VFNN using Euler's method to solve ordinary differential equations (ODEs) and gaussian vector fields is tested. The first experiments present visual results remarking the important features of the new architecture and providing another contribution with the geometrically interpretable regularization of model parameters. Then, the new architecture is evaluated for different hyperparameters and inputs, with the objective of evaluating the influence on model performance, computational time, and complexity. The VFNN model is compared against the known basic models Naive Bayes, Feed Forward Neural Networks, and Support Vector Machines(SVM), showing comparable, or better, results for different datasets. Finally, the conclusion provides many new questions and ideas for improvement of the model that can be used to increase model performance.
Are Automated Vehicles Safer than Manually Driven Cars?
Venue: arXiv cs.HC 2019
Year: 2019

Are automated vehicles really safer than manually driven vehicles? If so, how would we know? Answering this question has spurred a contentious debate. Unfortunately, several issues make answering this question difficult for the foreseeable future. First, how do we measure safety? Second, how can we keep track of automated vehicle (AV) safety? Finally, how do we determine what is or what is not an AV? Until these questions are addressed, it will continue to be difficult to determine whether or when AVs might really be safer than manually driven vehicles.