Computer Sciences Commons^™

Formal Modeling And Validation Of Stateflow Diagrams, Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong, Manchun Zheng

Research Collection School Of Computing and Information Systems

Stateflow is an industrial tool for modeling and simulating control systems in model-based development. In this paper, we present our latest work on automatic verification of Stateflow using model-checking techniques. We propose an approach to systematically translate Stateflow diagrams to a formal modeling language called CSP# by precisely following Stateflow’s execution semantics, which is described by examples. A translator is developed inside the Process Analysis Toolkit (PAT) model checker to automate this process with the support of various Stateflow advanced modeling features. Formal analysis can be conducted on the transformed CSP# with PAT’s simulation and model-checking power. Using our approach, …

How Is M&S Interoperability Different From Other Interoperability Domains?, Andreas Tolk, Saikou Y. Diallo, Jose J. Padilla, Charles D. Turnitsa

Computational Modeling & Simulation Engineering Faculty Publications

During every standard workshop or event, the examples of working interoperability solutions are used to motivate for 'plug and play' standards for M&S as well, like standardized batteries for electronics, or the use of XML to exchange data between heterogeneous systems. While these are successful applications of standards, they are off the mark regarding M&S interoperability. The challenge of M&S is that the product that needs to be made interoperable is not the service or the system alone, but the model behind it as well. The paper shows that the alignment of conceptualizations is the real problem that is not …

Patterns As Objects In Grace, Andrew P. Black, Michael Homer, James Noble, David J. Pearce, Kim B. Bruce

Computer Science Faculty Publications and Presentations

Object orientation and pattern matching are often seen as conflicting approaches to program design. Object oriented programs place type-dependent behaviour inside objects and invoke it via dynamic dispatch, while pattern matching programs place type-dependent behaviour outside data structures and invoke it via multiway conditionals (case statements). Grace is a new, dynamic, object-oriented language designed to support teaching: to this end, Grace needs to support both styles. In this paper we explain how this conflict can be resolved gracefully: by modelling patterns and cases as partial functions, reifying those functions as first-class objects, and then building up complex patterns from simpler …

Parallel Sorting On A Spatial Computer, Max Orhai, Andrew P. Black

Computer Science Faculty Publications and Presentations

We describe a parallel sort for a spatial computer that requires minimal communication. We show simulations of the sort in 1 and 2 dimensions.

Presentation slides are located below in the Additional Files

Fusion Of Visual And Thermal Images Using Genetic Algorithms, Sertan Erkanli, Jiang Li, Ender Oguslu, Shangce Gao (Ed.)

Electrical & Computer Engineering Faculty Publications

No abstract provided.

The Basic Scheme For The Evaluation Of Functional Logic Programs, Arthur Peters

Dissertations and Theses

Functional logic languages provide a powerful programming paradigm combining the features of functional languages and logic languages. However, current implementations of functional logic languages are complex, slow, or both. This thesis presents a scheme, called the Basic Scheme, for compiling and executing functional logic languages based on non-deterministic graph rewriting. This thesis also describes the implementation and optimization of a prototype of the Basic Scheme. The prototype is simple and performs well compared to other current implementations.

A Hybridized Lagrangian Relaxation And Simulated Annealing Method For The Course Timetabling Problem, Aldy Gunawan, Kim Leng Poh

Research Collection School Of Computing and Information Systems

This paper describes a timetabling problem at universities, where a master course timetable is given extrinsically and conflicts due to students' course enrollment do not need to be considered. A solver for the problem, which integrates both teacher assignment and course scheduling, is described. An initial solution is obtained by a mathematical programming approach based on Lagrangian relaxation. This solution is further improved by a simulated annealing algorithm. The proposed method has been tested on instances from a university in Indonesia, as well as on several randomly generated datasets, and the corresponding computational results are reported.

The R Journal (December 2011) 3(2): Complete Issue, The R Foundation

The R Journal

Contributed Research Articles

Creating and Deploying an Application with (R)Excel and R, Thomas Baier, Erich Neuwirth, and Michele De Meo

glm2: Fitting Generalized Linear Models with Convergence Problems, Ian C. Marschner

Implementing the Compendium Concept with Sweave and DOCSTRIP, Michael Lundholm

Watch Your Spelling! Kurt Hornik and Duncan Murdoch

Ckmeans.1d.dp: Optimal k-means Clustering in One Dimension by Dynamic Programming, Haizhou Wang and Mingzhou Song

Nonparametric Goodness-of-Fit Tests for Discrete Null Distributions, Taylor B. Arnold and John W. Emerson

Using the Google Visualisation API with R, Markus Gesmann and Diego de Castillo

GrapheR: a Multiplatform GUI for Drawing Customizable Graphs in …

Rainbow: An R Package For Visualizing Functional Time Series, Han Lin Shang

The R Journal

