OpenRaiser/Intern-Atlas huggingface dataset:
Functional Requirements-Based Automated Testing for Avionics
Venue: arXiv cs.SE 2017
Year: 2017

We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that existing manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then formulate the automated test generation procedure and apply its prototype in case studies with industrial partners. In review, the method developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.
Agent based simulation of the evolution of society as an alternate maximization problem
Venue: arXiv cs.MA 2017
Year: 2017

Understanding the evolution of human society, as a complex adaptive system, is a task that has been looked upon from various angles. In this paper, we simulate an agent-based model with a high enough population tractably. To do this, we characterize an entity called \textit{society}, which helps us reduce the complexity of each step from $\mathcal{O}(n^2)$ to $\mathcal{O}(n)$. We propose a very realistic setting, where we design a joint alternate maximization step algorithm to maximize a certain \textit{fitness} function, which we believe simulates the way societies develop. Our key contributions include (i) proposing a novel protocol for simulating the evolution of a society with cheap, non-optimal joint alternate maximization steps (ii) providing a framework for carrying out experiments that adhere to this joint-optimization simulation framework (iii) carrying out experiments to show that it makes sense empirically (iv) providing an alternate justification for the use of \textit{society} in the simulations.
Analyzing Effects of Seasonal Variations in Wind Generation and Load on Voltage Profiles
Venue: arXiv cs.SY 2017
Year: 2017

This paper presents a methodology for building daily profiles of wind generation and load for different seasons to assess their impacts on voltage violations. The measurement-based wind models showed very high accuracy when validated against several years of actual wind power data. System load modeling was carried out by analyzing the seasonal trends that occur in residential, commercial, and industrial loads. When the proposed approach was implemented on the IEEE 118-bus system, it could identify violations in bus voltage profiles that the season-independent model could not capture. The results of the proposed approach are expected to provide better visualization of the problems that seasonal variations in wind power and load might cause to the electric power grid.
Tradeoffs Between Information and Ordinal Approximation for Bipartite Matching
Venue: arXiv cs.GT 2017
Year: 2017

We study ordinal approximation algorithms for maximum-weight bipartite matchings. Such algorithms only know the ordinal preferences of the agents/nodes in the graph for their preferred matches, but must compete with fully omniscient algorithms which know the true numerical edge weights (utilities). %instead of only their relative orderings. Ordinal approximation is all about being able to produce good results with only limited information. Because of this, one important question is how much better the algorithms can be as the amount of information increases. To address this question for forming high-utility matchings between agents in $\mathcal{X}$ and $\mathcal{Y}$, we consider three ordinal information types: when we know the preference order of only nodes in $\mathcal{X}$ for nodes in $\mathcal{Y}$, when we know the preferences of both $\mathcal{X}$ and $\mathcal{Y}$, and when we know the total order of the edge weights in the entire graph, although not the weights themselves. We also consider settings where only the top preferences of the agents are known to us, instead of their full preference orderings. We design new ordinal approximation algorithms for each of these settings, and quantify how well such algorithms perform as the amount of information given to them increases.
Three-Pass Protocol Implementation in Vigenere Cipher Classic Cryptography Algorithm with Keystream Generator Modification
Venue: arXiv cs.CR 2017
Year: 2017

Vigenere Cipher is one of the classic cryptographic algorithms and included into symmetric key cryptography algorithm, where to encryption and decryption process use the same key. Vigenere Cipher has the disadvantage that if key length is not equal to the length of the plaintext, then the key will be repeated until equal to the plaintext length, it course allows cryptanalysts to make the process of cryptanalysis. And weaknesses of the symmetric key cryptographic algorithm is the safety of key distribution factor, if the key is known by others, then the function of cryptography itself become useless. Based on two such weaknesses, in this study, we modify the key on Vigenere Cipher, so when the key length smaller than the length of plaintext entered, the key will be generated by a process, so the next key character will be different from the previous key character. In This study also applied the technique of Three-pass protocol, a technique which message sender does not need to send the key, because each using its own key for the message encryption and decryption process, so the security of a message would be more difficult to solved.
Online Job Scheduling with Redundancy and Opportunistic Checkpointing: A Speedup-Function-Based Analysis
Venue: arXiv cs.DC 2017
Year: 2017

