Computer Sciences Commons^™

Operational Verification Of A Relativistic Program, Robert T. Bauer

Computer Science Faculty Publications and Presentations

Engineering eorts to achieve scalable multiprocessor perfor- mance for concurrent reader-writer programs have resulted in a family of algorithms that are non-blocking and that tolerate interprocessor in- terference. Because these algorithms accept a unique frame of reference for each processor's accesses to memory, they typify a concurrent pro- gramming technique for shared memory multicore architectures called relativistic programmming.

Rigorous verification of these algorithms is not possible with existing semantic based approaches because the semantics under approximates multiprocessor behavior and the algorithms rely on abstruse interactions with the operating system that aren't reconciled with language seman- tics.

The Read-Copy Update (RCU) …

Sample Size Estimation While Controlling False Discovery Rate For Microarray Experiments Using The Ssize.Fdr Package, Megan Orr, Peng Liu

The R Journal

Microarray experiments are becoming more and more popular and critical in many biological disciplines. As in any statistical experiment, appropriate experimental design is essential for reliable statistical inference, and sample size has a crucial role in experimental design. Because microarray experiments are rather costly, it is important to have an adequate sample size that will achieve a desired power with out wasting resources.

For a given microarray data set, thousands of hypotheses, one for each gene, are simultaneously tested. Storey and Tibshirani (2003) argue that con trolling false discovery rate (FDR) is more reasonable and more powerful than controlling family-wise …

Emd: A Package For Empirical Mode Decomposition And Hilbert Spectrum, Donghoh Kim, Hee-Seok Oh

The R Journal

The concept of empirical mode decomposition (EMD)and the Hilber tspectrum (HS) has been developed rapidly in many disciplines of science and engineering since Huang et al. (1998) invented EMD. The key feature of EMD is to decompose a signal into so-called intrinsic mode function (IMF). Further more, the Hilbert spectral analysis of intrinsic mode functions provides frequency information evolving with time and quantifies the amount of variation due to oscillation at different time scales and time locations. In this article,we introduce an R package called EMD (KimandOh, 2008) that performs one and two-dimensional EMD and HS.

Modeling Without Data Using Expert Opinion, Vincent Goulet, Michel Jacques, Mathieu Pigeon

The R Journal

The expert package provides tools to create and manipulate empirical statistical models using expert opinion (or judgment). Here, the latter expression refers to a specific body of techniques to elicit the distribution of a random variable when data is scarce or unavailable. Opinions on the quantiles of the distribution are sought from experts in the field and aggregated into a final estimate. The package supports aggregation by means of the Cooke, Mendel–Sheridan and predefined weights models.

We do not mean to give a complete introduction to the theory and practice of expert opinion elicitation in this paper. However, for the …

Admit, David Ardia, Lennart F. Hoogerheide, Herman K. Van Dijk

The R Journal

This note presents the package AdMit (Ardia et al., 2008, 2009), an R implementation of the adaptive mixture of Student-t distributions (AdMit) procedure developed by Hoogerheide (2006); see also Hoogerheide et al. (2007); Hoogerheide and van Dijk (2008). The AdMit strategy consists of the construction of a mixture of Student-t distributions which approximates a target distribution of interest. The fitting procedure relies only on a kernel of the tar get density, so that the normalizing constant is not required. In a second step, this approximation is used as an importance function in importance sampling or as a candidate density in …

The Hwriter Package: Composing Html Documents With R Objects, Gregoire Pau, Wolfgang Huber

The R Journal

HTML documents are structured documents made of diverse elements such as paragraphs, sections, columns, figures and tables organized in a hierarchical layout. Combination of HTML documents and hyperlinking is useful to report analysis results; for example, in the package array Quality Metrics (Kauffmannetal., 2009), estimating the quality of mi croarray data sets and cellHTS2(Boutrosetal.,2006), performing the analysis of cell-based screens.

There are several tools for exporting data from R into HTML documents. The package R2HTML is able to render a large diversity of R objects in HTML but does not easily support combining them in a structured layout and …

Collaborative Software Development Using R-Forge, Stefan Theußl, Achim Zeileis