Recent advances in computer technology have tremendously increased the use of functional data, whose graphical representation can be infinite-dimensional curves, images or shapes. This article describes four methods for visualizing functional time series using an R add-on package. These methods are demonstrated using age-specific Australian fertility data from 1921 to 2006 and monthly sea surface temperatures from January 1950 to December 2006.

Using The Google Visualisation Api With R, Markus Gesmann, Diego De Castillo

The R Journal

The googleVis package provides an interface between R and the Google Visualisation API to create interactive charts which can be embedded into web pages. The best known of these charts is probably the Motion Chart, popularised by Hans Rosling in his TED talks. With the googleVis package users can easily create web pages with interactive charts based on R data frames and display them either via the local R HTTPhelp server or within their own sites.

Ckmeans.1d.Dp: Optimal K-Means Clustering In One Dimension By Dynamic Programming, Haizhou Wang, Mingzhou Song

The R Journal

The heuristic k-means algorithm, widely used for cluster analysis, does not guarantee optimality. We developed a dynamic programming algorithm for optimal one-dimensional clustering. The algorithm is implemented as an R package called Ckmeans.1d.dp. We demonstrate its ad vantage in optimality and runtime over the standard iterative k-means algorithm.

Implementing The Compendium Concept With Sweave And Docstrip, Michael Lundholm

The R Journal

This article suggests an implementation of the compendium concept by combining Sweave and the LATEX literate programming environment DOCSTRIP.

Content-Based Social Network Analysis Of Mailing Lists, Angela Bohn, Ingo Feinerer, Kurt Hornik, Patrick Mair

The R Journal

Social Network Analysis (SNA) provides tools to examine relationships between people. Text Mining (TM) allows capturing the text they produce in Web 2.0 applications, for example, however it neglects their social structure. This paper applies an approach to combine the two methods named “content-based SNA”. Using the R mailing lists, R-help and R-devel, we show how this combination can be used to describe people’s interests and to find out if authors who have similar interests actually communicate. We find that the expected positive relationship between sharing interests and communicating gets stronger as the centrality scores of authors in the communication …

Watch Your Spelling!, Kurt Hornik, Duncan Murdoch

The R Journal

We discuss the facilities in base R for spell checking via Aspell, Hunspell or Ispell, which are useful in particular for conveniently checking the spelling of natural language texts in package Rd files and vignettes. Spell checking performance is illustrated using the Rd files in package stats. This example clearly indicates the need for a domain-specific statistical dictionary. We analyze the results of spell checking all Rd files in all CRAN packages and show how these can be employed for building such a dictionary.

Nonparametric Goodness-Of-Fit Tests For Discrete Null Distributions, Taylor B. Arnold, John W. Emerson

The R Journal

Methodology extending nonparametric goodness-of-fit tests to discrete null distributions has existed for several decades. However, modern statistical software has generally failed to provide this methodology to users. We offer a revision of R’s ks.test() function and a new cvm.test() function that fill this need in the R language for two of the most popular nonparametric goodness-of-fit tests. This paper describes these contributions and provides examples of their usage. Particular attention is given to various numerical issues that arise in their implementation.

Portable C++ For R Packages, Martyn Plummer

The R Journal

Package checking errors are more common on Solaris than Linux. In many cases, these errors are due to non-portable C++ code. This article reviews some commonly recurring problems in C++ code found in R packages and suggests solutions.

Glm2: Fitting Generalized Linear Models With Convergence Problems, Ian C. Marschner

The R Journal

The R function glm uses step-halving to deal with certain types of convergence problems when using iteratively reweighted least squares to fit a generalized linear model. This works well in some circumstances but non-convergence remains a possibility, particularly with a non standard link function. In some cases this is be cause step-halving is never invoked, despite a lack of convergence. In other cases step-halving is invoked but is unable to induce convergence. One remedy is to impose a stricter form of step halving than is currently available in glm, so that the deviance is forced to decrease in every iteration. …

Creating And Deploying An Application With (R)Excel And R, Thomas Baier, Erich Neuwirth, Michele De Meo

The R Journal

We present some ways of using R in Excel and build an example application using the package rpart. Starting with simple interactive use of rpart in Excel, we eventually package the code into an Excel-based application, hiding all details (including R itself) from the end user. In the end, our application implements a service oriented architecture (SOA) with a clean separation of presentation and computation layer

Grapher: A Multiplatform Gui For Drawing Customizable Graphs In R, Maxime Hervé

The R Journal

This article presents GrapheR, a Graphical User Interface allowing the user to draw customizable and high-quality graphs without knowing any R commands. Six kinds of graph are available: histograms, box-and-whisker plots, bar plots, pie charts, curves and scatter plots. The complete process is described with the examples of a bar plot and a scatter plot illustrating the legendary puzzle of African and European swallows’ migrations.

Processj: A Process-Oriented Programming Language, Matthew Sowders

UNLV Theses, Dissertations, Professional Papers, and Capstones

Java is a general purpose object-oriented programming language that has been widely adopted. Because of its high adoption rate and its lineage as a C-style language, its syntax is familiar to many programmers. The downside is that Java is not natively concurrent. Volumes have been written about concurrent programming in Java; however, concurrent programming is difficult to reason about within an object-oriented paradigm and so is difficult to get right.

occam -π is a general purpose process-oriented programming language. Concurrency is part of the theoretical underpinnings of the language. Concurrency is simple to reason about within an occam -π application …

Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li

Research Collection School Of Computing and Information Systems

Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We …

Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu

Research Collection School Of Computing and Information Systems

Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled …

Houdini's Wxpython, Michael Moore

Senior Seminars

This paper shows the importance of Python in Houdini. It goes into how and why Python is so important in Houdini. We see how we can build tools in Python that can be invaluable in the making of 3d animations in Houdini. Through building tools that help Houdini the programmer needs a way to build a GUI application. In building a GUI application we used wxWidget. Showing what wxWidget and how it can be used in Python. Then showing the strengths of wxWidget we compared it to Python's built in GUI application builder Tkinter, and from there showed how wxPython …

Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …

An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu

Research Collection School Of Computing and Information Systems

In inference of untimed regular languages, given an unknown language to be inferred, an automaton is constructed to accept the unknown language from answers to a set of membership queries each of which asks whether a string is contained in the unknown language. One of the most well-known regular inference algorithms is the L* algorithm, proposed by Angluin in 1987, which can learn a minimal deterministic finite automaton (DFA) to accept the unknown language. In this work, we propose an efficient polynomial time learning algorithm, TL*, for timed regular language accepted by event-recording automata. Given an unknown timed regular language, …

Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan

Research Collection School Of Computing and Information Systems

Topology-based multi-agent systems (TMAS), wherein agents interact with one another according to their spatial relationship in a network, are well suited for problems with topological constraints. In a TMAS system, however, each agent may have a different state space, which can be rather large. Consequently, traditional approaches to multi-agent cooperative learning may not be able to scale up with the complexity of the network topology. In this paper, we propose a cooperative learning strategy, under which autonomous agents are assembled in a binary tree formation (BTF). By constraining the interaction between agents, we effectively unify the state space of individual …

Architecture For A Flexible And Scalable Simulation Engine, Robert C. Holcomb Jr.

Computational Modeling & Simulation Engineering Theses & Dissertations

Simulation is used by many different industries to gain insight on actions and decisions that may be too dangerous or costly to perform in reality. Although the use of computers to assist with modeling and simulation has been studied for quite a while, computer infrastructure, hardware, and capabilities are changing at a rapid pace. Computer software once written is difficult and costly to change, especially in order to take advantage of the advances in computer hardware. This thesis focuses on the design and implementation of a software simulation architecture that allows flexibility in the modeling conducted and scalability in the …

Amibe: An Imperative Programming Language With First Class Continuations, Yuting Wang

Master's Theses

A continuation represents the future of an execution. It is often used as an intermediate representation(IR) to compile functional programming languages, make control flow explicit and full beta-reduction(function inlining) possible. Continuations are also a language feature that gives user the ability to completely control the execution control flow(first class continuation). Efficient implementation of first class continuation is important for languages that need non-determinism and backtracking(e.g., COMET). We present a prototype imperative programming language with first class continuation -- AMIBE. AMIBE uses the LLVM compiler infrastructure which is attractive for its optimizing tools and overall modern organization. However, LLVM does not …

Roaming Region For Delaunay Triangulation, Romas James Hada

UNLV Theses, Dissertations, Professional Papers, and Capstones

Delaunay graphs have been used in CAD/CAM, sensor network and geographic information systems. We investigate the reliability properties of nodes in Delaunay graphs. For measuring the reliability we formulate the concept of roaming-region for nodes. A node v with large roaming-region r(v) such that v is positioned near the center of r(v) is identified as a reliable node. We develop algorithms for constructing roaming-regions and present an implementation of the proposed algorithm in the Java programming language.

Automatic Content Generation For Video Self Modeling, Ju Shen, Anusha Raghunathan, Sen-Ching S. Cheung, Ravi R. Patel

Computer Science Faculty Publications

Video self modeling (VSM) is a behavioral intervention technique in which a learner models a target behavior by watching a video of him or herself. Its effectiveness in rehabilitation and education has been repeatedly demonstrated but technical challenges remain in creating video contents that depict previously unseen behaviors. In this paper, we propose a novel system that re-renders new talking-head sequences suitable to be used for VSM treatment of patients with voice disorder. After the raw footage is captured, a new speech track is either synthesized using text-to-speech or selected based on voice similarity from a database of clean speeches. …