Programming Languages and Compilers Commons^™

Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li

Research Collection School Of Computing and Information Systems

The process analysis toolkit (PAT) integrates the expressiveness of state, event, time, and probability-based languages with the power of model checking. PAT is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 12 different expressive modeling languages with many application domains and has attracted thousands of registered users from hundreds of organizations. In this invited talk, we will present the PAT system and its vision on “Event Analytics” (EA) which is beyond “Data Analytics”. The EA research is based on applying model checking to event planning, scheduling, prediction, strategy analysis and decision …

An Overview Of The Current State Of The Test-First Vs. Test-Last Debate, Christopher M. Thomas

Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal

When it comes to software development, perhaps one of the most important and time consuming processes is that of software testing. In fact, early studies on software testing estimated that it could consume fifty percent or more of development costs for a product. Because of this, the ability to optimize testing to reduce testing costs can be very valuable. In this paper we compare two popular methods, test-last testing, often used in waterfall software development processes, and test-first testing, often used in Agile test driven software development methods, by reviewing recent studies on the subject. In this review we discuss …

Improved Microrobotic Control Through Image Processing And Automated Hardware Interfacing, Archit R. Aggarwal, Wuming Jing, David J. Cappelleri

The Summer Undergraduate Research Fellowship (SURF) Symposium

Untethered submilliliter-sized robots (microrobots) are showing potential use in different industrial, manufacturing and medical applications. A particular type of these microrobots, magnetic robots, have shown improved performance in power and control capabilities compared to the other thermal and electrostatic based robots. However, the magnetic robot designs have not been assessed in a robust manner to understand the degree of control in different environments and their application feasibility. This research project seeks to develop a custom control software interface to provide a holistic tool for researchers to evaluate the microrobotic performance through advance control features. The software deliverable involved two main …

A Palm Vein Identification System Based On Gabor Wavelet Features, Ran Wang, Guoyou Wang, Zhong Chen, Zhigang Zeng, Yong Wang

Research Collection School Of Computing and Information Systems

As a new and promising biometric feature, thermal palm vein pattern has drawn lots of attention in research and application areas. Many algorithms have been proposed for authentication since palm vein has special characteristics, such as liveness detection and hard to forgery. However, the detection accuracy of palm vein quite depends on the preprocessing and feature representation, which is supposed to be translation and rotation invariant to some extent. In this paper, we proposed an effective method for palm vein identification based on Gabor wavelet features which contains five steps: image acquisition, ROI detection, image preprocessing, features extraction, and matching. …

Structure Preserving Large Imagery Reconstruction, Ju Shen, Jianjun Yang, Sami Taha Abu Sneineh, Bryson Payne, Markus Hitz

Computer Science Faculty Publications

With the explosive growth of web-based cameras and mobile devices, billions of photographs are uploaded to the internet. We can trivially collect a huge number of photo streams for various goals, such as image clustering, 3D scene reconstruction, and other big data applications. However, such tasks are not easy due to the fact the retrieved photos can have large variations in their view perspectives, resolutions, lighting, noises, and distortions. Furthermore, with the occlusion of unexpected objects like people, vehicles, it is even more challenging to find feature correspondences and reconstruct realistic scenes. In this paper, we propose a structure-based image …

Diamonds Are A Girl's Best Friend: Partial Order Reduction For Timed Automata With Abstractions, Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun

Research Collection School Of Computing and Information Systems

A major obstacle for using partial order reduction in the context of real time verification is that the presence of clocks and clock constraints breaks the usual diamond structure of otherwise independent transitions. This is especially true when information of the relative values of clocks is preserved in the form of diagonal constraints. However, when diagonal constraints are relaxed by a suitable abstraction, some diamond structure is re-introduced in the zone graph. In this article, we introduce a variant of the stubborn set method for reducing an abstracted zone graph. Our method works with all abstractions, but especially targets situations …

Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …

Writing Self-Testing Java Classes With Selftest, Yoonsik Cheon

