OpenRaiser/Intern-Atlas huggingface dataset:
Application of Ontologies in Identifying Requirements Patterns in Use Cases
Venue: arXiv cs.SE 2014
Year: 2014

Use case specifications have successfully been used for requirements description. They allow joining, in the same modeling space, the expectations of the stakeholders as well as the needs of the software engineer and analyst involved in the process. While use cases are not meant to describe a system's implementation, by formalizing their description we are able to extract implementation relevant information from them. More specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. In the paper we propose the transformation of Use Case descriptions expressed in a Controlled Natural Language into an ontology expressed in the Web Ontology Language (OWL). OWL's query engines can then be used to identify requirements patterns expressed as queries over the ontology. We describe a tool that we have developed to support the approach and provide an example of usage.
Correct-by-construction model composition: Application to the Invasive Software Composition method
Venue: arXiv cs.SE 2014
Year: 2014

Composition technologies improve reuse in the development of large-scale complex systems. Safety critical systems require intensive validation and verification activities. These activities should be compositional in order to reduce the amount of residual verification activities that must be conducted on the composite in addition to the ones conducted on each components. In order to ensure the correctness of compositional verification and assess the minimality of the residual verification, the contribution proposes to use formal specification and verification at the composition operator level. A first experiment was conducted in [15] using proof assistants to formalize the generic composition technology ISC and prove that type checking was compositional. This contribution extends our early work to handle full model conformance and study the mandatory residual verification. It shows that ISC operators are not fully compositional with respect to conformance and provides the minimal preconditions on the operators mandatory to ensure compositional conformance. The appropriate operators from ISC (especially bind) have been implemented in the COQ4MDE framework that provides a full implementation of MOF in the COQ proof assistant. Expected properties, respectively residual verification, are expressed as post, respectfully pre, conditions for the composition operators. The correctness of the compositional verification is proven in COQ.
Optimal Power Control for Analog Bidirectional Relaying with Long-Term Relay Power Constraint
Venue: arXiv cs.IT 2014
Year: 2014

Wireless systems that carry delay-sensitive information (such as speech and/or video signals) typically transmit with fixed data rates, but may occasionally suffer from transmission outages caused by the random nature of the fading channels. If the transmitter has instantaneous channel state information (CSI) available, it can compensate for a significant portion of these outages by utilizing power allocation. In a conventional dual-hop bidirectional amplify-and-forward (AF) relaying system, the relay already has instantaneous CSI of both links available, as this is required for relay gain adjustment. We therefore develop an optimal power allocation strategy for the relay, which adjusts its instantaneous output power to the minimum level required to avoid outages, but only if the required output power is below some cutoff level; otherwise, the relay is silent in order to conserve power and prolong its lifetime. The proposed scheme is proven to minimize the system outage probability, subject to an average power constraint at the relay and fixed output powers at the end nodes.
Bayes and Naive Bayes Classifier
Venue: arXiv cs.LG 2014
Year: 2014

The Bayesian Classification represents a supervised learning method as well as a statistical method for classification. Assumes an underlying probabilistic model and it allows us to capture uncertainty about the model in a principled way by determining probabilities of the outcomes. This Classification is named after Thomas Bayes (1702-1761), who proposed the Bayes Theorem. Bayesian classification provides practical learning algorithms and prior knowledge and observed data can be combined. Bayesian Classification provides a useful perspective for understanding and evaluating many learning algorithms. It calculates explicit probabilities for hypothesis and it is robust to noise in input data. In statistical classification the Bayes classifier minimises the probability of misclassification. That was a visual intuition for a simple case of the Bayes classifier, also called: 1)Idiot Bayes 2)Naive Bayes 3)Simple Bayes
Analysis of Petri Net Models through Stochastic Differential Equations
Venue: arXiv cs.PF 2014
Year: 2014

It is well known, mainly because of the work of Kurtz, that density dependent Markov chains can be approximated by sets of ordinary differential equations (ODEs) when their indexing parameter grows very large. This approximation cannot capture the stochastic nature of the process and, consequently, it can provide an erroneous view of the behavior of the Markov chain if the indexing parameter is not sufficiently high. Important phenomena that cannot be revealed include non-negligible variance and bi-modal population distributions. A less-known approximation proposed by Kurtz applies stochastic differential equations (SDEs) and provides information about the stochastic nature of the process. In this paper we apply and extend this diffusion approximation to study stochastic Petri nets. We identify a class of nets whose underlying stochastic process is a density dependent Markov chain whose indexing parameter is a multiplicative constant which identifies the population level expressed by the initial marking and we provide means to automatically construct the associated set of SDEs. Since the diffusion approximation of Kurtz considers the process only up to the time when it first exits an open interval, we extend the approximation by a machinery that mimics the behavior of the Markov chain at the boundary and allows thus to apply the approach to a wider set of problems. The resulting process is of the jump-diffusion type. We illustrate by examples that the jump-diffusion approximation which extends to bounded domains can be much more informative than that based on ODEs as it can provide accurate quantity distributions even when they are multi-modal and even for relatively small population levels. Moreover, we show that the method is faster than simulating the original Markov chain.
Minimum total weighted completion time: Faster approximation schemes
Venue: arXiv cs.DS 2014
Year: 2014