The R Journal

Open source software (OSS) is typically created in a decentralized self-organizing process by a community of developers having the same or similar interests (see the famous essay by Raymond, 1999). A key factor for the success of OSS over the last two decades is the Internet: Developers who rarely meet face-to-face can employ new means of communication, both for rapidly writing and deploying software (in the spirit of Linus Torvald’s “release early, release often paradigm”). Therefore, many tools emerged that assist a collaborative software development process, including in particular tools for source code management (SCM) and version control.

In the …

Facets Of R, John M. Chambers

The R Journal

We are seeing today a widespread, and welcome, tendency for non-computer-specialists among statisticians and others to write collections of R functions that organize and communicate their work. Along with the flood of software sometimes comes an attitude that one need-only-learn, or teach, a sort of basic how-to-write-the-function level of R programming, beyond which most of the detail is unimportant or can be absorbed without much discussion. As delusions go, this one is not very objectionable if it encourages participation. Nevertheless, a delusion it is. In fact, functions are only one of a variety of important facets that R has acquired …

Easier Parallel Computing In R With Snowfall And Sfcluster, Jochen Knaus, Christine Porzelius, Harald Binder, Guido Schwarzer

The R Journal

Many statistical analysis tasks in areas such as bioinformatics are computationally very intensive, while lots of them rely on embarrassingly parallel computations (Grama et al., 2003). Multiple computers or even multiple processor cores on standard desktop computers, which are widespread nowadays, can easily contribute to faster analyses.

R itself does not allow parallel execution. There are some existing solutions for R to distribute calculations over many computers — a cluster — for ex ample Rmpi, rpvm, snow, nws or papply. However these solutions require the user to setup and manage the cluster on his own and …

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

The R Journal

Contributed Research Articles

Facets of R, John M. Chambers

Collaborative Software Development Using R-Forge, Stefan Theußl and Achim Zeileis

Drawing Diagrams with R, Paul Murrell

The hwriter package: Composing HTML Documents with R Objects, Gregoire Pau and Wolfgang Huber

AdMit, David Ardia, Lennart F. Hoogerheide, and Herman K. van Dijk

expert: Modeling Without Data Using Expert Opinion, Vincent Goulet, Michel Jacques, and Mathieu Pigeon

New Numerical Algorithm for Multivariate Normal Probabilities in Package mvtnorm, Xuefei Mi, Tetsuhisa Miwa, and Torsten Hothorn

EMD: A Package for Empirical Mode Decomposition and Hilbert Spectrum, Donghoh Kim, and Hee-Seok Oh

Sample Size Estimation while …

Drawing Diagrams With R, Paul Murrell

The R Journal

R provides a number of well-known high-level facilities for producing sophisticated statistical plots, including the “traditional” plots in the graphics pack age (R Development Core Team, 2008), the Trellis style plots provided by lattice (Sarkar, 2008), and the grammar-of-graphics-inspired approach of ggplot2 (Wickham, 2009). However, R also provides a powerful set of low level graphics facilities for drawing basic shapes and, more importantly, for arranging those shapes relative to each other, which can be used to draw a wide variety of graphical images. This article highlights some of R’s low-level graphics facilities by demonstrating their use in the production of …

Pmml: An Open Standard For Sharing Models, Alex Guazzelli, Michael Zeller, Wen-Ching Lin, Graham Williams

The R Journal

The PMML package exports a variety of predictive and descriptive models from R to the Predictive Model Markup Language (Data Mining Group, 2008). PMML is an XML-based language and has become the de-facto standard to represent not only predictive and descriptive models, but also data pre- and post-processing. In so doing, it allows for the interchange of models among different tools and environments, mostly avoiding proprietary issues and incompatibilities.

The PMML package itself (Williams et al., 2009) was conceived at first as part of Togaware’s data mining toolkit Rattle, the R Analytical Tool To Learn Easily (Williams, 2009). Although it …

A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …

The Design And Implementation Of A Safe, Lightweight Haskell Compiler, Timothy Jan Chevalier

Computer Science Faculty Publications and Presentations

