Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Programming Languages and Compilers (21)
- Engineering (14)
- Databases and Information Systems (12)
- Social and Behavioral Sciences (9)
- Computer Engineering (8)
-
- Information Security (8)
- Communication (5)
- Graphics and Human Computer Interfaces (5)
- Systems Architecture (4)
- Communication Technology and New Media (3)
- Education (3)
- OS and Networks (3)
- Other Computer Sciences (3)
- Theory and Algorithms (3)
- Computer and Systems Architecture (2)
- Curriculum and Instruction (2)
- Digital Communications and Networking (2)
- Discrete Mathematics and Combinatorics (2)
- Electrical and Computer Engineering (2)
- Higher Education (2)
- Mathematics (2)
- Numerical Analysis and Scientific Computing (2)
- Operational Research (2)
- Operations Research, Systems Engineering and Industrial Engineering (2)
- Organizational Communication (2)
- Applied Behavior Analysis (1)
- Applied Mathematics (1)
- Institution
-
- Singapore Management University (88)
- Western University (13)
- University of Nevada, Las Vegas (7)
- Air Force Institute of Technology (5)
- University of Arkansas, Fayetteville (3)
-
- University of Nebraska - Lincoln (3)
- University of Texas at El Paso (3)
- LSU New Orleans (2)
- California Polytechnic State University, San Luis Obispo (1)
- California State University, San Bernardino (1)
- City University of New York (CUNY) (1)
- Colby College (1)
- Montana Tech Library (1)
- New Jersey Institute of Technology (1)
- Technological University Dublin (1)
- University of Denver (1)
- University of New Hampshire (1)
- University of North Florida (1)
- Vocational Training Council (1)
- Western Michigan University (1)
- Keyword
-
- Model Check (7)
- Software engineering (4)
- Collaboration (3)
- Context (3)
- Label Transition System (3)
-
- Mobile (3)
- Sensing (3)
- Software development (3)
- Activity recognition (2)
- Combinatorics (2)
- Constraints (2)
- Cost estimation (2)
- Defect prediction (2)
- Dynamic analysis (2)
- Empirical study (2)
- Energy (2)
- Fault Localization (2)
- Formal Verification (2)
- Games (2)
- Linear Temporal Logic (2)
- Model Checking (2)
- Model checking (2)
- NCCR-MICS (2)
- NCCR-MICS/ESDM (2)
- Operational Semantic (2)
- Optimization (2)
- Platform (2)
- Power Management (2)
- Programming (2)
- Project management (2)
- Publication
-
- Research Collection School Of Computing and Information Systems (88)
- Electrical and Computer Engineering Publications (13)
- College of Engineering: Graduate Celebration Programs (4)
- Computer Science and Computer Engineering Undergraduate Honors Theses (3)
- Theses and Dissertations (3)
-
- LSU New Orleans Theses and Dissertations (2)
- School of Computing: Dissertations, Theses, and Student Research (2)
- AFIT Patents (1)
- COURI Symposium Abstracts, Spring 2012 (1)
- COURI Symposium Abstracts, Summer 2012 (1)
- Civil and Environmental Engineering and Construction Faculty Research (1)
- Computer Science & Software Engineering (1)
- Departmental Technical Reports (CS) (1)
- Dissertations (1)
- Electronic Theses and Dissertations (1)
- Faculty Publications (1)
- Honors Theses (1)
- Honors Theses and Capstones (1)
- Library Faculty Presentations (1)
- Master's Theses (1)
- Other (1)
- Practical Social and Industrial Research Symposium (1)
- Publications and Research (1)
- School of Computing: Technical Reports (1)
- Theses (1)
- Theses Digitization Project (1)
- UNF Graduate Theses and Dissertations (1)
- UNLV Theses, Dissertations, Professional Papers, and Capstones (1)
- Publication Type
Articles 31 - 60 of 136
Full-Text Articles in Software Engineering
Duplicate Bug Report Detection With A Combination Of Information Retrieval And Topic Modeling, Anh Tuan Nguyen, Tung Nguyen, Tien Nguyen, David Lo, Chengnian Sun
Duplicate Bug Report Detection With A Combination Of Information Retrieval And Topic Modeling, Anh Tuan Nguyen, Tung Nguyen, Tien Nguyen, David Lo, Chengnian Sun
Research Collection School Of Computing and Information Systems
Detecting duplicate bug reports helps reduce triaging efforts and save time for developers in fixing the same issues. Among several automated detection approaches, text-based information retrieval (IR) approaches have been shown to outperform others in term of both accuracy and time efficiency. However, those IR-based approaches do not detect well the duplicate reports on the same technical issues written in different descriptive terms. This paper introduces DBTM, a duplicate bug report detection approach that takes advantage of both IR-based features and topic-based features. DBTM models a bug report as a textual document describing certain technical issue(s), and models duplicate bug …
Diversity Maximization Speedup For Fault Localization, Liang Gong, David Lo, Lingxiao Jiang, Hongyu Zhang
Diversity Maximization Speedup For Fault Localization, Liang Gong, David Lo, Lingxiao Jiang, Hongyu Zhang
Research Collection School Of Computing and Information Systems
Fault localization is useful for reducing debugging effort. However, many fault localization techniques require non-trivial number of test cases with oracles, which can determine whether a program behaves correctly for every test input. Test oracle creation is expensive because it can take much manual labeling effort. Given a number of test cases to be executed, it is challenging to minimize the number of test cases requiring manual labeling and in the meantime achieve good fault localization accuracy. To address this challenge, this paper presents a novel test case selection strategy based on Diversity Maximization Speedup (DMS). DMS orders a set …
To What Extent Could We Detect Field Defects? An Empirical Study Of False Negatives In Static Bug Finding Tools, Ferdian Thung, Lucia Lucia, David Lo, Lingxiao Jiang, Premkumar Devanbu, Foyzur Rahman
To What Extent Could We Detect Field Defects? An Empirical Study Of False Negatives In Static Bug Finding Tools, Ferdian Thung, Lucia Lucia, David Lo, Lingxiao Jiang, Premkumar Devanbu, Foyzur Rahman
Research Collection School Of Computing and Information Systems
Software defects can cause much loss. Static bug-finding tools are believed to help detect and remove defects. These tools are designed to find programming errors; but, do they in fact help prevent actual defects that occur in the field and reported by users? If these tools had been used, would they have detected these field defects, and generated warnings that would direct programmers to fix them? To answer these questions, we perform an empirical study that investigates the effectiveness of state-of-the-art static bug finding tools on hundreds of reported and fixed defects extracted from three open source programs: Lucene, Rhino, …
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
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 …
The Fat Thumb: Using The Thumb's Contact Size For Single-Handed Mobile Interaction, Sebastian Boring, David Ledo, Xiang ‘Anthony’ Chen, Nicolai Marquardt, Anthony Tang, Saul Greenberg
The Fat Thumb: Using The Thumb's Contact Size For Single-Handed Mobile Interaction, Sebastian Boring, David Ledo, Xiang ‘Anthony’ Chen, Nicolai Marquardt, Anthony Tang, Saul Greenberg
Research Collection School Of Computing and Information Systems
Modern mobile devices allow a rich set of multi-finger interactions that combine modes into a single fluid act, for example, one finger for panning blending into a two-finger pinch gesture for zooming. Such gestures require the use of both hands: one holding the device while the other is interacting. While on the go, however, only one hand may be available to both hold the device and interact with it. This mostly limits interaction to a single-touch (i.e., the thumb), forcing users to switch between input modes explicitly. In this paper, we contribute the Fat Thumb interaction technique, which uses the …
Adaptive In-Network Processing For Bandwidth And Energy Constrained Mission-Oriented Multi-Hop Wireless Networks, Sharanya Eswaran, James Edwards, Archan Misra, Thomas La Porta
Adaptive In-Network Processing For Bandwidth And Energy Constrained Mission-Oriented Multi-Hop Wireless Networks, Sharanya Eswaran, James Edwards, Archan Misra, Thomas La Porta
Research Collection School Of Computing and Information Systems
In-network processing, involving operations such as filtering, compression and fusion, is a technique widely used in wireless sensor and ad hoc networks for reducing the communication overhead. In many tactical stream-oriented applications, especially in military scenarios, both link bandwidth and node energy are critically constrained resources. For such applications, in-network processing itself imposes non-negligible computing cost. In this work, we have developed a unified, utility-based closed-loop control framework that permits distributed convergence to both a) the optimal level of compression performed by a forwarding node on streams, and b) the best set of nodes where the operators of the stream …
Observatory Of Trends In Software Related Microblogs, Achananuparp Palakorn, Nelman Lubis Ibrahim, Yuan Tian, David Lo, Ee Peng Lim
Observatory Of Trends In Software Related Microblogs, Achananuparp Palakorn, Nelman Lubis Ibrahim, Yuan Tian, David Lo, Ee Peng Lim
Research Collection School Of Computing and Information Systems
Microblogging has recently become a popular means to disseminate information among millions of people. Interestingly, software developers also use microblog to communicate with one another. Different from traditional media, microblog users tend to focus on recency and informality of content. Many tweet contents are relatively more personal and Opinionated, compared to that of traditional news report. Thus, by analyzing microblogs, one could get the up-to-date information about what people are interested in or feel toward a particular topic. In this paper, we describe our microblog observatory that aggregates more than 70,000 Twitter feeds, captures software-related tweets, and computes trends from …
Interactive Fault Localization Leveraging Simple User Feedback, Liang Gong, David Lo, Lingxiao Jiang, Hongyu Zhang
Interactive Fault Localization Leveraging Simple User Feedback, Liang Gong, David Lo, Lingxiao Jiang, Hongyu Zhang
Research Collection School Of Computing and Information Systems
Millions of people, including those in the software engineering communities have turned to microblogging services, such as Twitter, as a means to quickly disseminate information. A number of past studies by Treude et al., Storey, and Yuan et al. have shown that a wealth of interesting information is stored in these microblogs. However, microblogs also contain a large amount of noisy content that are less relevant to software developers in engineering software systems. In this work, we perform a preliminary study to investigate the feasibility of automatic classification of microblogs into two categories: relevant and irrelevant to engineering software systems. …
Automatic Classification Of Software Related Microblogs, Philips Kokoh Prasetyo, David Lo, Achananuparp Palakorn, Yuan Tian, Ee Peng Lim
Automatic Classification Of Software Related Microblogs, Philips Kokoh Prasetyo, David Lo, Achananuparp Palakorn, Yuan Tian, Ee Peng Lim
Research Collection School Of Computing and Information Systems
Millions of people, including those in the software engineering communities have turned to microblogging services, such as Twitter, as a means to quickly disseminate information. A number of past studies by Treude et al., Storey, and Yuan et al. have shown that a wealth of interesting information is stored in these microblogs. However, microblogs also contain a large amount of noisy content that are less relevant to software developers in engineering software systems. In this work, we perform a preliminary study to investigate the feasibility of automatic classification of microblogs into two categories: relevant and irrelevant to engineering software systems. …
Detecting Similar Applications With Collaborative Tagging, Ferdian Thung, David Lo, Lingxiao Jiang
Detecting Similar Applications With Collaborative Tagging, Ferdian Thung, David Lo, Lingxiao Jiang
Research Collection School Of Computing and Information Systems
Millions of people, including those in the software engineering communities have turned to microblogging services, such as Twitter, as a means to quickly disseminate information. A number of past studies by Treude et al., Storey, and Yuan et al. have shown that a wealth of interesting information is stored in these microblogs. However, microblogs also contain a large amount of noisy content that are less relevant to software developers in engineering software systems. In this work, we perform a preliminary study to investigate the feasibility of automatic classification of microblogs into two categories: relevant and irrelevant to engineering software systems. …
When Would This Bug Get Reported?, Ferdian Thung, David Lo, Lingxiao Jiang, Lucia Lucia, Foyzur Rahman, Premkumar Devanbu
When Would This Bug Get Reported?, Ferdian Thung, David Lo, Lingxiao Jiang, Lucia Lucia, Foyzur Rahman, Premkumar Devanbu
Research Collection School Of Computing and Information Systems
Millions of people, including those in the software engineering communities have turned to microblogging services, such as Twitter, as a means to quickly disseminate information. A number of past studies by Treude et al., Storey, and Yuan et al. have shown that a wealth of interesting information is stored in these microblogs. However, microblogs also contain a large amount of noisy content that are less relevant to software developers in engineering software systems. In this work, we perform a preliminary study to investigate the feasibility of automatic classification of microblogs into two categories: relevant and irrelevant to engineering software systems. …
Kbe-Anonymity: Test Data Anonymization For Evolving Programs, Lucia Lucia, David Lo, Lingxiao Jiang, Aditya Budi
Kbe-Anonymity: Test Data Anonymization For Evolving Programs, Lucia Lucia, David Lo, Lingxiao Jiang, Aditya Budi
Research Collection School Of Computing and Information Systems
High-quality test data that is useful for effective testing is often available on users’ site. However, sharing data owned by users with software vendors may raise privacy concerns. Techniques are needed to enable data sharing among data owners and the vendors without leaking data privacy. Evolving programs bring additional challenges because data may be shared multiple times for every version of a program. When multiple versions of the data are cross-referenced, private information could be inferred. Although there are studies addressing the privacy issue of data sharing for testing and debugging, little work has explicitly addressed the challenges when programs …
A Framework To Annotate The Uncertainty For Geospatial Data, Zhao Yang
A Framework To Annotate The Uncertainty For Geospatial Data, Zhao Yang
LSU New Orleans Theses and Dissertations
We have developed a new approach to annotate the uncertainty information of geospatial data. This framework is composed of a geospatial platform and the data with uncertainty. The framework supports geospatial sources such as Geography Markup Language (GML) with uncertainty information. The purpose of this framework is to integrate the uncertainty information of data from the application users and thereby ease the development of processing uncertainty information of geospatial data. Having well organized data and using this framework, the end-users can store the uncertainty information on the current geospatial data structure. For example, a GIS user can share the error …
Measurement-Driven Performance Analysis Of Indoor Femtocellular Networks, Trung-Tuan Luong, Vigneshwaran Subbaraju, Archan Misra, Srinivasan Seshan
Measurement-Driven Performance Analysis Of Indoor Femtocellular Networks, Trung-Tuan Luong, Vigneshwaran Subbaraju, Archan Misra, Srinivasan Seshan
Research Collection School Of Computing and Information Systems
This paper describes initial empirical studies, performed on a 6-node 3G indoor femtocellular testbed, that investigate the impact of pedestrian mobility on network parameters, such as handoff behavior and data throughput. The studies establish that, owing to the small radii of cells, even modest changes in movement speed can have disproportionately large impact on handoff patterns and network throughput. By also revealing a strong temporal dependency effect, the studies motivate the need for algorithms to accurately predict RF signal strength distributions in dynamic indoor environments. We present such an RF prediction algorithm, based on crowd-sourced signal strength readings, and show …
Adaptive Display Power Management For Oled Displays, Kiat Wee Tan, Rajesh Krishna Balan
Adaptive Display Power Management For Oled Displays, Kiat Wee Tan, Rajesh Krishna Balan
Research Collection School Of Computing and Information Systems
Mobile gaming has become increasingly popular in the past few years with the proliferation of smartphones that have the increased CPU, memory, and network (3.5G etc.) capabilities to support a vast range of interesting games. In addition, these phones also have high quality displays, such as Organic Light Emitting Diodes (OLED) displays, that allow the intricate details in games to be shown in vivid detail to end users. Unfortunately, these displays tend to consume a lot of energy which in turn limits the amount of time that a user can spend actually playing games on these devices. In this paper, …
Eliciting A Sensemaking Process From Verbal Protocols Of Reverse Engineers, Adam R. Bryant, Robert F. Mills, Gilbert L. Peterson, Michael R. Grimaila
Eliciting A Sensemaking Process From Verbal Protocols Of Reverse Engineers, Adam R. Bryant, Robert F. Mills, Gilbert L. Peterson, Michael R. Grimaila
Faculty Publications
A process of sensemaking in reverse engineering was elicited from verbal protocols of reverse engineers as they investigated the assembly code of executable programs. Four participants were observed during task performance and verbal protocols were collected and analyzed from two of the participants to determine their problem-solving states and characterize likely transitions between those states. From this analysis, a high-level process of sensemaking is described which represents hypothesis generation and information-seeking behaviors in reverse engineering within a framework of goal-directed planning. Future work in validation and application of the process is discussed.
Control-Theoretic Utility Maximization In Multihop Wireless Networks Under Mission Dynamics, Sharanya Eswaran, Archan Misra, Thomas La Porta
Control-Theoretic Utility Maximization In Multihop Wireless Networks Under Mission Dynamics, Sharanya Eswaran, Archan Misra, Thomas La Porta
Research Collection School Of Computing and Information Systems
Both bandwidth and energy become important resource constraints when multi-hop wireless networks are used to transport high data rate traffic for a moderately long duration. In such networks, it is important to control the traffic rates to not only conform to the link capacity bounds but also to ensure that the energy of battery-powered forwarding nodes is utilized judiciously to avoid premature exhaustion (i.e., the network lasts as long as the applications require data from the sources) without being unneccesarily conservative (i.e., ensuring that the applications derive the maximum utility possible). Unlike prior work that focuses on the instantaneous distributed …
The Case For Cloud-Enabled Mobile Sensing Services, Sougata Sen, Archan Misra, Rajesh Krishna Balan, Lipyeow Lim
The Case For Cloud-Enabled Mobile Sensing Services, Sougata Sen, Archan Misra, Rajesh Krishna Balan, Lipyeow Lim
Research Collection School Of Computing and Information Systems
We make the case for cloud-enabled mobile sensing services that support an emerging application class, one which infers near-real time collective context using sensor data obtained continuously from a large set of consumer mobile devices. We present the high-level architecture and functional requirements for such a mobile sensing service, and argue that such a service can significantly improve the scalability and energy-efficiency of large-scale mobile sensing by coordinating the sensing & processing tasks across multiple devices. We then focus specifically on the problem of energy efficiency and provide early exemplars of how optimizing query execution jointly over multiple phones can …
Adapting Video Delivery Based On Motion Triggered Visual Attention, Hari Kalva, V. Adzic, Lai-Tee Cheok
Adapting Video Delivery Based On Motion Triggered Visual Attention, Hari Kalva, V. Adzic, Lai-Tee Cheok
Research Collection School Of Computing and Information Systems
Cues from human visual system (HVS) can be used for further optimization of compression in modern hybrid video coding platforms. We present work that explores and exploits motion related attentional limitations. Algorithms for exploiting motion triggered attention were developed and compared with MPEG AVC/H.264 encoder with various settings for different bitrate levels. For the sequences with high motion activity our algorithm provides up to 8% bitrate savings.
Toward A Mobile Platform For Pervasive Games, Inseok Hwang, Youngki Lee, Taiwoo Park, Junehwa Song
Toward A Mobile Platform For Pervasive Games, Inseok Hwang, Youngki Lee, Taiwoo Park, Junehwa Song
Research Collection School Of Computing and Information Systems
Emerging pervasive games will be immersed into real-life situations and leverage new types of contextual interactions therein. For instance, a player’s punching gesture, running activity, and fast heart rate conditions can be used as the game inputs. Although the contextual interaction is the core building blocks of pervasive games, individual game developers hardly utilize a rich set of interactions within a game play. Most challenging, it is significantly difficult for developers to expect dynamic availability of input devices in real life, and adapt to the situation without system-level support. Also, it is challenging to coordinate its resource use with other …
Automatic Compositional Verification Of Timed Systems, Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong, Étienne André
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
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
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, …
Generating Minimal T-Wise Test Suites, Luis C. Gutierrez, Carlos Nieto, Francisco Zapata, Martine Ceberio
Generating Minimal T-Wise Test Suites, Luis C. Gutierrez, Carlos Nieto, Francisco Zapata, Martine Ceberio
COURI Symposium Abstracts, Summer 2012
As the use of computing devices increases every day, users rely on the adequate functioning of software. When software is not tested properly, it can yield erroneous information or a complete failure of the system. The NIST estimates that defective software cost the United States economy close to $60 billion a year. Therefore, there is a need to develop software testing techniques that are time and cost effective. Fully testing software under all possible combinations of parameters values cannot be reduced. However, testing can focus on covering all combinations of subsets of parameters and empirical data shows that doing so …
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
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 …
Formal Analysis Of Pervasive Computing Systems, Yan Liu, Xian Zhang, Jin Song Dong, Yang Liu, Jun Sun, Jit Biswas, Mounir Mokhtari
Formal Analysis Of Pervasive Computing Systems, Yan Liu, Xian Zhang, Jin Song Dong, Yang Liu, Jun Sun, Jit Biswas, Mounir Mokhtari
Research Collection School Of Computing and Information Systems
Pervasive computing systems are heterogenous and complex as they usually involve human activities, various sensors and actuators as well as middleware for system controlling. Therefore, analyzing such systems is highly nontrivial. In this work, we propose to use formal methods for analyzing pervasive computing systems. Firstly, a formal modeling framework is proposed to cover the main characteristics of pervasive computing systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts etc.) and propose their specifications as safety and liveness properties. Finally, we demonstrate our ideas using a case study of a …
A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong
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.
Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong
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 hence interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesize a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed CSP, a language capable of specifying hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present an algorithm for efficient parameter synthesis that behaves well in practice.
Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun
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 …
Mydeal: The Context-Aware Urban Shopping Assistant, Kartik Muralidharan, Swapna Gottipati, Jing Jiang, Narayan Ramasubbu, Rajesh Krishna Balan
Mydeal: The Context-Aware Urban Shopping Assistant, Kartik Muralidharan, Swapna Gottipati, Jing Jiang, Narayan Ramasubbu, Rajesh Krishna Balan
Research Collection School Of Computing and Information Systems
A common problem in large Urban cities, of the sort seen in Asia, is the huge number of retail options available in the city. In particular, it is not uncommon to find multiple malls, each with hundreds of stores inside, just a short distance from each other in almost every part of these cities. These factors make it incredibly hard for consumers to identify stores of interest to them in any particular mall.In response, a number of shopping assistance applications have been created for mobile phones.However, these applications mostly just allow users to know which stores are where or to …