Programming Languages and Compilers Commons^™

Defeating Sql Injection, Lwin Khin Shar, Hee Beng Kuan Tan

Research Collection School Of Computing and Information Systems

The best strategy for combating SQL injection, which has emerged as the most widespread website security risk, calls for integrating defensive coding practices with both vulnerability detection and runtime attack prevention methods.

Improved Bdd-Based Discrete Analysis Of Timed Systems, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu

Research Collection School Of Computing and Information Systems

Model checking timed systems through digitization is relatively easy, compared to zone-based approaches. The applicability of digitization, however, is limited mainly for two reasons, i.e., it is only sound for closed timed systems; and clock ticks cause state space explosion. The former is mild as many practical systems are subject to digitization. It has been shown that BDD-based techniques can be used to tackle the latter to some extent. In this work, we significantly improve the existing approaches by keeping the ticks simple in the BDD encoding. Taking advantage of the ‘simple’ nature of clock ticks, we fine-tune the encoding …

Automatic Compositional Verification Of Timed Systems, Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong, Étienne André

Research Collection School Of Computing and Information Systems

Specification and verification of real-time systems are important research topics with crucial applications; however, the so-called state space explosion problem often prevents model checking to be used in practice for large systems. In this work, we present a self-contained toolkit to analyze real-time systems specified using event-recording automata (ERAs), which supports system modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that our tool outperforms the state-of-the-art timed model checker.

Analytic Programming With Fmri Data: A Quick-Start Guide For Statisticians Using R, Ani Eloyan, Shanshan Li, John Muschelli, Jim Pekar, Stewart Mostofsky, Brian S. Caffo

Johns Hopkins University, Dept. of Biostatistics Working Papers

Functional magnetic resonance imaging (fMRI) is a thriving field that plays an important role in medical imaging analysis, biological and neuroscience research and practice. This manuscript gives a didactic introduction to the statistical analysis of fMRI data using the R project along with the relevant R code. The goal is to give tatisticians who would like to pursue research in this area a quick start for programming with fMRI data along with the available data visualization tools.

Using Monterey Phoenix To Formalize And Verify System Architectures, Jiexin Zhang, Yang Liu, Mikhail Auguston, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Modeling and analyzing software architectures are useful for helping to understand the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. Firstly, we formalize the syntax and operational semantics for MP. This language is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. Secondly, …

Probabilistic Model Checking Multi-Agent Behaviors In Dispersion Games Using Counter Abstraction, Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Lin Gui, Jin Song Dong, Ho-Fung Leung

Research Collection School Of Computing and Information Systems

Accurate analysis of the stochastic dynamics of multi-agent system is important but challenging. Probabilistic model checking, a formal technique for analysing a system which exhibits stochastic behaviors, can be a natural solution to analyse multi-agent systems. In this paper, we investigate this problem in the context of dispersion games focusing on two strategies: basic simple strategy (BSS) and extended simple strategies (ESS). We model the system using discrete-time Markov chain (DTMC) and reduce the state space of the models by applying counter abstraction technique. Two important properties of the system are considered: convergence and convergence rate. We show that these …

A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Real-life systems are usually hard to control, due to their complicated structures, quantitative time factors and even stochastic behaviors. In this work, we present a model checker to analyze hierarchical probabilistic real-time systems. A modeling language called PRTS is used to specify such systems, and automatic zone-abstraction approach, which is probability preserving, is used to generate finite state MDP. We have implemented PRTS in model checking framework PAT so that friendly user interface can be used to edit, simulate and verify PRTS models. Some experiments are conducted to show our tool’s efficiency.

Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. We first carried out a number of experiments on different planning tools in order to compare their performance and …

Xgrid And R: Parallel Distributed Processing Using Heterogeneous Groups Of Apple Computers, Sarah C. Anoke, Yuting Zhao, Rafael Jaeger, Nicholas J. Horton

The R Journal

The Apple Xgrid system provides access to groups (or grids) of computers that can be used to facilitate parallel processing. We describe the xgrid package which facilitates access to this system to undertake independent simulations or other long-running jobs that can be divided into replicate runs within R. Detailed examples are provided to demonstrate the interface, along with results from a simulation study of the performance gains using a variety of grids. Use of the grid for “embarassingly parallel” independent jobs has the potential for major speedups in time to completion. Appendices provide guidance on setting up the workflow, utilizing …

The R Journal (June 2012) 4(1): Complete Issue, The R Foundation

The R Journal

Contributed Research Articles

Analysing Seasonal Data, Adrian G. Barnett, Peter Baker, and Annette J. Dobson

MARSS: Multivariate Autoregressive State-space Models for Analyzing Time-series Data, Elizabeth E. Holmes, Eric J. Ward, and Kellie Wills

openair: Data Analysis Tools for the Air Quality Community, Karl Ropkins and David C. Carslaw

Foreign Library Interface, Daniel Adler

Vdgraph: A Package for Creating Variance Dispersion Graphs, John Lawson

xgrid and R: Parallel Distributed Processing Using Heterogeneous Groups of Apple Computers, Sarah C. Anoke, Yuting Zhao, Rafael Jaeger, and Nicholas J. Horton

maxent: An R Package for Low-memory Multinomial Logistic Regression with Support for Semi-automated Text …

Foreign Library Interface, Daniel Adler

The R Journal