Typed programming languages offer safety guarantees that help programmers write correct code, but typical language implementations offer no proof that source-level guarantees extend to executable code. Moreover, typical implementations link programs with unsafe runtime system (RTS) code. I present a compiler for the functional language Haskell that preserves some of the properties of Haskell’s type system. The soundness proof for the combination of the compiler and a verified RTS requires a proof that the compiler emits code that cooperates correctly with the RTS. In particular, the latter proof must address the boundary between the user program and the garbage collector. …

A Survey Of Monge Properties, Swetha Sethumadhavan

UNLV Theses, Dissertations, Professional Papers, and Capstones

Monge properties play an important role in theoretical computer science. Many greedy algorithms are based on such properties, as is speedup in dynamic programming. Monge properties are simple monotonicity properties which are observed and used in various settings such as resource optimization, computational geometry, statistical sampling, computational biology and coding.

Python As A Teaching Tool, Jason Schultz

Honors Capstones

Capstone submitted as a graduate requirement for the BSU Honors Program.

Algorithms For Vertex-Weighted Matching In Graphs, Mahantesh Halappanavar

Computer Science Theses & Dissertations

A matching M in a graph is a subset of edges such that no two edges in M are incident on the same vertex. Matching is a fundamental combinatorial problem that has applications in many contexts: high-performance computing, bioinformatics, network switch design, web technologies, etc. Examples in the first context include sparse linear systems of equations, where matchings are used to place large matrix elements on or close to the diagonal, to compute the block triangular decomposition of sparse matrices, to construct sparse bases for the null space or column space of under-determined matrices, and to coarsen graphs in multi-level …

Pat: Towards Flexible Verification Under Fairness, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang

Research Collection School Of Computing and Information Systems

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed to model check systems with a variety of fairness effectively in two different settings. Empirical evaluation shows that PAT complements existing model checkers in terms of fairness. We report that previously unknown bugs have been revealed using PAT against systems functioning …

Squeak By Example, Andrew P. Black, Stéphane Ducasse, Oscar Nierstrasz, Damien Pollet, Damien Cassou, Marcus Denker

Computer Science Faculty Publications and Presentations

Squeak is a modern open-source development environment for the classic Smalltalk-80 programming language. This book, intended for both students and developers, will guide you gently through the language and tools by means of a series of examples and exercises.

Additional material is available from the book's web page at SqueakByExample.org.

User Interface Design, Moritz Stefaner, Sebastien Ferre, Saverio Perugini, Jonathan Koren, Yi Zhang

Computer Science Faculty Publications

As detailed in Chap. 1, system implementations for dynamic taxonomies and faceted search allow a wide range of query possibilities on the data. Only when these are made accessible by appropriate user interfaces, the resulting applications can support a variety of search, browsing and analysis tasks. User interface design in this area is confronted with specific challenges. This chapter presents an overview of both established and novel principles and solutions.

An Investigation Into Student Reactions Towards Rad Versus Traditional Programming Environments For Novice Developers, Pansy Colkers

Theses : Honours

The traditional approach to programming using text editors is widely used in many institutions to teach introductory programming. These types of traditional programming environments provide fundamental programming concepts for learning, especially in the context of novice developers. In recent years, teaching institutions have seen a trend towards the introduction of visual "drag-and-drop" rapid application development (RAD) environments for teaching novice programmers. These 'environments capture student interest in programming by allowing the construction of workable programs within a short time frame based on minimal pre-existing coding knowledge. However, some have argued that these visual RAD environments might not be suitable for …

Specifying Reusable Aspects, Neelam Soundarajan, Raffi Khatchadourian

Publications and Research

Aspect-Oriented Programming enables developers to manage, in a more modular fashion, implementations of crosscutting concerns that might be scattered or tangled if aspect-oriented techniques were not utilized. Our interest in this paper is in considering techniques for specifying precise properties of aspects. In particular, we are interested in specifying reusable aspects; i.e., aspects that correspond to crosscutting concerns that occur in many systems. These abstract aspects can be reused in various systems where a particular concern is applicable. Although there has been work on issues related to reasoning about aspects and the behaviors of aspect-oriented systems, specifying reusable abstract aspects …