Departmental Technical Reports (CS)

This document provides a tutorial introduction to Java annotations called SelfTest. The SelfTest annotations allow one to annotate Java classes with test data, and the SelfTest annotation processor generates executable JUnit test classes from annotated Java classes by translating test cases to executable JUnit tests. The SelfTest annotations not only automate unit testing of Java classes significantly but also provides a step toward writing self-testing Java classes by embedding test data in source code for both compile and runtime processing.

Automatic Objects Removal For Scene Completion, Jianjun Yang, Yin Wang, Honggang Wang, Kun Hua, Wei Wang, Ju Shen

Computer Science Faculty Publications

With the explosive growth of Web-based cameras and mobile devices, billions of photographs are uploaded to the Internet. We can trivially collect a huge number of photo streams for various goals, such as 3D scene reconstruction and other big data applications. However, this is not an easy task due to the fact the retrieved photos are neither aligned nor calibrated. Furthermore, with the occlusion of unexpected foreground objects like people, vehicles, it is even more challenging to find feature correspondences and reconstruct realistic scenes. In this paper, we propose a structure-based image completion algorithm for object removal that produces visually …

Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, …

Towards Verification Of Computation Orchestration, Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang

Research Collection School Of Computing and Information Systems

Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we …

Model Checking Approach To Automated Planning, Yi Li, Jin Song Dong, Jing Sun, Yang Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Model checking provides a way to automatically explore the state space of a finite state system based on desired properties, whereas planning is to produce a sequence of actions that leads from the initial state to the target goal states. Previous research in this field proposed a number of approaches for connecting model checking with planning problem solving. In this paper, we investigate the feasibility of using an established model checking framework, Process Analysis Toolkit (PAT), as a planning solution provider for upper layer applications. To achieve this, we first carry out a number of experiments on different model checking …

Learning Assumptions For Compositional Verification Of Timed Systems, Shang-Wei Lin Lin, Yang Liu, Jun Sun, Jun Sun

Research Collection School Of Computing and Information Systems

Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, because constructing appropriate assumptions for AGR usually requires human creativity and experience. To automate compositional verification of timed systems, we propose a compositional verification framework using a learning algorithm for automatic construction of timed assumptions for AGR. We prove the correctness and termination of the proposed learning-based framework, and experimental results show that our method performs significantly better than traditional monolithic timed model checking.

Complexity Of The Soundness Problem Of 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 for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for …

An Approach For Clone Detection In Documentation Reuse, Dmitry V. Lutsiv, Dmitry Koznov, Hamid A. Basit, Eng Lieh Ouh, Mikhail N. Smirnov, Konstantin Y. Romanovsky

Research Collection School Of Computing and Information Systems

The paper focuses on the searching method for repetitions in DocBook/DRL or plain text documents. An algorithm has been designed based on software clone detection. The algorithm supports filtering results: clones are rejected if clone length in the group is less than 5 symbols, intersection of clone groups is eliminated, meaningfulness clones are removed, the groups containing clones consisting only of XML are eliminated. Remaining search is supported: found clones are extracted from the documentation, and clone search is repeated. One step is proved to be enough. Adaptive reuse technique of Paul Bassett – Stan Jarzabek has been implemented. A …

From Rssi To Csi: Indoor Localization Via Channel Response, Zheng Yang, Zimu Zhou, Yunhao Liu

Research Collection School Of Computing and Information Systems

The spatial features of emitted wireless signals are the basis of location distinction and determination for wireless indoor localization. Available in mainstream wireless signal measurements, the Received Signal Strength Indicator (RSSI) has been adopted in vast indoor localization systems. However, it suffers from dramatic performance degradation in complex situations due to multipath fading and temporal dynamics.

Cell: A Compositional Verification Framework, Kun Ji, Yang Liu, Jun Sun, Jun Sun, Jin Song Dong, Truong Khanh Nguyen

Research Collection School Of Computing and Information Systems

