Software Engineering Commons^™

Data Mining For Software Engineering, Tao Xie, Suresh Thummalapenta, David Lo, Chao Liu

Research Collection School Of Computing and Information Systems

To improve software productivity and quality, software engineers are increasingly applying data mining algorithms to various software engineering tasks. However, mining SE data poses several challenges. The authors present various algorithms to effectively mine sequences, graphs, and text from such data.

Formal Verification Of Scalable Nonzero Indicators, Jun Sun, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen, Yanhong A. Liu

Research Collection School Of Computing and Information Systems

Concurrent algorithms are notoriously difficult to design correctly, and high performance algorithms that make little or no use of locks even more so. In this paper, we describe a formal verification of a recent concurrent data structure Scalable NonZero Indicators. The algorithm supports incrementing, decrementing, and querying the shared counter in an efficient and linearizable way without blocking. The algorithm is highly non-trivial and it is challenging to prove the correctness. We have proved that the algorithm satisfies linearizability, by showing a trace refinement relation from the concrete implementation to its abstract specification. These models are specified in CSP and …

Identifying Bug Signatures Using Discriminative Graph Mining, Hong Cheng, David Lo, Yang Zhou, Xiaoyin Wang, Xifeng Yan

Research Collection School Of Computing and Information Systems

Bug localization has attracted a lot of attention recently. Most existing methods focus on pinpointing a single statement or function call which is very likely to contain bugs. Although such methods could be very accurate, it is usually very hard for developers to understand the context of the bug, given each bug location in isolation. In this study, we propose to model software executions with graphs at two levels of granularity: methods and basic blocks. An individual node represents a method or basic block and an edge represents a method call, method return or transition (at the method or basic …

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

Research Collection School Of Computing and Information Systems

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

Poster Abstract: Beamcast: Harnessing Beamforming Capabilities For Link Layer Multicast, Souvik Sen, Rahul Ghosh, Jie Xiong, Romit Roy Choudhury

Research Collection School Of Computing and Information Systems

Wireless multicast is an important service primitive for emerging applications such as live video, streaming audio and content telecasts. Transmission rate in such a link layer multicast is bottlenecked by the rate of the weakest client, leading to channel under-utilization. Attempts to increase the data rate results in lower reliability (due to higher bit error rate) and higher unfairness. This poster utilizes smart beamforming antennas to improve multicast performance in wireless LANs. The main idea is to satisfy majority of the (strong) clients with a high-rate omnidirectional transmission, followed by high-rate directional transmission(s) to cover the weaker ones. By selecting …

Automatic Steering Of Behavioral Model Inference, David Lo, Leonardo Mariani, Mauro Pezze

Research Collection School Of Computing and Information Systems

Many testing and analysis techniques use finite state models to validate and verify the quality of software systems. Since the specification of such models is complex and time-consuming, researchers defined several techniques to extract finite state models from code and traces. Automatically generating models requires much less effort than designing them, and thus eases the verification and validation of large software systems. However, when models are inferred automatically, the precision of the mining process is critical. Behavioral models mined with imprecise processes can include many spurious behaviors, and can thus compromise the results of testing and analysis techniques that use …

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

Research Collection School Of Computing and Information Systems

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

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

Research Collection School Of Computing and Information Systems

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

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

Research Collection School Of Computing and Information Systems

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

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

Research Collection School Of Computing and Information Systems

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

Free, Source-Code-Available, Or Proprietary: An Ethically Charged, Context-Sensitive Choice, Marty J. Wolf, Keith W. Miller, Frances Grodzinsky

School of Computer Science & Engineering Faculty Publications

We demonstrate that different categories of software raise different ethical concerns with respect to whether software ought to be Free Software or Proprietary Software. We outline the ethical tension between Free Software and Proprietary Software that stems from the two kinds of licenses. For some categories of software we develop support for normative statements regarding the software development landscape. We claim that as society's use of software changes, the ethical analysis for that category of software must necessarily be repeated. Finally, we make a utilitarian argument that the software development environment should encourage both Free Software and Proprietary Software to …

Mferio: The Design And Evaluation Of A Peer-To-Peer Mobile Payment System, Rajesh Krishna Balan, Narayanasamy Ramasubbu, Komsit Prakobphol, Nicolas Christin, Jason Hong

Research Collection School Of Computing and Information Systems

In this paper, we present the design and evaluation of a near-field communication-based mobile p2p payment application, called mFe-rio, that is designed to replace cash-based transactions. We first identify design criteria that payment systems should satisfy and then explain how mFerio, relative to those criteria, improves on the limitations of cash-based systems. We next describe mFerio's implementation and user interface design, focusing on the balance between usability and security. Finally, we present the results of a two-phase user study, involving a total of 104 people, that shows that mFerio has low cognitive load and is also fast, accurate, and easy …

Adaptive In-Network Processing For Bandwidth And Energy Constrained Mission-Oriented Multi-Hop Wireless Networks, Sharanya Eswaran, Matthew Johnson, 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 widely used in sensor networks to reduce the communication overhead. In many tactical and stream-oriented wireless network applications, both link bandwidth and node energy are critically constrained resources and in-network processing itself imposes non-negligible computing cost. In this work, we have developed a unified and distributed closed-loop control framework that computes both a) the optimal level of sensor stream compression performed by a forwarding node, and b) the best set of nodes where the stream processing operators should be deployed. Our framework extends the Network Utility Maximization (NUM) paradigm, …