We study classic scheduling problems on uniformly related machines. Efficient polynomial time approximation schemes (EPTAS's) are fast and practical approximation schemes. New methods and techniques are essential in developing such improved approximation schemes, and their design is a primary goal of this research agenda. We present EPTAS's for the scheduling problem of a set of jobs on uniformly related machines so as to minimize the total weighted completion time, both for the case with release dates and its special case without release dates. These problems are NP-hard in the strong sense, and therefore EPTAS's are the best possible approximation schemes unless P=NP. Previously, only PTAS's were known for these two problems, while an EPTAS was known only for the special case of identical machines without release dates.
Multi-User Coverage Probability of Uplink Cellular Systems: a Stochastic Geometry Approach
Venue: arXiv cs.IT 2014
Year: 2014

We analyze the coverage probability of multi-user uplink cellular networks with fractional power control. We use a stochastic geometry approach where the mobile users are distributed as a Poisson Point Process (PPP), whereas the serving base station (BS) is placed at the origin. Using conditional thinning, we are able to calculate the coverage probability of $k$ users which are allocated a set of orthogonal resources in the cell of interest, obtaining analytical expressions for this probability considering their respective distances to the serving BS. These expressions give useful insights on the interplay between the power control policy, the interference level and the degree of fairness among different users in the system.
A Collaborative Framework for In-network Video Caching in Mobile Networks
Venue: arXiv cs.NI 2014
Year: 2014

Due to explosive growth of online video content in mobile wireless networks, in-network caching is becoming increasingly important to improve the end-user experience and reduce the Internet access cost for mobile network operators. However, caching is a difficult problem due to the very large number of online videos and video requests,limited capacity of caching nodes, and limited bandwidth of in-network links. Existing solutions that rely on static configurations and average request arrival rates are insufficient to handle dynamic request patterns effectively. In this paper, we propose a dynamic collaborative video caching framework to be deployed in mobile networks. We decompose the caching problem into a content placement subproblem and a source-selection subproblem. We then develop SRS (System capacity Reservation Strategy) to solve the content placement subproblem, and LinkShare, an adaptive traffic-aware algorithm to solve the source selection subproblem. Our framework supports congestion avoidance and allows merging multiple requests for the same video into one request. We carry extensive simulations to validate the proposed schemes. Simulation results show that our SRS algorithm achieves performance within 1-3% of the optimal values and LinkShare significantly outperforms existing solutions.
Resolving Multi-path Interference in Time-of-Flight Imaging via Modulation Frequency Diversity and Sparse Regularization
Venue: arXiv cs.CV 2014
Year: 2014

Time-of-flight (ToF) cameras calculate depth maps by reconstructing phase shifts of amplitude-modulated signals. For broad illumination or transparent objects, reflections from multiple scene points can illuminate a given pixel, giving rise to an erroneous depth map. We report here a sparsity regularized solution that separates K-interfering components using multiple modulation frequency measurements. The method maps ToF imaging to the general framework of spectral estimation theory and has applications in improving depth profiles and exploiting multiple scattering.
Formale Entwicklung einer Steuerung für eine Fertigungszelle mit SYSYFOS
Venue: arXiv cs.LO 2014
Year: 2014

Using the synthesis approach of Manna and Waldinger, a formally specified and verified control circuitery for a production cell was developped. Building an appropriate formal language level, we could achieve a requirements specification to the informal description. We demonstrated that the paradigm of deductive synthesis can be applied to the development of complete verified systems, including hardware and mechanics. We defined two domain-specific logical operators that schematise frequent patterns in specification and proof and hence allow a more concise and expressive presentation. In Burghardt (1995), an english short version of this paper, without appendices, can be found.
Design of Reversible Counter
Venue: arXiv cs.OH 2014
Year: 2014

This article presents a research work on the design and synthesis of sequential circuits and flip-flops that are available in digital arena; and describes a new synthesis design of reversible counter that is optimized in terms of quantum cost, delay and garbage outputs compared to the existing designs. We proposed a new model of reversible T flip-flop in designing reversible counter
Steerable Antennas for Automotive Communication Systems
Venue: arXiv cs.OH 2014
Year: 2014

This research project undertakes a comprehensive analysis of RF beamforming techniques for design, simulation, fabrication, and measurement of Butler Matrix and Rotman Lens beamforming networks. It is aimed to develop novel and well-established designs for steerable antenna systems that can be used in vehicular telematics and automotive communication systems based on microwave and millimeter-wave techniques.
Upper-Bounding the Capacity of Relay Communications - Part II
Venue: arXiv cs.IT 2014
Year: 2014

This paper focuses on the capacity of peer-to-peer relay communications wherein the transmitter are assisted by an arbitrary number of parallel relays, i.e. there is no link and cooperation between the relays themselves. We detail the mathematical model of different relaying strategies including cutset and amplify and forward strategies. The cutset upper bound capacity is presented as a reference to compare another realistic strategy. We present its outer region capacity which is lower than that in the existing literature. We show that a multiple parallel relayed network achieves its maximum capacity by virtue of only one relay or by virtue of all relays together. Adding a relay may even decrease the overall capacity or may do not change it. We exemplify various outer region capacities of the addressed strategies with two different case studies. The results exhibit that in low signal-to-noise ratio (SNR) environments the cutset outperforms the amplify and forward strategy and this is contrary in high SNR environments.
Higher Rank Interference Effect on Weak Beamforming or OSTBC Terminals
Venue: arXiv cs.IT 2014
Year: 2014

User performance on a wireless network depends on whether a neighboring cochannel interferer applies a single (spatial) stream or a multi stream transmission. This work analyzes the impact of interference rank on a beamforming and orthogonal space-time block coded (OSTBC) user transmission. We generalize existing analytical results on signal-to-interference-plus-noise-ratio (SINR) distribution and outage probability under arbitrary number of unequal power interferers. We show that higher rank interference causes lower outage probability, and can support better outage threshold especially in the case of beamforming.
Research Challenges in Wireless Sensor Network: A State of the Play
Venue: arXiv cs.NI 2014
Year: 2014

A wireless sensor network (WSN) has important applications such as remote environmental monitoring and target tracking. This has been enabled by the availability, particularly in recent years, of sensors that are smaller, cheaper, and intelligent. These sensors are equipped with wireless interfaces with which they can communicate with one another to form a network. The design of a WSN depends significantly on the application, and it must consider factors such as the environment, the applications design objectives, cost, hardware, and system constraints. The goal of survey is to present a comprehensive review of the recent literature in wireless sensor network. This paper reviews the major development and new research challenges in this area.
On the Remarkable Features of Binding Forms
Venue: arXiv cs.LO 2014
Year: 2014

Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order sentences represent only one of the remarkable results. According to the criteria used to identify the particular classes of interest, this process was declined into several research programs, of which some of the most deeply investigated are the ones classifying sentences in prenex normal form in base of their prefix vocabulary. Unfortunately, almost all of these approaches did not shed any light on the reasons why modal logic is so robustly decidable. Trying to answer to this question, Andreka, van Benthem, and Nemeti introduced the guarded fragment of first-order logic, which generalizes the modal framework by essentially retaining all its fundamental properties. They started, so, a completely new research program based on the way quantifications can be relativized. Although this approach succeeded in its original task, we cannot consider it satisfactory in spotting the reasons why some complex extensions of modal logic are well-behaved. In particular, by just using the related results, we are not able to derive the decidability of multi-agent logics for strategic abilities. In this paper, aiming to lay the foundation for a more thorough understanding of some of these decidability questions, we introduce a new kind of classification based on the binding forms that are admitted in a sentence, i.e., on the way the arguments of a relation can be bound to a variable. We describe a hierarchy of first-order fragments based on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with the guarded logic and related extensions. We also prove, via a new model-theoretic technique, that it enjoys the finite-model property and a PSpace satisfiability problem.
Density Evolution for Min-Sum Decoding of LDPC Codes Under Unreliable Message Storage
Venue: arXiv cs.IT 2014
Year: 2014

We analyze the performance of quantized min-sum decoding of low-density parity-check codes under unreliable message storage. To this end, we introduce a simple bit-level error model and show that decoder symmetry is preserved under this model. Subsequently, we formulate the corresponding density evolution equations to predict the average bit error probability in the limit of infinite blocklength. We present numerical threshold results and we show that using more quantization bits is not always beneficial in the context of faulty decoders.
LOS-based Conjugate Beamforming and Power-Scaling Law in Massive-MIMO Systems
Venue: arXiv cs.IT 2014
Year: 2014

This paper is concerned with massive-MIMO systems over Rician flat fading channels. In order to reduce the overhead to obtain full channel state information and to avoid the pilot contamination problem, by treating the scattered component as interference, we investigate a transmit and receive conjugate beamforming (BF) transmission scheme only based on the line-of-sight (LOS) component. Under Rank-1 model, we first consider a single-user system with N transmit and M receive antennas, and focus on the problem of power-scaling law when the transmit power is scaled down proportionally to 1/MN. It can be shown that as MN grows large, the scattered interference vanishes, and the ergodic achievable rate is higher than that of the corresponding BF scheme based fast fading and minimum mean-square error (MMSE) channel estimation. Then we further consider uplink and downlink single-cell scenarios where the base station (BS) has M antennas and each of K users has N antennas. When the transmit power for each user is scaled down proportionally to 1/MN, it can be shown for finite users that as M grows without bound, each user obtains finally the same rate performance as in the single-user case. Even when N grows without bound, however, there still remains inter-user LOS interference that can not be cancelled. Regarding infinite users, there exists such a power scaling law that when K and the b-th power of M go to infinity with a fixed and finite ratio for a given b in (0, 1), not only inter-user LOS interference but also fast fading effect can be cancelled, while fast fading effect can not be cancelled if b=1. Extension to multi-cells and frequency-selective channels are also discussed shortly. Moreover, numerical results indicate that spacial antenna correlation does not have serious influence on the rate performance, and the BS antennas may be allowed to be placed compactly when M is very large.
Memory-only selection of dictionary PINs
Venue: arXiv cs.CR 2014
Year: 2014

We estimate the security of dictionary-based PINs (Personal Identification Numbers) that a user selects from his/her memory without any additional aids. The estimates take into account the distribution of words in source language. We use established security metrics, such as entropy, guesswork, marginal guesswork and marginal success rate. The metrics are evaluated for various scenarios -- aimed at improving the security of the produced PINs. In general, plain and straightforward construction of memory-only dictionary PINs yields unsatisfactory results and more involved methods must be used to produce secure PINs.
Improving Bilayer Product Quantization for Billion-Scale Approximate Nearest Neighbors in High Dimensions
Venue: arXiv cs.CV 2014
Year: 2014

The top-performing systems for billion-scale high-dimensional approximate nearest neighbor (ANN) search are all based on two-layer architectures that include an indexing structure and a compressed datapoints layer. An indexing structure is crucial as it allows to avoid exhaustive search, while the lossy data compression is needed to fit the dataset into RAM. Several of the most successful systems use product quantization (PQ) for both the indexing and the dataset compression layers. These systems are however limited in the way they exploit the interaction of product quantization processes that happen at different stages of these systems. Here we introduce and evaluate two approximate nearest neighbor search systems that both exploit the synergy of product quantization processes in a more efficient way. The first system, called Fast Bilayer Product Quantization (FBPQ), speeds up the runtime of the baseline system (Multi-D-ADC) by several times, while achieving the same accuracy. The second system, Hierarchical Bilayer Product Quantization (HBPQ) provides a significantly better recall for the same runtime at a cost of small memory footprint increase. For the BIGANN dataset of billion SIFT descriptors, the 10% increase in Recall@1 and the 17% increase in Recall@10 is observed.
Improved 3-Dimensional Security in Cloud Computing
Venue: arXiv cs.CR 2014
Year: 2014

Cloud computing is a trending technology in the field of Information Technology as it allows sharing of resources over a network. The reason Cloud computing gained traction so rapidly was because of its performance, availability and low cost among other features. Besides these features, companies are still refraining from binding their business with cloud computing due to the fear of data leakage. The focus of this paper is on the problem of data leakage. It proposes a framework which works in two phases. The first phase consists of data encryption and classification which is performed before storing the data. In this phase, the client may want to encrypt his data prior to uploading. After encryption, data is classified using three parameters namely Confidentiality [C], Integrity [I] and Availability [A]. With the help of proposed algorithm, criticality rating (Cr) of the data is calculated. According to the Cr, security will be provided on the basis of the 3 Dimensions proposed in this paper. The second phase consists of data retrieval by the client. As per the concept of 3D, users who want to access their data need to be authenticated, to avoid data from being compromised. Before every access to data, the users identity is verified for authorization. After the user is authorized for data access, if the data is encrypted, the user can decrypt the same.
Evaluation and Ranking of Machine Translated Output in Hindi Language using Precision and Recall Oriented Metrics
Venue: arXiv cs.CL 2014
Year: 2014

Evaluation plays a crucial role in development of Machine translation systems. In order to judge the quality of an existing MT system i.e. if the translated output is of human translation quality or not, various automatic metrics exist. We here present the implementation results of different metrics when used on Hindi language along with their comparisons, illustrating how effective are these metrics on languages like Hindi (free word order language).