In a large-scale computing cluster, the job completions can be substantially delayed due to two sources of variability, namely, variability in the job size and that in the machine service capacity. To tackle this issue, existing works have proposed various scheduling algorithms which exploit redundancy wherein a job runs on multiple servers until the first completes. In this paper, we explore the impact of variability in the machine service capacity and adopt a rigorous analytical approach to design scheduling algorithms using redundancy and checkpointing. We design several online scheduling algorithms which can dynamically vary the number of redundant copies for jobs. We also provide new theoretical performance bounds for these algorithms in terms of the overall job flowtime by introducing the notion of a speedup function, based on which a novel potential function can be defined to enable the corresponding competitive ratio analysis. In particular, by adopting the online primal-dual fitting approach, we prove that our SRPT+R Algorithm in a non-multitasking cluster is $(1+ε)$-speed, $\ O(\frac{1}ε)$-competitive. We also show that our proposed Fair+R and LAPS+R($β$) Algorithms for a multitasking cluster are $(4+ε)$-speed, $\ O(\frac{1}ε)$-competitive and {($2 + 2β+ 2ε)$-speed $O(\frac{1}{βε})$-competitive} respectively. We demonstrate via extensive simulations that our proposed algorithms can significantly reduce job flowtime under both the non-multitasking and multitasking modes.
An Embedded Deep Learning based Word Prediction
Venue: arXiv cs.CL 2017
Year: 2017

Recent developments in deep learning with application to language modeling have led to success in tasks of text processing, summarizing and machine translation. However, deploying huge language models for mobile device such as on-device keyboards poses computation as a bottle-neck due to their puny computation capacities. In this work we propose an embedded deep learning based word prediction method that optimizes run-time memory and also provides a real time prediction environment. Our model size is 7.40MB and has average prediction time of 6.47 ms. We improve over the existing methods for word prediction in terms of key stroke savings and word prediction rate.
Statistical Parametric Speech Synthesis Using Generative Adversarial Networks Under A Multi-task Learning Framework
Venue: arXiv cs.SD 2017
Year: 2017

In this paper, we aim at improving the performance of synthesized speech in statistical parametric speech synthesis (SPSS) based on a generative adversarial network (GAN). In particular, we propose a novel architecture combining the traditional acoustic loss function and the GAN's discriminative loss under a multi-task learning (MTL) framework. The mean squared error (MSE) is usually used to estimate the parameters of deep neural networks, which only considers the numerical difference between the raw audio and the synthesized one. To mitigate this problem, we introduce the GAN as a second task to determine if the input is a natural speech with specific conditions. In this MTL framework, the MSE optimization improves the stability of GAN, and at the same time GAN produces samples with a distribution closer to natural speech. Listening tests show that the multi-task architecture can generate more natural speech that satisfies human perception than the conventional methods.
A new and improved algorithm for online bin packing
Venue: arXiv cs.DS 2017
Year: 2017

We revisit the classic online bin packing problem. In this problem, items of positive sizes no larger than 1 are presented one by one to be packed into subsets called "bins" of total sizes no larger than 1, such that every item is assigned to a bin before the next item is presented. We use online partitioning of items into classes based on sizes, as in previous work, but we also apply a new method where items of one class can be packed into more than two types of bins, where a bin type is defined according to the number of such items grouped together. Additionally, we allow the smallest class of items to be packed in multiple kinds of bins, and not only into their own bins. We combine this with the approach of packing of sufficiently big items according to their exact sizes. Finally, we simplify the analysis of such algorithms, allowing the analysis to be based on the most standard weight functions. This simplified analysis allows us to study the algorithm which we defined based on all these ideas. This leads us to the design and analysis of the first algorithm of asymptotic competitive ratio strictly below 1.58, specifically, we break this barrier and provide an algorithm AH (Advanced Harmonic) whose asymptotic competitive ratio does not exceed 1.5783.
Towards new methods for process adjustments based on parts quality measurements
Venue: arXiv cs.SY 2017
Year: 2017

Thermoplastics injection molding allows the production of complex parts in large series. Industrial quality requirements are increasing. The injection molding process needs to be regulate in order to maintain a working point. There is actually no method to adjust all the parameters of the process in order to optimize the final quality of the product. We can rely on the success of neural networks models to propose a robust self-adaptive adjustment method. Objective is to adjust machine parameters for each cycle, based on measured quality characteristics on the produced part. A classical industrial cycle time is often less than 30 seconds ; therefore challenges are: measuring, computing and setting up machine parameters within this short timeframe. In this presentation we establish a specific literature review, on which will base our experimental works.
Linear Parsing Expression Grammars
Venue: arXiv cs.FL 2017
Year: 2017