A Semiotic Analysis Of Unified Modeling Language Graphical Notations, Keng Siau, Yuhong Tian

Research Collection School Of Computing and Information Systems

Unified modeling language (UML) is the standard modeling language for object-oriented system development. Despite its status as a standard, UML has a fuzzy formal specification and a weak theoretical foundation. Semiotics, the study of signs, provides a good theoretical foundation for UML research because graphical notations (or visual signs) of UML are subjected to the principles of signs. In our research, we use semiotics to study the effectiveness of graphical notations in UML. We hypothesized that the use of iconic signs as UML graphical notations leads to representation that is more accurately interpreted and that arouses fewer connotations than the …

Specifying And Verifying Event-Based Fairness Enhanced Systems, Jun Sun, Yang Liu, Jin Song Dong, Hai H. Wang

Research Collection School Of Computing and Information Systems

Liveness/Fairness plays an important role in software specification, verification and development. Existing event-based compositional models are safety-centric. In this paper, we describe a framework for systematically specifying and verifying event-based systems under fairness assumptions. We introduce different event annotations to associate fairness constraints with individual events. Fairness annotated events can be used to embed liveness/fairness assumptions in event-based models flexibly and naturally. We show that state-of-the-art verification algorithms can be extended to verify models under fairness assumptions, with little computational overhead. We further improve the algorithm by other model checking techniques like partial order reduction. A toolset named Pat has …

On The Assessment Of Pointcut Design In Evolving Aspect-Oriented Software, Raffi Khatchadourian, Phil Greenwood, Awais Rashid

Publications and Research

No abstract provided.

Specifying And Verifying Sensor Networks: An Experiment Of Formal Methods, Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang

Research Collection School Of Computing and Information Systems

With the development of sensor technology and electronic miniaturization, wireless sensor networks have shown a wide range of promising applications as well as challenges. Early stage sensor network analysis is critical, which allows us to reveal design errors before sensor deployment. Due to their distinguishable features, system specification and verification of sensor networks are highly non-trivial tasks. On the other hand, numerous formal theories and analysis tools have been developed in formal methods community, which may offer a systematic method for formal analysis of sensor networks. This paper presents our attempt on applying formal methods to sensor network specification/verification. An …

Rejuvenate Pointcut: A Tool For Pointcut Expression Recovery In Evolving Aspect-Oriented Software, Raffi Khatchadourian, Awais Rashid

Publications and Research

Aspect-oriented programming (AOP) strives to localize the scattered and tangled implementations of crosscutting concerns (CCCs) by allowing developers to declare that certain actions (advice) should be taken at specific points (join points) during the execution of software where a CCC (an aspect) is applicable. However, it is non-trivial to construct optimal pointcut expressions (a collection of join points) that capture the true intentions of the programmer and, upon evolution, maintain these intentions. We demonstrate an AspectJ source-level inferencing tool called rejuvenate pointcut which helps developers maintain pointcut expressions over the lifetime of a software product. A key insight into the …

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. In this paper, we present an automated approach which 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. To illustrate that the motivation behind our proposal is well-founded, we first …

Timed Automata Patterns, Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi

Research Collection School Of Computing and Information Systems

Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack composable patterns for high-level system design. Specification languages like Timed Communicating Sequential Process (CSP) and Timed Communicating Object-Z (TCOZ) are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in time-enriched process algebras. The patterns facilitate the hierarchical design of complex systems …

Holistic Characterization Of Parallel Programming Models In A Distributed Memory Environment, Christopher Bryan

Computer Science and Computer Engineering Undergraduate Honors Theses

The popularity of cluster computing has increased focus on usability, especially in the area of programmability. Languages and libraries that require explicit message passing have been the standard. New languages, designed for cluster computing, are coming to the forefront as a way to simplify parallel programming. Titanium and Fortress are examples of this new class of programming paradigms. This work holistically characterizes these languages and contrasts them with the standard model of parallel programming, and presents benchmark results of small computational kernels written in these languages and models.