This paper presents CELL, a comprehensive and extensible framework for compositional verification of concurrent and real-time systems based on commonly used semantic models. For each semantic model, CELL offers three libraries, i.e., compositional verification paradigms, learning algorithms and model checking methods to support various state-of-the-art compositional verification approaches. With well-defined APIs, the framework could be applied to build customized model checkers. In addition, each library could be used independently for verification and program analysis purposes. We have built three model checkers with CELL. The experimental results show that the performance of these model checkers can offer similar or often better …

A Robust Rgbd Slam System For 3d Environment With Planar Surfaces, Po-Chang Su, Ju Shen, Sen-Ching S. Cheung

Computer Science Faculty Publications

With the increasing popularity of RGB-depth (RGB-D) sensors such as the Microsoft Kinect, there have been much research on capturing and reconstructing 3D environments using a movable RGB-D sensor. The key process behind these kinds of simultaneous location and mapping (SLAM) systems is the iterative closest point or ICP algorithm, which is an iterative algorithm that can estimate the rigid movement of the camera based on the captured 3D point clouds. While ICP is a well-studied algorithm, it is problematic when it is used in scanning large planar regions such as wall surfaces in a room. The lack of depth …

Reaper – Toward Automating Mobile Cloud Communication, Daniel R. Ward

LSU New Orleans Theses and Dissertations

Mobile devices connected to cloud based services are becoming a mainstream method of delivery up-to-date and context aware information to users. Connecting mobile applications to cloud service require significant developer effort. Yet this communication code usually follows certain patterns, varying accordingly to the specific type of data sent and received from the server. By analyzing the causes of theses variations, we can create a system that can automate the code creation for communication from a mobile device to a cloud server. To automate code creation, a general pattern must extracted. This general solution can then be applied to any database …

Enhancing The Expressiveness Of The Cleanjava Language, Melisa Vela, Yoonsik Cheon

Departmental Technical Reports (CS)

The CleanJava language is a formal annotation language for Java to support Cleanroom-style functional program verification that views a program as a mathematical function from one program state to another. The CleanJava notation is based on the Java expression syntax with a few extensions, and thus its vocabulary is somewhat limited to that of Java. This often makes it difficult to specify the rich semantics of a Java program in a succinct and natural way that is easy to manipulate for formal correctness reasoning. In this paper we propose to make the CleanJava language more expressive by supporting user-defined mathematical …

Spring­11: Pdc In Cs1/2 And A Mobile/Cloud Intermediate Mobile/Cloud Intermediate Software Design Course, Joseph P. Kaylor, Konstantin Läufer, Chandra N. Sekharan, George K. Thiruvathukal

Computer Science: Faculty Publications and Other Works

Recent changes in the environment of Loyola University Chicago’s Department of Computer Science include a better differentiation of our four undergraduate majors, growing interest in computing among science majors, and an increased demand for graduates with mobile and cloud skills. In our continued effort to incorporate parallel and distributed computing topics into the undergraduate curriculum, we are focusing on these three existing courses:

CS1: In response to a request from the physics department, we started to offer a CS1 section aimed at majors in physics and other hard sciences this spring semester. This section includes some material on numerical methods …

Building Capable, Energy-Efficient, Flexible Visualization And Sensing Clusters From Commodity Tablets, Thomas Delgado Dias, Xian Yan, Konstantin Läufer, George K. Thiruvathukal

Computer Science: Faculty Publications and Other Works

We explore the application of clusters of commodity tablet devices to problems spanning a “trilogy” of concerns: visualization, sensing, and computation. We conjecture that such clusters provide a low-cost, energy-efficient, flexible, and ultimately effective platform to tackle a wide range of problems within this trilogy. This is a work in progress, and we now elaborate our position and give a preliminary status report.

A wide range of Android tablet devices are available in terms of price and capabilities. “You get what you pay for” w.r.t. display resolution, sensors, and chipset---corresponding to the trilogy. $200 gets one a 1280x800-pixel touch display, …