PEGs were formalized by Ford in 2004, and have several pragmatic operators (such as ordered choice and unlimited lookahead) for better expressing modern programming language syntax. Since these operators are not explicitly defined in the classic formal language theory, it is significant and still challenging to argue PEGs' expressiveness in the context of formal language theory.Since PEGs are relatively new, there are several unsolved problems.One of the problems is revealing a subclass of PEGs that is equivalent to DFAs. This allows application of some techniques from the theory of regular grammar to PEGs. In this paper, we define Linear PEGs (LPEGs), a subclass of PEGs that is equivalent to DFAs. Surprisingly, LPEGs are formalized by only excluding some patterns of recursive nonterminal in PEGs, and include the full set of ordered choice, unlimited lookahead, and greedy repetition, which are characteristic of PEGs. Although the conversion judgement of parsing expressions into DFAs is undecidable in general, the formalism of LPEGs allows for a syntactical judgement of parsing expressions.
A Survey on Geographically Distributed Big-Data Processing using MapReduce
Venue: arXiv cs.DB 2017
Year: 2017

Hadoop and Spark are widely used distributed processing frameworks for large-scale data processing in an efficient and fault-tolerant manner on private or public clouds. These big-data processing systems are extensively used by many industries, e.g., Google, Facebook, and Amazon, for solving a large class of problems, e.g., search, clustering, log analysis, different types of join operations, matrix multiplication, pattern matching, and social network analysis. However, all these popular systems have a major drawback in terms of locally distributed computations, which prevent them in implementing geographically distributed data processing. The increasing amount of geographically distributed massive data is pushing industries and academia to rethink the current big-data processing systems. The novel frameworks, which will be beyond state-of-the-art architectures and technologies involved in the current system, are expected to process geographically distributed data at their locations without moving entire raw datasets to a single location. In this paper, we investigate and discuss challenges and requirements in designing geographically distributed data processing frameworks and protocols. We classify and study batch processing (MapReduce-based systems), stream processing (Spark-based systems), and SQL-style processing geo-distributed frameworks, models, and algorithms with their overhead issues.
Calibrated Fairness in Bandits
Venue: arXiv cs.LG 2017
Year: 2017

We study fairness within the stochastic, \emph{multi-armed bandit} (MAB) decision making framework. We adapt the fairness framework of "treating similar individuals similarly" to this setting. Here, an `individual' corresponds to an arm and two arms are `similar' if they have a similar quality distribution. First, we adopt a {\em smoothness constraint} that if two arms have a similar quality distribution then the probability of selecting each arm should be similar. In addition, we define the {\em fairness regret}, which corresponds to the degree to which an algorithm is not calibrated, where perfect calibration requires that the probability of selecting an arm is equal to the probability with which the arm has the best quality realization. We show that a variation on Thompson sampling satisfies smooth fairness for total variation distance, and give an $\tilde{O}((kT)^{2/3})$ bound on fairness regret. This complements prior work, which protects an on-average better arm from being less favored. We also explain how to extend our algorithm to the dueling bandit setting.
An Interactive Tool for Natural Language Processing on Clinical Text
Venue: arXiv cs.HC 2017
Year: 2017

Natural Language Processing (NLP) systems often make use of machine learning techniques that are unfamiliar to end-users who are interested in analyzing clinical records. Although NLP has been widely used in extracting information from clinical text, current systems generally do not support model revision based on feedback from domain experts. We present a prototype tool that allows end users to visualize and review the outputs of an NLP system that extracts binary variables from clinical text. Our tool combines multiple visualizations to help the users understand these results and make any necessary corrections, thus forming a feedback loop and helping improve the accuracy of the NLP models. We have tested our prototype in a formative think-aloud user study with clinicians and researchers involved in colonoscopy research. Results from semi-structured interviews and a System Usability Scale (SUS) analysis show that the users are able to quickly start refining NLP models, despite having very little or no experience with machine learning. Observations from these sessions suggest revisions to the interface to better support review workflow and interpretation of results.
End-to-End Learning of Semantic Grasping
Venue: arXiv cs.RO 2017
Year: 2017

We consider the task of semantic robotic grasping, in which a robot picks up an object of a user-specified class using only monocular images. Inspired by the two-stream hypothesis of visual reasoning, we present a semantic grasping framework that learns object detection, classification, and grasp planning in an end-to-end fashion. A "ventral stream" recognizes object class while a "dorsal stream" simultaneously interprets the geometric relationships necessary to execute successful grasps. We leverage the autonomous data collection capabilities of robots to obtain a large self-supervised dataset for training the dorsal stream, and use semi-supervised label propagation to train the ventral stream with only a modest amount of human supervision. We experimentally show that our approach improves upon grasping systems whose components are not learned end-to-end, including a baseline method that uses bounding box detection. Furthermore, we show that jointly training our model with auxiliary data consisting of non-semantic grasping data, as well as semantically labeled images without grasp actions, has the potential to substantially improve semantic grasping performance.
Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets
Venue: arXiv cs.LO 2017
Year: 2017

