Programming Languages and Compilers Commons^™

Symbolic Model-Checking Of Stateful Timed Csp Using Bdd And Digitization, Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Stateful Timed CSP has been recently proposed to model (and verify) hierarchical real-time systems. It is an expressive modeling language which combines data structure/operations, complicated control flows (modeled using compositional process operators adopted from Timed CSP), and real-time requirements like deadline and within. It has been shown that Stateful Timed CSP is equivalent to closed timed automata with silent transitions, which implies that the timing constraints of Stateful Timed CSP can be captured using explicit tick events, through digitization. In order to tackle the state space explosion problem, we develop a BDD-based symbolic model checking approach to verify Stateful Timed …

Dependently Typed Programming With Singletons, Richard A. Eisenberg, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas are in- spired by dependently typed programs, the code looks significantly different. As a result, GHC implementors have responded with ex- tensions to Haskell’s type system, such as GADTs, type families, and datatype promotion. However, there remains a significant dif- ference between programming in Haskell and in full-spectrum de- pendently typed languages. Haskell enforces a phase separation be- tween runtime values …

The R Journal (December 2012) 4(2): Complete Issue, The R Foundation

The R Journal

Contributing Articles

What's in a Name? Paul Murrell

It's Not What You Draw, It's What You Don't Draw, Paul Murrell

Debugging grid Graphics, Paul Murrell and Velvet Ly

frailtyHL: A Package for Fitting Frailty Models with H-likelihood, Il Do Ha, Maengseok Noh, and Youngjo Lee

influence.ME: Tools for Detecting Influential Data in Mixed Effects Models, Rense Nieuwenhuis, Manfred te Grotenhuis and Ben Pelzer

The crs Package: Nonparametric Regression Splines for Continuous and Categorical Predictors, Zhenghua Nie and Jeffrey S. Racine

Rfit: Rank-based Estimation for Linear Models, John D. Kloke and Joseph W. McKean

Graphical Markov Models with Mixed Graphs in …

The Crs Package: Nonparametric Regression Splines For Continuous And Categorical Predictors, Zhenghua Nie, Jeffery S. Racine

The R Journal

A new package crs is introduced for computing nonparametric regression (and quantile) splines in the presence of both continuous and categorical predictors. B-splines are employed in the regression model for the continuous predictors and kernel weighting is employed for the categorical predictors. We also de velop a simple R interface to NOMAD, which is a mixed integer optimization solver used to compute optimal regression spline solutions.

Influence.Me: Tools For Detecting Influential Data In Mixed Effects Models, Rense Nieuwenhuis, Manfred Te Grotenhuis, Ben Pelzer

The R Journal

influence.ME provides tools for detecting influential data in mixed effects models. The application of these models has become common practice, but the development of diagnostic tools has lagged behind. influence.ME calculates standardized measures of influential data for the point estimates of generalized mixed effects models, such as DFBETAS, Cook’s distance, as well as percentile change and a test for changing levels of significance. influence.ME calculates these measures of influence while ac counting for the nesting structure of the data. The package and measures of influential data are introduced, a practical example is given, and strategies for dealing with influential data …

Graphical Markov Models With Mixed Graphs In R, Kayvan Sadeghi, Giovanni M. Marchetti

The R Journal

In this paper we provide a short tuto rial illustrating the new functions in the package ggm that deal with ancestral, summary and ribbonless graphs. These are mixed graphs (containing three types of edges) that are important because they capture the modified independence structure after marginalisation over, and conditioning on, nodes of directed acyclic graphs. We provide functions to verify whether a mixed graph implies that A is independent of B given C for any disjoint sets of nodes and to generate maximal graphs inducing the same independence structure of non-maximal graphs. Finally, we provide functions to decide on the …

What's In A Name?, Paul Murrell

The R Journal

Any shape that is drawn using the grid graphics package can have a name associated with it. If a name is provided, it is possible to access, query, and modify the shape after it has been drawn. These facilities allow for very detailed customisations of plots and also for very general transformations of plots that are drawn by packages based on grid.

Frailtyhl: A Package For Fitting Frailty Models With H-Likelihood, Il Do Ha, Maengseok Noh, Youngjo Lee

The R Journal

We present the frailtyHL package for fitting semi-parametric frailty models using h likelihood. This package allows lognormal or gamma frailties for random-effect distribution, and it fits shared or multilevel frailty models for correlated survival data. Functions are provided to format and summarize the frailtyHL results. The estimates of fixed effects and frailty parameters and their standard errors are calculated. We illustrate the use of our package with three well known data sets and compare our results with various alternative R-procedures.

Rfit: Rank-Based Estimation For Linear Models, John D. Kloke, Joseph W. Mckeen

The R Journal

In the nineteen seventies, Jureĉková and Jaeckel proposed rank estimation for linear models. Since that time, several authors have developed inference and diagnostic methods for these estimators. These rank-based estimators and their associated inference are highly efficient and are robust to outliers in response space. The methods include estimation of standard errors, tests of general linear hypotheses, confidence intervals, diagnostic procedures including studentized residuals, and measures of influential cases. We have developed an R package, Rfit, for computing of these robust procedures. In this paper we highlight the main features of the pack age. The package uses standard linear …

It's Not What You Draw, It's What You Don't Draw, Paul Murrell

The R Journal

The R graphics engine has new support for drawing complex paths via the functions polypath() and grid.path(). This article explains what is meant by a complex path and demonstrates the usefulness of complex paths in drawing non-trivial shapes, logos, customised data symbols, and maps.

Debugging Grid Graphics, Paul Murrell, Velvet Ly

The R Journal

A graphical scene that has been produced using the grid graphics package consists of grobs (graphical objects) and viewports. This article describes functions that allow the exploration and inspection of the grobs and viewports in a grid scene, including several functions that are available in a new package called gridDe bug. The ability to explore the grobs and view ports in a grid scene is useful for adding more drawing to a scene that was produced using grid and for understanding and debugging the grid code that produced a scene.

The State Of Naming Conventions In R, Rasmus Bååth

The R Journal

Most programming language communities have naming conventions that are generally agreed upon, that is, a set of rules that governs how functions and variables are named. This is not the case with R, and a review of unofficial style guides and naming convention us age on CRAN shows that a number of different naming conventions are currently in use. Some naming conventions are, however, more popular than others and as a newcomer to the R community or as a developer of a new package this could be useful to consider when choosing what naming convention to adopt.

Dynamic Data Race Detection And Healing, Du Li

School of Computing: Dissertations, Theses, and Student Research

Perpetual availability is an important operational goal in today's computer systems. However, achieving this goal is challenging because modern software systems contain faults that can cause them to fail. For example, multi-threading is widely used in modern software to fully utilize the computing capability of multicore processors. However, employing multi-threading can lead to concurrency faults such as deadlock and data race that are notoriously difficult to to isolate, detect, and repair.Data races, which involves two concurrent accesses to the same data where at least one is a write, are the most common concurrency faults.

As our first step, we investigate …

Effective Computer Programming Instruction For Pre-University Albanian Students, Robert Mccloud, Ardiana Sula

School of Computer Science & Engineering Faculty Publications

The relationship between pre-university students and technology is frequently overrated. While we receive glowing reports about how young people are knowledgeable about computers, the truth is that their knowledge is typically about computer content and the manipulation of applications. Young students too often treat the actual programming and understanding of computers as a sort of magical mystery.

In this paper we look at a new Albanian initiative to identify and nurture the most talented of our pre-university students. In particular we look at contributions to the goal of making Albanians the most talented programmers in this area of Europe.

The …

Fame, Soft Flock Formation Control For Collective Behavior Studies And Rapid Games Development, Choon Sing Ho, Yew-Soon Ong, Xianshun Chen, Ah-Hwee Tan

Research Collection School Of Computing and Information Systems

We present FAME, a comprehensive C# software library package providing soft formation control for large flocks of agents. While many existing available libraries provide means to create flocks of agent equipped with simple steering behavior, none so far, to the best of our knowledge, provides an easy and hassle free approach to control the formation of the flock. Here, besides the basic flocking mechanisms, FAME provides an extensive range of advanced features that gives enhanced soft formation control over multiple flocks. These soft formation features include defining flocks in any user-defined formation, automated self-organizing agent within formation, manipulating formation shape …

Automatic Generation Of Provably Correct Embedded Systems, Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

With the demand for new and complicated features, embedded systems are becoming more and more difficult to design and verify. Even if the design of a system is verified, how to guarantee the consistency between the design and its implementation remains a big issue. As a solution, we propose a framework that can help a system designer to model his or her embedded system using a high-level modeling language, verify the design of the system, and automatically generate executable software codes whose behavior semantics are consistent with that of the high-level model. We use two case studies to demonstrate the …

More Anti-Chain Based Refinement Checking, Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang, Shanping Li

Research Collection School Of Computing and Information Systems

Refinement checking plays an important role in system verification. It establishes properties of an implementation by showing a refinement relationship between the implementation and a specification. Recently, it has been shown that anti-chain based approaches increase the efficiency of trace refinement checking significantly. In this work, we study the problem of adopting anti-chain for stable failures refinement checking, failures-divergence refinement checking and probabilistic refine checking (i.e., a probabilistic implementation against a non-probabilistic specification). We show that the first two problems can be significantly improved, because the state space of the product model may be reduced dramatically. Though applying anti-chain for …

An Analytical And Experimental Comparison Of Csp Extensions And Tools, Ling Shi, Yang Liu, Jun Sun, Jin Song Dong, Gustavo Carvalho

Research Collection School Of Computing and Information Systems

Communicating Sequential Processes (CSP) has been widely applied to modeling and analyzing concurrent systems. There have been considerable efforts on enhancing CSP by taking data and other system aspects into account. For instance, CSP M combines CSP with a functional programming language whereas CSP# integrates high-level CSP-like process operators with low-level procedure code. Little work has been done to systematically compare these CSP extensions, which may have subtle and substantial differences. In this paper, we compare CSP M and CSP# not only on their syntax, but also operational semantics as well as their supporting tools such as FDR, ProB, and …

Neural Modeling Of Episodic Memory: Encoding, Retrieval, And Forgetting, Wenwen Wang, Budhitama Subagdja, Ah-Hwee Tan, Janusz A. Starzyk

Research Collection School Of Computing and Information Systems

This paper presents a neural model that learns episodic traces in response to a continuous stream of sensory input and feedback received from the environment. The proposed model, based on fusion Adaptive Resonance Theory (fusion ART) network, extracts key events and encodes spatio-temporal relations between events by creating cognitive nodes dynamically. The model further incorporates a novel memory search procedure, which performs parallel search of stored episodic traces continuously. Combined with a mechanism of gradual forgetting, the model is able to achieve a high level of memory performance and robustness, while controlling memory consumption over time. We present experimental studies, …

Scalable Content Authentication In H.264/Svc Videos Using Perceptual Hashing Based On Dempster-Shafer Theory, Dengpan Ye, Zhuo Wei, Xuhua Ding, Robert H. Deng

Research Collection School Of Computing and Information Systems

The content authenticity of the multimedia delivery is important issue with rapid development and widely used of multimedia technology. Till now many authentication solutions had been proposed, such as cryptology and watermarking based methods. However, in latest heterogeneous network the video stream transmission has b een coded in scalable way such as H.264/SVC, there is still no good authentication solution. In this paper, we firstly summarized related works and p roposed a scalable content authentication scheme using a ratio of different energy (RDE) based perceptual hashing in Q/S dimension, which is used Dempster-Shafer theory and combined with the latest scalable …

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.

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.

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 …

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 …

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 …

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 …