Programming Languages and Compilers Commons^™

Interactive Ambient Visualizations For Soft Advice, Emerson Murphy-Hill, Titus Barik, Andrew P. Black

Computer Science Faculty Publications and Presentations

Some software packages offer the user soft advice: recommendations that are intended to help the user create high quality artifacts, but which may turn out to be bad advice. It is left to the user to determine whether the soft advice really will improve quality, and to decide whether or not to adopt it. Visualizations can help the user in making this decision, but we believe that conventional visualizations are less than ideal. In this paper, we describe an interactive ambient visualization to help users identify, understand and interpret soft advice.

Our visualization was developed to help programmers interpret code …

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 …

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 …

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 …

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 …

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 …

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 …

Cuda Web Api Remote Execution Of Cuda Kernels Using Web Services, Massimo J. Becker

Master's Theses

Massively parallel programming is an increasingly growing field with the recent introduction of general purpose GPU computing. Modern graphics processors from NVIDIA and AMD have massively parallel architectures that can be used for such applications as 3D rendering, financial analysis, physics simulations, and biomedical analysis. These massively parallel systems are exposed to programmers through in- terfaces such as NVIDIAs CUDA, OpenCL, and Microsofts C++ AMP. These frame- works expose functionality using primarily either C or C++. In order to use these massively parallel frameworks, programs being implemented must be run on machines equipped with massively parallel hardware. These requirements limit …

Pointcut Rejuvenation: Recovering Pointcut Expressions In Evolving Aspect-Oriented Software, Raffi Khatchadourian, Phil Greenwood, Awais Rashid, 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 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. To illustrate that the motivation behind our proposal is well founded, …

Extending Java For Android Programming, Yoonsik Cheon

Departmental Technical Reports (CS)

Android is one of the most popular platforms for developing mobile applications. However, its framework relies on programming conventions and styles to implement framework-specific concepts like activities and intents, causing problems such as reliability, readability, understandability, and maintainability. We propose to extend Java to support Android framework concepts explicitly as built-in language features. Our extension called Android Java will allow Android programmers to express these concepts in a more reliable, natural, and succinct way.

Programming In A Socially Networked World: The Evolution Of The Social Programmer, Christoph Treude, Fernando Figueira Filho, Brendan Cleary, Margaret-Anne Storey

Research Collection School Of Computing and Information Systems

Social media has changed how software developers collaborate, how they coordinate their work, and where they find information. Social media sites, such as the Question and Answer (Q&A) portal Stack Overflow, fill archives with millions of entries that contribute to what we know about software development, covering a wide range of topics. For today’s software developers, reusable code snippets, introductory usage examples, and pertinent libraries are often just a web search away. In this position paper, we discuss the opportunities and challenges for software developers that rely on web content curated by the crowd, and we envision the future of …

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, …

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.

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 …

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, …

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 …

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 …

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 …

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. …

Formalizing Reusable Aspect-Oriented Concurrency Control, Neelam Soundarajan, Derek Bronish, Raffi Khatchadourian

Publications and Research

Java and its library provide powerful concurrency control mechanisms. However, their use can lead to similar synchronization code scattered across multiple classes, synchronization and functional code being tangled together, and similar code being duplicated in many applications. Aspect-oriented (AO) programming makes it possible to address these problems. However, the specific behavior of systems built using AO techniques can be challenging to comprehend. We propose a specification approach to precisely express such systems' critical concurrency and synchronization properties. We illustrate the method with a simple example.