Non-Redundant Sequential Rules - Theory And Algorithm, David Lo, Siau-Cheng Khoo, Limsoon Wong

Research Collection School Of Computing and Information Systems

A sequential rule expresses a relationship between two series of events happening one after another. Sequential rules are potentially useful for analyzing data in sequential format, ranging from purchase histories, network logs and program execution traces. In this work, we investigate and propose a syntactic characterization of a non-redundant set of sequential rules built upon past work on compact set of representative patterns. A rule is redundant if it can be inferred from another rule having the same support and confidence. When using the set of mined rules as a composite filter, replacing a full set of rules with a …

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 …

Classification Of Software Behaviors For Failure Detection: A Discriminative Pattern Mining Approach, David Lo, Hong Cheng, Jiawei Han, Siau-Cheng Khoo, Chengnian Sun

Research Collection School Of Computing and Information Systems

Software is a ubiquitous component of our daily life. We often depend on the correct working of software systems. Due to the difficulty and complexity of software systems, bugs and anomalies are prevalent. Bugs have caused billions of dollars loss, in addition to privacy and security threats. In this work, we address software reliability issues by proposing a novel method to classify software behaviors based on past history or runs. With the technique, it is possible to generalize past known errors and mistakes to capture failures and anomalies. Our technique first mines a set of discriminative features capturing repetitive series …

Incremental Validation Of Formal Specifications, Paul S. Corwin

Master's Theses

This thesis presents a tool for the mechanical validation of formal software specifications. The tool is based on a novel approach to incremental validation. In this approach, small-scale aspects of a specification are validated, as part of the stepwise refinement of a formal model.

The incremental validation technique can be considered a form of "lightweight" model checking. This is in contrast to a "heavyweight" approach, wherein an entire large-scale model is validated en masse.

The validation tool is part of a formal modeling and specification language (FMSL), used in software engineering instruction. A lightweight, incremental approach to validation is beneficial …

The Impact Of Process Choice In High Maturity Environments: An Empirical Analysis, Narayanasamy Ramasubbu, Rajesh Krishna Balan

Research Collection School Of Computing and Information Systems

We present the results of a three year field study of the software development process choices made by project teams at two leading offshore vendors. In particular, we focus on the performance implications of project teams that chose to augment structured, plan-driven processes to implement the CMM level-5 Key Process Areas (KPAs) with agile methods. Our analysis of 112 software projects reveals that the decision to augment the firm-recommended, plan-driven approach with improvised, agile methods was significantly affected by the extent of client knowledge and involvement, newness of technology, and the project size. Furthermore this decision had a significant and …

Automatic Mining Of Functionally Equivalent Code Fragments Via Random Testing, Lingxiao Jiang, Zhendong Su

Research Collection School Of Computing and Information Systems

Similar code may exist in large software projects due to some common software engineering practices, such as copying and pasting code and n-version programming. Although previous work has studied syntactic equivalence and small-scale, coarse-grained program-level and function-level semantic equivalence, it is not known whether significant fine-grained, code-level semantic duplications exist. Detecting such semantic equivalence is also desirable because it can enable many applications such as code understanding, maintenance, and optimization. In this paper, we introduce the first algorithm to automatically mine functionally equivalent code fragments of arbitrary size - down to an executable statement. Our notion of functional equivalence is …

Concernlines: A Timeline View Of Co-Occurring Concerns, Christoph Treude, Margaret-Anne Storey

Research Collection School Of Computing and Information Systems

Understanding the evolution of a software system requires understanding how information about the release history, non-functional requirements and project milestones relates to functional requirements on the software components. This short paper describes a new tool, called CONCERNLINES, that supports this cognitive process by visualizing co-occurring concerns over time.

How Tagging Helps Bridge The Gap Between Social And Technical Aspects In Software Development, Christoph Treude, Margaret-Anne Storey

Research Collection School Of Computing and Information Systems

Empirical research on collaborative software development practices indicates that technical and social aspects of software development are often intertwined. The processes followed are tacit and constantly evolving, thus not all of them are amenable to formal tool support. In this paper, we explore how ldquotaggingrdquo, a lightweight social computing mechanism, is used to bridge the gap between technical and social aspects of managing work items. We present the results from an empirical study on how tagging has been adopted and adapted over the past two years of a large project with 175 developers. Our research shows that the tagging mechanism …

A Video Manager, Nicholas Omann

Honors Capstones

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

A Framework For Using Modeling And Simulation-Based Methods In Support Of Project Management In A U.S. Department Of Defense Enterprise Architecture Framework Environment, Jose Leprout Bricio-Neto

Computational Modeling & Simulation Engineering Theses & Dissertations

The Enterprise Architecture, Analysis and Project Management (EA2PM) framework developed and proposed in this study enables better evaluation of the ability for enterprise architects, project managers and analysts to share system data using their own domain-specific software tools with a focus on the capability to automatically generate a discrete-event simulation model. EA2PM framework is based on applying a Knowledge Management (KM) construct to establish data and information boundaries, and developing a methodology that allows for high levels of traceability from system architecture's environmental factors through assessment of data and information mediation across domains within a KM system.

An application of …

Improving Automated Requirements Trace Retrieval Through Term-Based Enhancement Strategies, Xuchang Zou

College of Computing and Digital Media Dissertations

Requirements traceability is concerned with managing and documenting the life of requirements. Its primary goal is to support critical software development activities such as evaluating whether a generated software system satisfies the specified set of requirements, checking that all requirements have been implemented by the end of the lifecycle, and analyzing the impact of proposed changes on the system. Various approaches for improving requirements traceability practices have been proposed in recent years. Automated traceability methods that utilize information retrieval (IR) techniques have been recognized to effectively support the trace generation and retrieval process. IR based approaches not only significantly reduce …

Pipelined Apache Http Server, Kevin Le

Master's Theses

Web servers often become overloaded with irregular surges in web traffic. Several techniques have been explored to cope with these overloads such as distributing load throughout different servers. This thesis presents Pipelined Apache HTTP Server, a modified version of the Apache Software Foundation’s HTTP Server that utilizes a pipelined execution of Apache’s request cycle. We discuss Apache’s original architecture, the modifications necessary for implementation of pipelined execution, and analyze its run time. Ultimately, we hoped to increase throughput of Apache but fall short because of unbalanced request phases and pipelining overhead.

Efficient Mining Of Closed Repetitive Gapped Subsequences From A Sequence Database, Bolin Ding, David Lo, Jiawei Han, Siau-Cheng Khoo

Research Collection School Of Computing and Information Systems

There is a huge wealth of sequence data available, for example, customer purchase histories, program execution traces, DNA, and protein sequences. Analyzing this wealth of data to mine important knowledge is certainly a worthwhile goal. In this paper, as a step forward to analyzing patterns in sequences, we introduce the problem of mining closed repetitive gapped subsequences and propose efficient solutions. Given a database of sequences where each sequence is an ordered list of events, the pattern we would like to mine is called repetitive gapped subsequence, which is a subsequence (possibly with gaps between two successive events within it) …

The Digital Wallet: Opportunities And Prototypes, Rajesh Krishna Balan, Narayanasamy Ramasubbu

Research Collection School Of Computing and Information Systems

Example digital wallet applications support secure P2P mobile cash transactions and alleviate point-of-sale confusion for consumers using multiple payment, discount, and loyalty cards.

A Social Relation Aware Routing Protocol For Mobile Ad Hoc Networks, Jisun An, Yangwoo Ko, Dongman Lee

Research Collection School Of Computing and Information Systems

In this paper, we propose a social relation aware routing protocol for mobile ad hoc networks, which is designed for content sharing mobile social applications. Since a content can be shared by a group of users who have similar interests, the similarity of users' interests is a good metric to predict who will consume which contents. Shared interests can be exploited in routing and replication of content request and reply to achieve enhanced efficacy in content sharing. Since routing determines which content will be forwarded by whom, a route selected based on similarity of interest increases the utilization of contents …

Programmable Presence Virtualization For Next-Generation Context-Based Applications, Arup Acharya, Nilanjan Banerjee, Dipanjan Chakraborty, Koustuv Dasgupta, Archan Misra, Shachi Sharma, Xiping Wang, Charles P. Wright

Research Collection School Of Computing and Information Systems

Presence, broadly defined as an event publish-notification infrastructure for converged applications, has emerged as a key mechanism for collecting and disseminating context attributes for next-generation services in both enterprise and provider domains. Current presence-based solutions and products lack in the ability to a) support flexible user-defined queries over dynamic presence data and b) derive composite presence from multiple provider domains. Accordingly, current uses of context are limited to individual domains/organizations and do not provide a programmable mechanism for rapid creation of context-aware services. This paper describes a presence virtualization architecture, where a virtualized presence server receives customizable queries from multiple …

Server-Assisted Context-Dependent Pervasive Wellness Monitoring, Archan Misra, Ben Falchuk, Shoshana Loeb

Research Collection School Of Computing and Information Systems

Recent research on remote health monitoring solutions has focused largely on developing context-dependent, streamprocessing capabilities on a personal mobile hub (typically, a cellphone) for energy-efficient transmission of data collected from a set of body-worn medical sensors. In this paper, we argue that commercial deployment of such pervasive wellness monitoring will require the extension of such ‘context dependency’ to the process of data collection (from the sensors to the mobile device) as well. In particular, the utilization of an individuals non-medical activity context, by the cellphone, in coordination with a backend server, is posited to be the key to supporting important …