We present an improved Foreign Function Interface (FFI) for R to call arbitary native functions without the need for C wrapper code. Further we discuss a dynamic linkage framework for binding standard C libraries to R across platforms using a universal type information format. The package rdyncall comprises the framework and an initial repository of cross platform bindings for standard libraries such as (legacy and modern) OpenGL, the family of SDL libraries and Expat. The package enables system level programming using the R language; sample applications are given in the article. We out line the underlying automation tool-chain that extracts …

Marss: Multivariate Autoregressive State-Space Models For Analyzing Time-Series Data, Elizabeth E. Holmes, Eric J. Ward, Kellie Wills

The R Journal

MARSS is a package for fitting multivariate autoregressive state-space models to time-series data. The MARSS package implements state-space models in a maximum likelihood framework. The core functionality of MARSSis based on likelihood maximization using the Kalman filter/smoother, combined with an EM algorithm. To make comparisons with other packages available, parameter estimation is also permitted via direct search routines avail able in ’optim’. The MARSS package allows data to contain missing values and allows a wide variety of model structures and constraints to be specified (such as fixed or shared parameters). In addition to model-fitting, the package provides bootstrap routines for …

Who Did What? The Roles Of R Package Authors And How To Refer To Them, Kurt Hornik, Duncan Murdoch, Achim Zeileis

The R Journal

Computational infrastructure for rep resenting persons and citations has been avail able in R for several years, but has been restructured through enhanced classes "person" and "bibentry" in recent versions of R. The new features include support for the specification of the roles of package authors (e.g. maintainer, author, contributor, translator, etc.) and more flexible formatting/printing tools among various other improvements. Here, we introduce the new classes and their methods and indicate how this functionality is employed in the management of R packages. Specifically, we show how the authors of R packages can be specified along with their roles in …

Maxent: An R Package For Low-Memory Multinomial Logistic Regression With Support For Semi-Automated Text Classification, Timothy P. Jurka

The R Journal

maxent is a package with tools for data classification using multinomial logistic regression, also known as maximum entropy. The focus of this maximum entropy classifier is to minimize memory consumption on very large datasets, particularly sparse document-term matrices represented by the tm text mining pack age.

Sumo: An Authenticating Web Application With An Embedded R Session, Timothy T. Bergsma, Michael S. Smith

The R Journal

Sumo is a web application intended as a template for developers. It is distributed as a Java ‘war’ file that deploys automatically when placed in a Servlet container’s ‘webapps’ directory. If a user supplies proper credentials, Sumocreates a session-specific Secure Shell connection to the host and a user-specific R session over that connection. Developers may write dynamic server pages that make use of the persistent R session and user-specific file space. The supplied example plots a data set conditional on preferences indicated by the user; it also displays some static text. A companion server page al lows the user to …

Analysing Seasonal Data, Adrian G. Barnett, Peter Baker, Annette J. Dobson

The R Journal

Many common diseases, such as the flu and cardiovascular disease, increase markedly in winter and dip in summer. These seasonal patterns have been part of life for millennia and were first noted in ancient Greece by both Hippocrates and Herodotus. Recent interest has focused on climate change, and the concern that seasons will become more extreme with harsher winter and summer weather. We describe a set of R functions designed to model seasonal pat terns in disease. We illustrate some simple descriptive and graphical methods, a more complex method that is able to model non-stationary patterns, and the case-crossover to …

Vdgraph: A Package For Creating Variance Dispersion Graphs, John Lawson

The R Journal

This article introduces the package Vdgraph that is used form a king variance dispersion graphs of response surface designs.The package includes functions that make the variance dispersion graph of one design or compare variance dispersion graphs of two designs, which are stored in data frames or matrices.The package also contains several minimum run response surface designs (stored as matrices) that are not available in other R packages.

Openair: Data Analysis Tools For The Air Quality Community, Karl Ropkins, David C. Carslaw

The R Journal

The openair package contains data analysis tools for the air quality community. This paper provides an overview of data importers, main functions, and selected utilities and workhorse functions within the package and the function output class, as of package version 0.4-14. It is intended as an explanation of the rationale for the package and a technical description for those wishing to work more inter actively with the main functions or develop additional functions to support ‘higher level’ use of openair and R.

Aligning Images In The Wild, Wen-Yan Lin, Linlin Liu, Yasuyuki Matsushita, Kok-Lim Low, Siying Liu

Research Collection School Of Computing and Information Systems

Aligning image pairs with significant appearance change is a long standing computer vision challenge. Much of this problem stems from the local patch descriptors’ instability to appearance variation. In this paper we suggest this instability is due less to descriptor corruption and more the difficulty in utilizing local information to canonically define the orientation (scale and rotation) at which a patch’s descriptor should be computed. We address this issue by jointly estimating correspondence and relative patch orientation, within a hierarchical algorithm that utilizes a smoothly varying parameterization of geometric transformations. By collectively estimating the correspondence and orientation of all the …

Complexity Of The Soundness Problem Of Bounded Workflow Nets, Guan Jun Liu, Jun Sun, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Classical workflow nets (WF-nets) are an important class of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property that guarantees these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable, and proposed (but not proved) that the soundness problem is EXPSPACE-hard. In this paper, we show that the satisfiability problem of Boolean expression is polynomial time reducible to the liveness problem of bounded WF-nets, and soundness and liveness are equivalent for bounded WF-nets. As a result, the soundness problem of bounded WF-nets is co-NP-hard.Workflow nets with …