Model based diagnosis finds a growing range of practical applications, and significant performance-wise improvements have been achieved in recent years. Some of these improvements result from formulating the problem with maximum satisfiability (MaxSAT). Whereas recent work focuses on analyzing failing observations separately, it is also the case that in practical settings there may exist many failing observations. This paper first investigates the drawbacks of analyzing failing observations separately. It then shows that existing solutions do not scale for large systems. Finally, the paper proposes a novel approach for diagnosing systems with many failing observations. The proposed approach is based on implicit hitting sets and so is tightly related with the original seminal work on model based diagnosis. The experimental results demonstrate not only the importance of analyzing multiple observations simultaneously, but also the significance of the implicit hitting set approach.
DDCCast: Meeting Point to Multipoint Transfer Deadlines Across Datacenters using ALAP Scheduling Policy
Venue: arXiv cs.NI 2017
Year: 2017

Large cloud companies manage dozens of datacenters across the globe connected using dedicated inter-datacenter networks. An important application of these networks is data replication which is done for purposes such as increased resiliency via making backup copies, getting data closer to users for reduced delay and WAN bandwidth usage, and global load balancing. These replications usually lead to network transfers with deadlines that determine the time prior to which all datacenters should have a copy of the data. Inter-datacenter networks have limited capacity and need be utilized efficiently to maximize performance. In this report, we focus on applications that transfer multiple copies of objects from one datacenter to several datacenters given deadline constraints. Existing solutions are either deadline agnostic, or only consider point-to-point transfers. We propose DDCCast, a simple yet effective deadline aware point to multipoint technique based on DCCast and using ALAP traffic allocation. DDCCast performs careful admission control using temporal planning, uses rate-allocation and rate-limiting to avoid congestion and sends traffic over forwarding trees that are carefully selected to reduce bandwidth usage and maximize deadline meet rate. We perform experiments confirming DDCCast's potential to reduce total bandwidth usage by up to $45\%$ while admitting up to $25\%$ more traffic into the network compared to existing solutions that guarantee deadlines.
DCCast: Efficient Point to Multipoint Transfers Across Datacenters
Venue: arXiv cs.NI 2017
Year: 2017

Using multiple datacenters allows for higher availability, load balancing and reduced latency to customers of cloud services. To distribute multiple copies of data, cloud providers depend on inter-datacenter WANs that ought to be used efficiently considering their limited capacity and the ever-increasing data demands. In this paper, we focus on applications that transfer objects from one datacenter to several datacenters over dedicated inter-datacenter networks. We present DCCast, a centralized Point to Multi-Point (P2MP) algorithm that uses forwarding trees to efficiently deliver an object from a source datacenter to required destination datacenters. With low computational overhead, DCCast selects forwarding trees that minimize bandwidth usage and balance load across all links. With simulation experiments on Google's GScale network, we show that DCCast can reduce total bandwidth usage and tail Transfer Completion Times (TCT) by up to $50\%$ compared to delivering the same objects via independent point-to-point (P2P) transfers.
Deep Discrete Hashing with Self-supervised Pairwise Labels
Venue: arXiv cs.CV 2017
Year: 2017

Hashing methods have been widely used for applications of large-scale image retrieval and classification. Non-deep hashing methods using handcrafted features have been significantly outperformed by deep hashing methods due to their better feature representation and end-to-end learning framework. However, the most striking successes in deep hashing have mostly involved discriminative models, which require labels. In this paper, we propose a novel unsupervised deep hashing method, named Deep Discrete Hashing (DDH), for large-scale image retrieval and classification. In the proposed framework, we address two main problems: 1) how to directly learn discrete binary codes? 2) how to equip the binary representation with the ability of accurate image retrieval and classification in an unsupervised way? We resolve these problems by introducing an intermediate variable and a loss function steering the learning process, which is based on the neighborhood structure in the original space. Experimental results on standard datasets (CIFAR-10, NUS-WIDE, and Oxford-17) demonstrate that our DDH significantly outperforms existing hashing methods by large margin in terms of~mAP for image retrieval and object recognition. Code is available at \url{https://github.com/htconquer/ddh}.