Network Technologies Used To Aggregate Environmental Data, Paul Stasiuk, Konstantin Läufer, George K. Thiruvathukal

Computer Science: Faculty Publications and Other Works

The goal of the Loyola Weather Service (lws) project is to design and build a system of functioning environmental monitoring widgets that can intelligently and autonomously control the environment around them based on set thresholds and triggers. The widgets will also have the ability to aggregate their data and easily display this data in various ways: through a user interface in the room that the widget is placed, via a web application, and programmatically via a RESTful web service.

Cjc: An Extensible Checker For The Cleanjava Annotation Language, Cesar Yeep

Departmental Technical Reports (CS)

CleanJava is a formal annotation language for the Java programming language to support a Cleanroom-style functional program verification technique that views programs as mathematical functions. It needs a suite of support tools including a checker that can parse annotations and check them for syntactic and static semantic correctness. The two key requirements of the checker are flexibility and extensibility. Since the language is still under development and refinement, it should be flexible to facilitate language experimentation and accommodate language changes. It should be also extensible to provide base code for developing more advanced support tools like an automated theorem prover. …

Efficient Architectures For Retrieving Mixed Data With Rest Architecture Style And Html5 Support, Koushik Maddipudi

Masters Theses & Specialist Projects

Software as a service is an emerging but important aspect of the web. Web
Services play a vital role in providing it. Web Services are commonly provided in one of two architectural styles: a "REpresentational State Transfer" (REST), or using the "Simple Object Access Protocol" (SOAP.) Originally most web content was text and small images. But more recent services involve complex data structures including text, images, audio, and video. The task of optimizing data to provide delivery of these structures is a complex one, involving both theoretical and practical aspects. In this thesis work, I have considered two architectures developed …

A Polyglot Approach To Bioinformatics Data Integration: Phylogenetic Analysis Of Hiv-1, Steven Reisman, Catherine Putonti, George K. Thiruvathukal, Konstantin Läufer

Computer Science: Faculty Publications and Other Works

RNA-interference has potential therapeutic use against HIV-1 by targeting highly-functional mRNA sequences that contribute to the virulence of the virus. Empirical work has shown that within cell lines, all of the HIV-1 genes are affected by RNAi-induced gene silencing. While promising, inherent in this treatment is the fact that RNAi sequences must be highly specific. HIV, however, mutates rapidly, leading to the evolution of viral escape mutants. In fact, such strains are under strong selection to include mutations within the targeted region, evading the RNAi therapy and thus increasing the virus’ fitness in the host. Taking a phylogenetic approach, we …

Senior Project Report - Doctest, Stephen Weessies

Computer Engineering

DocTest is a program that, simply put, allows a programmer or user to document STANAG 4586 (a standard for unmanned aerial vehicle interoperability) messages and test the vehicle system at Lockheed Martin [5]. The program is extensible to allow for further development aiding our software team to do what they do best and not get bogged down in tedious but necessary documentation. DocTest is also used to aid in testing, keeping track of the issues and bugs found and creating a document that captures each issue so an issue is not missed or forgotten. This program was made for use …

Object-Oriented Programming: Some History, And Challenges For The Next Fifty Years, Andrew P. Black

Computer Science Faculty Publications and Presentations

Object-oriented programming is inextricably linked to the pioneering work of Ole-Johan Dahl and Kristen Nygaard on the design of the Simula language, which started at the Norwegian Computing Centre in the Spring of 1961. However, object-orientation, as we think of it today—fifty years later—is the result of a complex interplay of ideas, constraints and people. Dahl and Nygaard would certainly recognize it as their progeny, but might also be amazed at how much it has grown up. This article is based on a lecture given on 22nd August 2011, on the occasion of the scientific opening of the Ole-Johan …

Verifying Linearizability Via Optimized Refinement Checking, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong Dong

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 are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on …

Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André

Research Collection School Of Computing and Information Systems

Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful …