Computer Sciences Commons^™

Detecting Malicious Javascript, Matthew F. Der

Honors Theses

The increased use of the World Wide Web and JavaScript as a scripting language for Web pages have made JavaScript a popular attack vector for infecting users' machines with malware. Additionally, attackers often obfuscate their code to avoid detection, which heightens the challenge and complexity of automated defense systems. We present two analyses of malicious scripts and suggest how they could be extended into intrusion detection systems. For our analyses we use a sample of deobfuscated malicious and benign scripts collected from actual Web sites. First, using our malicious sample, we perform a manual analysis of attack signatures, identifying four …

A Verification System For Interval-Based Specification Languages, Chunqing Chen, Jin Song Dong, Jun Sun, Andrew P. Martin

Research Collection School Of Computing and Information Systems

Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification …

Creating An Immersive Game World With Evolutionary Fuzzy Cognitive Maps, Yundong Cai, Ah-Hwee Tan, Zhiqi Shen, Boyang Li

Research Collection School Of Computing and Information Systems

An increasing number of serious games have been developed to enhance the user experiences in education and training. In order to bridge the gap of game experiences in the virtual environment and in the real life, it is crucial to generate believable characters and contexts in real-time. However, the variables to be simulated for a large-scale serious game are numerous. These variables are involved in complex causal relationships and their values change over time. In view that world modeling has not been well addressed with conventional models, this paper uses a computational model Evolutionary Fuzzy Cognitive Map (EFCM) to model …

Design Of A Software Framework Prototype For Scientific Model Interoperability, Eric Fritzinger, Sohei Okamoto

2010 Annual Nevada NSF EPSCoR Climate Change Conference

19 PowerPoint slides Session 2: Infrastructure Convener: Sergiu Dascalu, UNR Abstract: -What are models? -Mathematical models used to describe a system -E.g. Atmospheric, Oceanic, Ecological, etc… -Algorithmic calculations which take input and produce estimated results -Weather forecasting, global warming predictions, sea level estimations, etc… -Models are invaluable

Analysis Of Xbrl Literature: A Decade Of Progress And Puzzle, Saeed Roohani, Zhao Xianming, Ernest Capozzoli, Barbara Lamberton

Faculty Articles

XBRL (eXtensible Business Reporting language) was recently, in 2008, in its 10th year. The concept was articulated in 1998 by Charles Hoffman, known as XFRML (eXtensible Financial Reporting Mark Up Language) to facilitate the business reporting process and improve financial reporting. The objective of this paper is to examine a decade (1998-2008) of XBRL articles published in various publications including trade, practitioner and academic journals to identify trends and patterns, milestones, and organizations actively contributed to this development. Another goal is to assess public perceptions of XBRL, its capabilities and its future. We examined published articles where XBRL appeared either …

High School Microsoft Powerpoint, Ladane Du Boulay

Technology

The purpose of this lesson is for students to deepend and demonstrate their understanding of Powerpoint. The students will create a sample multimedia-rich presentation. They will be using their prior knowledge related to their social studies (i.e. Abraham Lincoln) and Science (i.e. Charles Darwin) classes.

Using Python To Program Lego Mindstorms Robots: The Pynxc Project, Brian S. Blais

Science and Technology Department Faculty Journal Articles

LEGO MINDSTORMS® NXT (Lego Group, 2006) is a perfect platform for introducing programming concepts, and is generally targeted toward children from age 8-14. The language which ships with the MINDSTORMS®, called NXTg, is a graphical language based on LabVIEW (Jeff Kodosky, 2010). Although there is much value in graphical languages, such as LabVIEW, a text-based alternative can be targeted at an older audiences and serve as part of a more general introduction to modern computing. Other languages, such as NXC (Not Exactly C) (Hansen, 2010) and PbLua (Hempel, 2010), fit this description. Here we introduce PyNXC, a subset of the …

Optimal Cryptographic Hardness Of Learning Monotone Functions, Dana Dachman-Soled, Homin K. Lee, Tal Malkin, Rocco A. Servedio, Andrew Wan, Hoeteck Wee

Publications and Research

Over the years a range of positive algorithmic results have been obtained for learning various classes of monotone Boolean functions from uniformly distributed random examples. Prior to our work, however, the only negative result for learning monotone functions in this model has been an information-theoretic lower bound showing that certain super-polynomial-size monotone circuits cannot be learned to accuracy 1/2+w(log n/ p n) (Blum, Burch, and Langford, FOCS’98). This is in contrast with the situation for nonmonotone functions, where a wide range of cryptographic hardness results establish that various “simple” classes of polynomial-size circuits are not learnable by polynomial-time algorithms.

In …

Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an on-the-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT …

Sos: Searching Help Pages Of R Packages, Spencer Graves, Sundar Dorai-Raj, Romain François

The R Journal

The sos package provides a means to quickly and flexibly search the help pages of contributed packages, finding functions and datasets in seconds or minutes that could not be found in hours or days by any other means we know. Its findFn function accesses Jonathan Baron’s R Site Search database and returns the matches in a data frame of class "findFn", which can be further manipulated by other sos functions to produce, for example, an Excel file that starts with a summary sheet that makes it relatively easy to prioritize alternative packages for further study. As such, it provides a …

Rattle: A Data Mining Gui For R, Graham J. Williams

The R Journal

Data mining delivers insights, pat terns, and descriptive and predictive models from the large amounts of data available today in many organisations. The data miner draws heavily on methodologies, techniques and algorithms from statistics, machine learning, and computer science. R increasingly provides a powerful platform for data mining. However, scripting and programming is sometimes a challenge for data analysts moving into data mining. The Rattle package provides a graphical user interface specifically for data mining using R. It also provides a stepping stone toward using R as a programming language for data analysis.

Copas: An R Package For Fitting The Copas Selection Model, J. Carpenter, G. Rücker, G. Schhwarzer

The R Journal

This article describes the R package copas which is an add-on package to the R pack age meta. The R package copas can be used to f it the Copas selection model to adjust for bias in meta-analysis. A clinical example is used to illustrate fitting and interpreting the Copas selection model.

Party On!, Carolin Strobl, Torsten Hothorn, Achim Zeileis

The R Journal

Random forests are one of the most popular statistical learning algorithms, and a variety of methods for fitting random forests and related recursive partitioning approaches is available in R. This paper points out two important features of the random forest implementation cforest available in the party package: The resulting forests are unbiased and thus prefer able to the randomForest implementation avail able in randomForest if predictor variables are of different types. Moreover, a conditional per mutation importance measure has recently been added to the party package, which can help evaluate the importance of correlated predictor variables. The rationale of this …

Aspects Of The Social Organization And Trajectory Of The R Project, John Fox

The R Journal

Based partly on interviews with members of the R Core team, this paper considers the development of the R Project in the context of open-source software development and, more generally, voluntary activities. The paper de scribes aspects of the social organization of the R Project, including the organization of the R Core team; describes the trajectory of the R Project; seeks to identify factors crucial to the success of R; and speculates about the prospects for R.

Asymptest: A Simple R Package For Classical Parametric Statistical Tests And Confidence Intervals In Large Samples, J.-F. Coeurjolly, R. Drouilhet, P. Lafaye De Micheaux, J.-F. Robineau

The R Journal

asympTest is an R package implementing large sample tests and confidence intervals. One and two sample mean and variance tests (differences and ratios) are considered. The test statistics are all expressed in the same form as the Student t-test, which facilitates their presentation in the classroom. This contribution also fills the gap of a robust (to non-normality) alternative to the chi-square single variance test for large samples, since no such procedure is implemented in standard statistical software.

Convergenceconcepts: An R Package To Investigate Various Modes Of Convergence, Pierre Lafaye De Micheaux, Benoit Liquet

The R Journal

ConvergenceConcepts is an R pack age, built upon the tkrplot, tcltk and lattice packages, designed to investigate the convergence of simulated sequences of random variables. Four classical modes of convergence may be studied, namely: almost sure convergence (a.s.), convergence in probability (P), convergence in law (L) and convergence in r-th mean (r). This investigation is performed through ac curate graphical representations. This package may be used as a pedagogical tool. It may give students a better understanding of these notions and help them to visualize these difficult theoretical concepts. Moreover, …

Automation In Cs1 With The Factoring Problem Generator, Joshua B. Parker

Master's Theses

As the field of computer science continues to grow, the number of students enrolled in related programs will grow as well. Though one-on-one tutoring is one of the more effective means of teaching, computer science instructors will have less and less time to devote to individual students. To address this growing concern, many tools that automate parts of an instructor’s job have been proposed. These tools can assist instructors in presenting concepts and grading student work, and they can help students learn to program more effectively. A growing group of intelligent tutoring systems attempts to tie all of this functionality …

The R Journal (December 2009) 1(2): Complete Issue, The R Foundation

The R Journal

Contributed Research Articles

Aspects of the Social Organization and Trajectory of the R Project, John Fox

Party on! Carolin Strobl, Torsten Hothorn and Achim Zeileis

ConvergenceConcepts: An R Package to Investigate Various Modes of Convergence, Pierre Lafaye de Micheaux and Benoit Liquet

asympTest: A Simple R Package for Classical Parametric Statistical Tests and Confidence Intervals in Large Samples, J.-F. Coeurjolly, R. Drouilhet, P. Lafaye de Micheaux and J.-F. Robineau

copas: An R package for Fitting the Copas Selection Model, J. Carpenter, G. Rücker and G. Schwarzer

Transitioning to R: Replicating SAS, Stata, and SUDAAN Analysis Techniques in Health Policy Data, …

Object Oriented Program Correctness With Oosiml, José M. Garrido

Faculty Articles

Software reliability depends on program correctness and robustness and these are extremely important in developing high-quality software. Correctness is also essential when considering aspects of software security. However, experience applying these concepts, associated methods, and supporting software with Eiffel and Java have shown that students find some diffculty learning program correctness and in learning the software tools provided. We have developed an experimental language, OOSimL, that includes an assertion notation similar to that of Eiffel but which has much more flexibility, and that provides the same semantics as Java.

The first part of this paper provides an overview of concepts …

A Gis Hub At Pace University, Peggy Minis, Hsui-Lin Winkler

Cornerstone 2 Reports : Community Outreach and Empowerment Through Service Learning and Volunteerism

The Thinkfinity Grant is to use technology to develop a GIS Hub at Pace University. The Hub is intended to show the larger community the work done at Pace and to show that our students and faculty are using GIS to solve geographically-based problems for communities and organizations. It also is intended to serve as a site from which users can download data to make their own maps and as a place where the larger community can find examples of maps and have the ability to manipulate maps.

Pointcut Rejuvenation: Recovering Pointcut Expressions In Evolving Aspect-Oriented Software, Raffi Khatchadourian, Phil Greenwood, Awais Rashid, Guoqing Harry Xu

Publications and Research

Pointcut fragility is a well-documented problem in Aspect-Oriented Programming; changes to the base-code can lead to join points incorrectly falling in or out of the scope of pointcuts. We present an automated approach that limits fragility problems by providing mechanical assistance in pointcut maintenance. The approach is based on harnessing arbitrarily deep structural commonalities between program elements corresponding to join points selected by a pointcut. The extracted patterns are then applied to later versions to offer suggestions of new join points that may require inclusion. We demonstrate the usefulness of our technique by rejuvenating pointcuts in multiple versions of several …

Unplanned Maintenance Scheduling A Lean Application Using Group Technology And Adaptive Conflict Resolution, Manish Shashibhushan Mittal

Mechanical & Aerospace Engineering Theses & Dissertations

Historically, production of ships is based on Group Technology (GT) with product oriented work breakdown structure. Recent GT applications have been effectively adapted to ship maintenance operations. In this thesis we have developed a GT based classification and coding system for the three basic requirements for maintenance operations: personnel, resources and space.

Traditionally unplanned maintenance activities are executed as and when the resources are available. This thesis presents a method for planning and scheduling these jobs with many of the traditional Lean manufacturing principles first adapted appropriately and then applied to Lean Maintenance. This method begins with identifying the priority …

Contributing Factors To Pointcut Fragility, Phil Greenwood, Awais Rashid, Raffi Khatchadourian

Publications and Research

Pointcut fragility is a well-documented problem of Aspect-Oriented Programming with changes to the base-code causing join points to incorrectly fall in or out of scope. In order to combat this problem a tool was developed that provides mechanical assistance to pointcut maintenance. This tool relied on the deep structural commonalities between program elements to detect when pointcut fragility occurs. During the assessment of this tool a number of common practices were uncovered that were employed both in the aspect and base-code that contributed to or prevented pointcut fragility. This paper documents the practices uncovered and describes how they can affect …

Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang

Research Collection School Of Computing and Information Systems

In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …

Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen

Research Collection School Of Computing and Information Systems

High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level …

Freedom Of Choice As A Motivational Factor In Active Learning, Atanas Radenski

Mathematics, Physics, and Computer Science Faculty Articles and Research

Freedom to choose what, when, and how to contribute in a learning process can motivate students to actively engage and achieve more in their studies. However, freedom of choice complicates course management and may deter instructors from allowing such freedom. Our approach is to utilize existing functionality of course management systems such as Moodle to automatically facilitate and coordinate free student choices and provide much needed relief for instructors at the same time. Using Moodle we have developed novel digital study packs that blend freedom of choice with guidance and control. Our survey shows that assisted freedom of choice is …

Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao

Research Collection School Of Computing and Information Systems

The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing population protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for …

Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

System modeling is important and highly non-trivial. The choice of specification language is an important factor in the success of the entire development. The language should cover several facets of the requirements and the model should precisely capture (up to abstraction of irrelevant details) an existing system or a system to be built. The language should have a semantic model suitable to study the behaviors of the system and to establish the validity of desired properties. A formal model can be the basis for a variety of system development activities, e.g., system simulation, visualization, verification or prototype synthesis.

Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process …

Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent …