| School of Computer Science and Engineering (CRICOS Provider No. 00098G)

Technical Reports

Send queries to reports@cse.unsw.edu.au.

TR #	Title	Author(s) and Affiliation(s)	Abstract

0816

Probabilistic Reverse Nearest Neighbor Queries on Uncertain Data

Muhammad Aamir Cheema
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: macheema@cse.unsw.edu.au

Xuemin Lin
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: lxue@cse.unsw.edu.au

Wei Wang
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: weiw@cse.unsw.edu.au

Wenjie Zhang
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: zhangw@cse.unsw.edu.au

Jian Pei
School of Computer Science
Simon Fraser University
Burnaby, BC Canada
E-mail: jpei@cs.sfu.ca

Uncertain data is inherent in many important applications where the exact data values are not known. While many types of queries on uncertain data have been studied, reverse nearest neighbor query on uncertain data is still an open problem. In this paper, we formalize the problem of probabilistic reverse nearest neighbor query based on the possible worlds semantics. We propose an efficient method that processes such queries efficiently. The key technique innovation is several novel pruning methods that exploit various properties of the problem. Extensive experiment demonstrates that our algorithm is highly efficient and scalable.

0815

Context-Aware Channel Coordination for Vehicular Communications

Zhe Wang
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: zhewang@cse.unsw.edu.au

Mahbub Hassan
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: mahbub@cse.unsw.edu.au

Vehicular communication could be the much anticipated breakthrough against the unabated fatal and near fatal accidents that continue to threaten the public safety on our roads. The same technology is also expected to concurrently support a range of non-safety applications including real-time traffic information, mobile entertainment, and access to the Internet. The standard has specified an explicit multi-channel structure whereby safety and non-safety transmissions will occur at different channels. Consequently, a vehicle with a conventional single-radio transceiver will need to continuously switch between the safety and the non-safety modes of operation. The interval spent in the safety mode (safety interval) at each cycle is a critical parameter that directly limits the availability of the technology for commercial use. Using simulation, we show that the safety interval required to satisfy the reliability of safety applications is a function of traffic density on the road. Given that in most roads traffic density is expected to vary during the day, we propose dynamic adjustment of the safety interval based on the traffic context. To further motivate the concept of traffic aware vehicular communications, we evaluate the performance of three dynamic channel coordination algorithms using empirical traffic data collected from the roads around the city of Sydney, Australia. A key finding is that, the time-of-day is an effective context that can prevent a vehicular radio from keep running in the safety mode unnecessarily, thereby enhancing the commercial opportunity of the technology. We further demonstrate that the use of the location context can dramatically improve the performance of the basic time-of-day algorithms.

0814

How Much of DSRC is Available for Non-Safety Use?

The Dedicated Short Range Communication (DSRC) technology is currently being standardized by the IEEE to enable a range of communication-based automotive safety applications. However, for DSRC to be cost-effective, it is important to accommodate commercial non-safety use of the spectrum as well. The co-existence of safety and non-safety is achieved through a periodic channel switching scheme whereby access to DSRC alternates between these two classes of applications. In this paper, we propose a framework that links the non-safety share of DSRC as effected by the channel switching to the performance requirements of safety applications. Using simulation experiments, we analyze the non-safety opportunity in the DSRC under varied road traffic conditions. We find that non-safety use of DSRC may have to be severely restricted during peak hours of traffic to insure that automotive safety is not compromised. Our study also sheds interesting insights into how simple strategies, e.g., optimizing the message generation rate of the safety applications, can significantly increase the commercial opportunities of DSRC. Finally, we find that adaptive schemes that can dynamically adjust the switching parameters in response to observed traffic conditions may help in maximizing the commercial use of DSRC.

0812

A Measurement Study of Bandwidth Predictability in Mobile Communication Networks

Jun Yao, Salil S. Kanhere, Mahbub Hassan
School of Computer Science and Engineering,
University of New South Wales,
Australia
Email: {jyao, salilk, mahbub}@cse.unsw.edu.au

While bandwidth predictability has been well studied in static environments, it remains largely unexplored in the context of mobile computing. To gain a deeper understanding of this important issue in the mobile environment, we conducted an eight-month measurement study consisting of 71 repeated trips along a 23Km route in Sydney under typical driving conditions. To account for the network diversity, we measure bandwidth from two independent cellular providers implementing the popular High-Speed Downlink Packet Access (HSDPA) technology in two different peak access rates (1.8 and 3.6 Mbps). Interestingly, we observe no significant correlation between the bandwidth signals at different points in time within a given trip. This observation eventually leads to the revelation that the popular time series models, e.g. the Autoregressive and Moving Average, typically used to predict network traffic in static environments are not as effective in capturing the regularity in mobile bandwidth. Although the bandwidth signal in a given trip appears as a random white noise, we are able to detect the existence of patterns by analyzing the distribution of the bandwidth observed during the repeated trips. We quantify the bandwidth predictability reflected by these patterns using tools from information theory, entropy in particular. The entropy analysis reveals that the bandwidth uncertainty may reduce by as much as 46% when observations from past trips are accounted for. We further demonstrate that the bandwidth in mobile computing appears more predictable when location is used as a context. All these observations are consistent across multiple independent providers offering different data transfer rates using possibly different networking hardware.

0811

Interference Analysis and Channel Assignment in Multi-Radio Multi-Channel Wireless Mesh Networks

Anjum Naveed
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: anaveed@cse.unsw.edu.au

Salil Kanhere
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: salilk@cse.unsw.edu.au

In a typical Wireless Mesh Network (WMN), the links that interfere with a particular link can be broadly classified into two categories depending on their geometric relationships: coordinated and non-coordinated links. In this paper, we analytically quantify the impact of both kind of interfering links on transmission losses. Our analysis shows that compared to coordinated links, the non-coordinated links result in significantly lower throughput and an unfair distribution of channel capacity amongst interfering links. We hypothesize that channel assignment in multi-radio multi-channel WMNs can be effective in significantly reducing the interference caused by the non-coordinated links. We prove that the channel assignment problem based on this hypothesis is NP-Hard. We propose a novel two-phase heuristic channel assignment protocol referred as Cluster-Based Channel Assignment Protocol (CCAP). The protocol logically partitions the network into non-overlapping clusters. In the first phase, nodes within a cluster are assigned to a common channel with orthogonal channels being used in adjacent clusters. The inter-cluster links are assigned channels with the aim of minimizing non-coordinated interference. The second phase of CCAP exploits channel diversity to sub-divide each cluster into multiple interference domains, thereby increasing the capacity of individual links. Simulation-based evaluations demonstrate that CCAP can achieve twice the aggregate network throughput as compared to existing channel assignment protocols, while ensuring a fair distribution of capacity amongst the links.

0810

Mashups for Data Integration: An Analysis

Giusy Di Lorenzo
Dipartimento di Informatica e Sistemistica
University Federico II
Via Claudio, 21
80125 Napoli, Italy
E-mail: giusy.dilorenzo@unina.it

Hakim Hacid
School of Computer Science Engineering
University of new south wales
Sydney, NSW 2052, Australia
E-mail: hakimh@cse.unsw.edu.au

Hye-young Paik
School of Computer Science and Engineering
University of new south wales
Sydney, NSW 2052, Australia
E-mail: hpaik@cse.unsw.edu.au

Boualem Benatallah
School of Computer Science and Engineering
University of new south wales
Sydney, NSW 2052, Australia
E-mail: boualem@cse.unsw.edu.au

Mashup is a new application development approach that allows users aggregate multiple services, each serving its own purpose, to create a service that serves a new purpose. Even if the Mashup approach opens new and broader opportunities for data/service consumers, the development process still requires the users to know, not only understand how to write code using languages, but also how to use the different Web APIs from all services. The objective of this study is to analyze the richnesses and weaknesses of the Mashup tools. In particular, we identify the behaviors and characteristics of general Mashup applications and analyze the tools with respect to the key aspects from the Mashup applications. We believe that this kind of study is important to drive future contributions in this emerging area where a lot of research and application fields, such as databases, user machine interaction, etc., can meet.

0809

Mix and Test Counting in Preferential Electoral Systems

Roland Wen, Richard Buckland
School of Computer Science and Engineering
University of New South Wales
Sydney, NSW 2052, Australia
E-mail: {rolandw,richardb}@cse.unsw.edu.au

Although there is a substantial body of work on online voting schemes that prevent bribery and coercion of voters, as yet there are few suitable schemes for counting in the alternative vote and single transferable vote preferential systems. Preferential systems are prone to bribery and coercion via signature attacks. This is an issue for online elections in Australia, where all parliamentary elections use these preferential systems. We present the Mix and Test Counting scheme, a preferential counting protocol that is resistant to signature attacks. For the alternative vote, it reveals no information apart from the identity of the winning candidate. For the single transferable vote, it reveals additional anonymised counting information. However the only candidates identified are the winning candidates.

0808

Herbrand Analysis of Some Second-order Theories with Weak Set Existence Principles

Chung Tong Lee
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: ctlee@cse.unsw.edu.au

Aleksandar Ignjatovic
School of Computer Science and Engineering
University of New South Wales, and
NICTA
NSW2052, Australia
Email: ignjat@cse.unsw.edu.au

We present a proof-theoretic analysis of some second-order theories of binary strings which were introduced in [5]. The core of these theories contains, besides finitely many open axioms for basic operations on strings, only a weak comprehension axiom schema. In such theories, a collection W can be defined to play the role of natural numbers. W is given as the intersection of all sets containing the empty string and closed under the two successor functions S0 and S1. We characterize the classes of functions which provably map W into itself and whose graphs are defined by formulas of an appropriate bounded quantifier complexity. For theories with weak comprehension schemas, this notion corresponds naturally to that of provably recursive functions for arithmetic theories. The techniques of Herbrand analysis developed by Sieg in [8] and [9] allow us to prove that these classes match up with levels of the polynomial-time hierarchy.

0807

Masked Ballot Receipt-Free Elections

Roland Wen
School of Computer Science and Engineering
University of New South Wales
Sydney, NSW 2052, Australia
E-mail: rolandw@cse.unsw.edu.au

Online election schemes mitigate bribery and coercion by precluding the generation of receipts that can prove how voters voted. In order to guarantee that each voter's public election data appears ambiguous, existing approaches to receipt-free schemes rely on problematic assumptions when voters cast ballots. We take a new approach by using the novel properties of the Damgard-Jurik cryptosystem to construct Masked Ballot, a receipt-free scheme that avoids such assumptions during the election. The Masked Ballot scheme assumes the existence of untappable channels for a trusted registrar to send private masking values to voters before the election, but does not require these channels during the election. Voters cast ballots over completely public channels without relying on untappability, anonymity or trusted devices.

0806

Towards Agile Service-oriented Business Systems: A Directive-oriented Pattern Analysis Approach

Soo Ling Lim
School of Computer Science and Engineering
University of New South Wales, and
NICTA, Australian Technology Park
Sydney, Australia
Email: slim@cse.unsw.edu.au

Fuyuki Ishikawa, Eric Platon
National Institute of Informatics
Tokyo, Japan
Email: {f-ishikawa,platon}@nii.ac.jp

Karl Cox
NICTA, Australian Technology Park
Sydney, Australia
Email: Karl.Cox@nicta.com.au

Volatile requirements should be managed such that changes can be introduced into the system in a quick and structured way. This paper presents Directive-oriented Pattern Analysis (DoPA), a requirements engineering approach that handles volatile requirements by managing the coupling between business intentions and service integration. The key insight is to utilise services as commodities via service choreography patterns. DoPA captures differentiating enterprise intentions as Directives, while using patterns to handle common business needs. This enables the notion of declarative configuration of services to achieve business agility.

0805

Adapting the Weighted Backtrack Estimator to Conflict Driven Search

Shai Haim
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: shaih@cse.unsw.edu.au

Toby Walsh
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: tw@cse.unsw.edu.au

Modern SAT solvers present several challenges to estimate search cost including coping with nonchronological backtracking and learning. We present a method to adapt an existing algorithm for estimating the size of a search tree to deal with these challenges. We show the effectiveness of this method using random and structured problems.

0804

Analysis of Per-node Traffic Load in Multi-hop Wireless Sensor Networks

Quan Jun Chen, Salil S. Kanhere, Mahbub Hassan
School of Computer Science and Engineering
University of New South Wales, Australia
E-mail: {quanc, salilk, mahbub}@cse.unsw.edu.au

The energy expended by sensor nodes in reception and transmission of data packets makes up a significant quantum of their total energy consumption. Consequently, models that can accurately predict the communication traffic load of a sensor node are critical for designing effective and efficient sensor network protocols. In this paper, we present an analytical model for estimating the per-node traffic load in a multi-hop wireless sensor network, where the nodes sense the environment periodically and forwards the data packets to the sink using greedy geographic routing. The analysis incorporates the idealistic circular coverage radio model as well as a realistic model, log-normal shadowing. Our results confirm that, irrespective of the radio models, the traffic load generally increases as a function of the node's proximity to the sink. In the immediate vicinity of the sink, however, the two radio models yield quite contrasting results. The ideal radio model reveals the existence of a volcano region near the sink, where the traffic load drops significantly. On the contrary, with the log-normal shadowing model, the opposite effect is observed, wherein the traffic load actually increases at a much higher rate as one approaches the sink resulting in the formation of a mountain peak. The results from our analysis are validated by extensive simulations. The simulations also demonstrate that our results are applicable in more realistic environments, which do not conform to the simplifying assumptions made in the analysis for mathematical tractability.

0803

Automatic collection of fuel prices from a network of mobile cameras

Yi Fei Dong, Salil Kanhere, Chun Tung Chou
School of Computer Science and Engineering
The University of New South Wales
Sydney, NSW 2052, Australia
Email: {ydon,salilk,ctchou}@cse.unsw.edu.au

Nirupama Bulusu
Portland State University, USA
Email: nbulusu@cs.pdx.edu

It is an undeniable fact that people want information. Unfortunately, even in today's highly automated society, a lot of the information we desire is still manually collected. An example is fuel prices where websites providing fuel price information either send their workers out to manually collect the prices or depend on volunteers manually relaying the information. This paper proposes a novel application of wireless sensor networks to automatically collect fuel prices from camera images of road-side price board (billboard) of service (or gas) stations. Our system exploits the ubiquity of mobile phones that have cameras as well as users contributing and sharing data. In our proposed system, cameras of contributing users will be automatically triggered when they get close to a service station. These images will then be processed by computer vision algorithms to extract the fuel prices. In this paper, we will describe the system architecture and present results from our computer vision algorithms. Based on 52 images, our system achieves a hit rate of 92.3% for correctly detecting the fuel price board from the image background and reads the prices correctly in 87.7% of them. To the best of our knowledge, this is the first instance of a sensor network being used for collecting consumer pricing information

0802

ERTP: Energy-efficient and Reliable Transport Protocol for Data Streaming in Wireless Sensor Networks

Tuan Le
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: dtle@cse.unsw.edu.au

Wen Hu
CSIRO ICT Centre
Brisbane, Australia
E-mail: wen.hu@csiro.au

Peter Corke
CSIRO ICT Centre
Brisbane, Australia
E-mail: peter.corke@csiro.au

Sanjay Jha
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sanjay@cse.unsw.edu.au

Emerging data streaming applications in Wireless Sensor Networks require re- liable and energy-efficient transport protocols. Our recent Wireless Sensor Network deployment in the Burdekin delta, Australia for water monitoring is one such example. Our application involved streaming sensed data such as pressure readings, water flow rate, and salinity readings periodi- cally from many scattered sensors to the sink node which in turn relayed them via an IP network to a remote site for archiving, processing and presentation. While latency is not a primary concern in this class of application (the sample rate is usually in terms of minutes or hours), energy-efficiency is. Long-term operation and reliable delivery of the sensed data to the sink are also desirable. In this paper, we discuss ERTP, an Energy-efficient and Reliable Transport Protocol for Wireless Sensor Networks. ERTP is designed for data streaming applications, in which sensor readings are transmitted from one or more sensor sources to a base station (or sink). ERTP uses a statistical reliability metric which ensures the number of data packets delivered to the sink exceeds the defined threshold. Using a statistical reliability metric when designing a reliable transport protocol guarantees the delivery of adequate information to the users, and reduces the number of transmissions when compared to absolute reliability. To reduce energy-consumption, ERTP uses hop-by-hop Implicit Acknowl- edgment with dynamically updated retransmission timeout for loss recovery. In multihop wireless networks, the transmitter can overhear a forwarding trans- mission and interpret it as an Implicit Acknowledgment. However, Implicit Acknowledgment timeout depends on the time taken a packet to be forwarded by the downstream node. Thus, a dynamic retransmission timeout estimation is crucial for the class of Hop-by-Hop Implicit Acknowledgment transport pro- tocol. By combining statistical reliability and hop-by-hop Implicit ACK loss re- covery, ERTP can provide the reliability to application users with the mini- mal energy-expense. Our extensive discrete event simulations and experimental evaluations show that ERTP is significantly more energy-efficient than current approaches and can reduce energy consumption by more than 50% when com- pared to current approaches. Consequently, sensors are more energy-efficient and the lifespan of the unattended WSN is increase

0801

Analytical Evaluation of the 802.11 Wireless Broadcast under Saturated Conditions

Zhe Wang and Mahbub Hassan
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: {zhewang, mahbub}@cse.unsw.edu.au

The popular IEEE 802.11 wireless networking standard has been traditionally used for unicast communications. There is, however, a recent trend in harnessing the broadcast capability of the standard in a range of monitoring and safety related applications, e.g., transportation safety and vehicular traffic management. As this trend continues, models that accurately predict the performance of the 802.11 broadcast will be increasingly useful. Although unicast modelling received considerable attention, analytical evaluation of the broadcast protocol remained relatively unexplored. Using a simple one-dimensional discrete time Markov chain, we analyse the reliability and throughput performance of the IEEE 802.11 broadcast communications for saturated traffic conditions. The model is validated by means of an independent commercial simulator. Using the proposed model, we provide an extensive performance analysis of the 802.11 broadcast communications. The analysis allows us to study the tradeoff between the communication reliability and the system throughput of a local area wireless broadcast network. The throughput performance of broadcast is compared with that of the unicast under different network sizes and different combinations of 802.11 protocol parameters.

0723

Tool support for verifying trace inclusion with Uppaal

Timothy Bourke
NICTA, Kensington Laboratory, and
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: tbourke@cse.unsw.edu.au

Arcot Sowmya
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sowmya@cse.unsw.edu.au

Trace inclusion against a deterministic Timed Automata can be verified with the Uppaal model checking tool by constructing a test automaton that snares illegal synchronisation possibilities. Constructing the automaton manually is tedious and error prone. This paper presents a tool that does it automatically for a subset of Uppaal models. Certain features of Uppaal, namely selection bindings and channel arrays, complicate the construction. We first formalise these features, and then show how to incorporate them directly in the testing construction. To do so we limit the forms of subscript that can be used to specify synchronisations; striving for a balance between practicability and program complexity. Unfortunately, some combinations of selection bindings and universal quantifiers cannot be effectively manipulated. The tool does not yet validate the determinism requirements, nor handle committed states or broadcast channels.

0722

Time-Aware Content Summarization of Data Streams

Quang-Khai Pham, R´egis Saint-Paul, Boualem Benatallah
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

Guillaume Raschia, Noureddine Mouaddib
Atlas Group
LINA at University of Nantes
Nantes, France

Major media companies such as The Financial Times, the Wall Street Journal or Reuters generate huge amounts of textual news data on a daily basis. Mining frequent patterns in this mass of information is critical for knowledge workers such as financial analysts, stock traders or economists. Using existing frequent pattern mining (FPM) algorithms for the analysis of news data is difficult because of the size and lack of structuring of the free text news content. In this article, we propose a Time-Aware Content Summarization algorithm to support FPM in financial news data. The summary allows a concise representation of large volume of data by taking into account the expert's peculiar interest. The summary also preserves the news arrival time information which is essential for FPM algorithms. We experimented the proposed approach on Reuters news data and integrated it into the Streaming TEmporAl Data (STEAD) analysis framework for interactive discovery of frequent pattern.

0721

Process Spaceship: Discovering Process Views in Process Spaces

Hamid Reza Motahari-Nezhad, R´egis Saint-Paul, Boualem Benatallah
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

Fabio Casati, Periklis Andritsos
University of Trento
Trento, Italy

Process and service execution analysis is a key endeavour for enterprises. Such analysis requires observing and correlating messages related to process and service executions, meaning that identifying if messages belong to the same process instance or service execution. A first challenge is that message correlation is subjective, i.e., depends on the purpose of the analysis and on the perspective of the analyst. Another challenge lies in the huge space of possible correlations between messages, which can be built based on different combinations of message attributes. In this paper, we consider process and service execution data as a process space, and different ways of performing correlations as process views that are views over the process space. We propose methods, by adopting a level-wise approach, and heuristics to identify the set of interesting process views and present a visual, interactive environment that allows users to efficiently navigate through the views identified over a process space. The experiments show the viability and efficiently of the approach on both synthetic and real-world service logs.

0719

Experience and Trust: A Sytems-Theoretic Approach

Rex Kwok and Norman Foo
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {rkwok|norman}@cse.unsw.edu.au

Abhaya Nayak
Department of Computing
Division of Information and Communication Sciences
Macquarie University, NSW 2109, Australia
Email: abhaya@ics.mq.edu.au

The core of scientific theories are laws. These laws often make use of theoretical terms, linguistic entities which do not directly refer to observables. There is therefore no direct way of determining which theoretical assertions are true. This suggests that multiple theories may exist which are incompatible with one another but compatible with all possible observations. Since such theories make the same empirical claims, empirical tests cannot be used to differentiate or rank such theories. One property that has been suggested for evaluating rival theories is coherence. This was investigated qualitatively until we introduced a coherence measure based on the average use of formulas in support sets for observations. Our idea was to identify highly coherent theories with those whose formulas that are tightly coupled to account for observations, while low coherence theories contain many disjointed and isolated statements. The present paper generalizes it to accommodate fundamental intuitions from the philosophy of science and better mirrors scientific practice. Moreover, this new approach is neutral with respect to the philosophy and practice of science, and is able to explain notions like modularization using coherence.

0718

Protocol Compatibility and Automatic Converter Synthesis

Karin Avnit
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: kavnit@cse.unsw.edu.au

Vijay D'Silva
Department of Computer Science,
ETH Zurich
CH-8092 Zurich, Switzerland
E-mail: vdsilva@inf.ethz.ch

Arcot Sowmya
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sowmya@cse.unsw.edu.au

S. Ramesh
GM India Science Lab
Bangalore India
E-mail: rameshari1958@gmail.com

Sri Parameswaran
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sridevan@cse.unsw.edu.au

Hardware module reuse is a standard solution to deal with the increasing complexity of chip architectures and growing pressure to reduce time to market. In the absence of a single module interface standard, pre-designed modules for “plug and play” usually require a converter between incompatible interface protocols. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from implementation or grossly simplify the structure of the protocols considered. In this work, we present a state-machine based formalism for modeling bus based communication protocols, a notion of protocol compatibility and of correct conversion between incompatible protocols. Using this formalism, we derive algorithms for checking protocol compatibility and for automatic converter synthesis. We report our experience with automatic converter synthesis between different configurations of widely used commercial bus protocols, such as AMBA AHB, ASB APB, and the open core protocol (OCP). The presented work is unique in its combination of a complete formal approach and the use of low abstraction level that enables precise modeling of protocol characteristics and simple translation to HDL.

0717

Experience and Trust: A Sytems-Theoretic Approach

Norman Foo
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: norman@cse.unsw.edu.au

Jochen Renz
Research School of Information Science and Engineering
Australian National University
Canberra ACT 2600, Australia
E-mail: jochen.renz@anu.edu.au

An influential model of agent trust and experience is that of Jonker and Treur. In that model an agent uses its experience of the interactions of another agent to assess its trustworthiness. We show here that a key property of that model is subsumed by a result of classical mathematical systems theory. Using the latter theory we also clarify the issue of when two experience sequences may be regarded as equivalent. An intuitive feature of the Jonker and Treur model is that experience sequence orderings are respected by functions that map such sequences to trust orderings. We raise a question about another intuitive property -- that of continuity of these functions, viz. that they map experience sequences that resemble each other to trust values that also resemble each other. Using fundamental results in the relationship between partial orders and topologies we also show that these two intutive properties are essentially equivalent.

0716

Localized Minimum-Latency Broadcasting in Multi-Radio Multi-Channel Multi-Rate Wireless Mesh Networks

J. Qadir, C.T. Chou, J.G. Lim
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {junaidq,ctchou,jool}@cse.unsw.edu.au

Archan Misra
Research Staff Member,
Next-Generation Web Infrastructure Dept.
IBM T J Watson Research Center
19 Skyline Drive,
Hawthorne, NY 10532, USA
Email: archan@us.ibm.com

We address the problem of minimizing the worst-case broadcast delay in ``multi-radio multi-channel multi-rate wireless mesh networks'' (MR2-MC WMN) in a distributed and localized fashion. Efficient broadcasting in such networks is especially challenging due to the desirability of exploiting the ``wireless broadcast advantage'' (WBA), the interface-diversity, the channel-diversity and the rate-diversity offered by these networks. We propose a framework that calculates a set of forwarding nodes and transmission rate at these forwarding nodes irrespective of the broadcast source. Thereafter, a forwarding tree is constructed taking into consideration the source of broadcast. Our broadcasting algorithms are distributed and utilize locally available information. To the best of our knowledge, this works constitutes the first contribution in the area of distributed broadcast in multi-radio multi-rate wireless mesh networks. We present a detailed performance evaluation of our distributed and localized algorithm and demonstrate that our algorithm can greatly improve broadcast performance by exploiting the rate, interface and channel diversity of MR2-MC WMNs and match the performance of centralized algorithms proposed in literature while utilizing only limited two-hop neighborhood information.

0715

Solving the expression problem in Haskell with true separate compilation

Sean Seefried
Formal Methods
NICTA
Email: sean.seefried@nicta.com.au

Manuel M. T. Chakravarty

Programming Languages and Systems
School of Computer Science & Engineering
University of New South Wales
Email: chak@cse.unsw.edu.au

We present a novel solution to the expression problem which offers true separate compilation and can be used in existing Haskell compilers that support multi-parameter type classes and recursive dictionaries. The solution is best viewed as both a programming idiom, allowing a programmer to implement open data types and open functions, and the target encoding of a translation from Haskell augmented with syntactic sugar.

0714

Resource-aware Broadcast and Multicast in Multi-rate Wireless Mesh Networks

Bao Hua Liu
Thales Australia - Joint Systems, Garden Island, NSW 2011, Australia

Chun Tung Chou
School of Computer Science and Engineering,
University of New South Wales, Australia
ctchou@cse.unsw.edu.au

Archan Misra
IBM T J Watson Research Center,
Hawthorne, New York, USA
archan@us.ibm.com

Sanjay Jha
School of Computer Science and Engineering,
University of New South Wales, Australia

This paper studies some of the fundamental challenges and opportunities associated with the network-layer broadcast and multicast in a multihop multirate wireless mesh network (WMN). In particular, we focus on exploiting the ability of nodes to perform link-layer broadcasts at different rates (with correspondingly different coverage areas). We first show how, in the broadcast wireless medium, the available capacity at a mesh node for a multicast transmission is not just a function of the aggregate pre-existing traffic load of other interfering nodes, but intricately coupled to the actual (sender, receiver) set and the link-layer rate of each individual transmission. We then present and study six alternative heuristic strategies for computing a broadcast tree that not only factors in a flow's traffic rate but also exploits the wireless broadcast advantage (WBA). Finally, we demonstrate how our insights can be extended to multicast routing in a WMN, and present results that show how a tree-formation algorithm that combines contention awareness with transmission rate diversity can significantly increase the total amount of admissible multicast traffic load in a WMN.

0713

A Stronger Notion of Equivalence for Logic Programs

Ka-Shu Wong
School of Computer Science and Engineering
and National ICT Australia
University of New South Wales
NSW 2052, Australia
E-mail: kswong@cse.unsw.edu.au

Several different notions of equivalence have been proposed for logic programs with answer set semantics, most notably strong equivalence. However, strong equivalence is not preserved by certain logic program operators such as the strong and weak forgetting operators of Zhang and Foo, in the sense that two programs which are strongly equivalent may no longer be strongly equivalent after the same operator is applied to both. We propose the stronger notion of T-equivalence which is designed to be preserved by logic program operators such as strong and weak forgetting. We give a syntactic definition of T-equivalence and provide a model-theoretic characterisation of T-equivalence using what we call T-models. We show that strong and weak forgetting does preserve T-equivalence and using this, arrive at a model-theoretic definition of the strong and weak forgetting operators using T-models.

0712

Protocol Compatibility and Automatic Converter Synthesis

Karin Avnit
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia.
E-mail: kavnit@cse.unsw.edu.au

Vijay D'Silva
Department of Computer Science,
ETH Zurich
CH-8092 Zurich, Switzerland.
E-mail: vdsilva@inf.ethz.ch

Arcot Sowmya
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia.
E-mail: sowmya@cse.unsw.edu.au

S. Ramesh
GM India Science Lab
Bangalore, India.
E-mail: rameshari1958@gmail.com

Sri Parameswaran
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sridevan@cse.unsw.edu.au

Hardware module reuse is common practice to deal with the increasing complexity of chip architectures and growing pressure to reduce time to market. In the absence of module interface standards, use of pre-designed modules in a "plug and play" fashion usually requires a converter between incompatible interface protocols. Though several approaches to such mediation have been proposed in the past, automation of protocol converter synthesis is yet to be realized. In this work, we present a state-machine based formalism for modeling bus based communication protocols, a notion of protocol compatibility and of protocol conversion. Using this formalism, we devise algorithms for checking protocol compatibility and for automatic converter synthesis. We report our experience with automatic converter synthesis for commercial bus protocols. The presented work is unique in its low abstraction level that enables precise modeling of protocol characteristics and simple translation to HDL.

0711

Topology Control and Channel Assignment in Multi-Radio Multi-Channel Wireless Mesh Networks

Anjum Naveed
School of Computer Science and Engineering
The University of New South Wales,
NSW 2052, Australia
E-mail: anaveed@cse.unsw.edu.au

Salil S. Kanhere
School of Computer Science and Engineering
The University of New South Wales,
NSW 2052, Australia
E-mail: salilk@cse.unsw.edu.au

Sanjay K. Jha
School of Computer Science and Engineering
The University of New South Wales,
NSW 2052, Australia
E-mail: sjha@cse.unsw.edu.au

The aggregate capacity of wireless mesh networks can be improved significantly by equipping each node with multiple interfaces and by using multiple channels in order to reduce the effect of interference. Efficient channel assignment is required to ensure the optimal use of the limited channels in the radio spectrum. In this paper, a Cluster-based Multipath Topology control and Channel assignment scheme (CoMTaC), is proposed, which explicitly creates a separation between the channel assignment and topology control functions, thus minimizing flow disruptions. A cluster-based approach is employed to ensure basic network connectivity. Intrinsic support for broadcasting with minimal overheads is also provided. CoMTaC also takes advantage of the inherent multiple paths that exist in a typical WMN by constructing a spanner of the network graph and using the additional node interfaces. The second phase of CoMTaC proposes a dynamic distributed channel assignment algorithm, which employs a novel interference estimation mechanism based on the average link-layer queue length within the interference domain. Partially overlapping channels are also included in the channel assignment process to enhance the network capacity. Extensive simulation based experiments have been conducted to test various parameters and the effectiveness of the proposed scheme. The experimental results show that the proposed scheme outperforms existing dynamic channel assignment schemes by a minimum of a factor of 2.

0710

Generative Code Specialisation for High-Performance Monte-Carlo Simulations

Don Stewart(1)
Hugh Chaffey-Millar(2)
Gabriele Keller(1)
Manuel M. T. Chakravarty(1)
Christopher Barner-Kowollik(2)

(1) Programming Languages and Systems
School of Computer Science & Engineering
University of New South Wales

(2) Centre for Advanced Macromolecular Design
School of Chemical Sciences and Engineering
University of New South Wales

We address the tension between software generality and performance in the domain of scientific and financial simulations based on Monte-Carlo methods. To this end, we present a novel software architecture, centred around the concept of a specialising simulator generator, that combines and extends methods from generative programming, partial evaluation, runtime code generation, and dynamic code loading. The core tenet is that, given a fixed simulator configuration, a generator in a functional language can produce low-level code that is more highly optimised than a manually implemented generic simulator. We also introduce a skeleton, or template, capturing a wide range of Monte-Carlo methods and use it to explain how to design specialising simulator generators and how to generate parallelised simulators for multi-core and distributed-memory multiprocessors. We evaluated the practical benefits and limitations of our approach by applying it to a highly relevant problem in computational chemistry. More precisely, we used a Markov-chain Monte-Carlo method for the study of advanced forms of polymerisation kinetics. The resulting implementation executes faster than all competing software products, while at the same time also being more general. The generative architecture allows us to cover a wider range of chemical reactions and to target a wider range of high-performance architectures (such as PC clusters and SMP multiprocessors). We show that it is possible to outperform low-level languages with functional programming in domains with very stringent performance requirements if the domain also demands generality.

0709

Message Correlation for Conversation Reconstruction in Service Interaction Logs

The problem of understanding the behavior of business processes and of services is rapidly becoming a priority in medium and large companies. To this end, recently, analysis tools as well as variations of data mining techniques have been applied to process and service execution logs to perform OLAP-style analysis and to discover behavioral (process and protocol) models out of execution data. All these approaches are based on one key assumption: events describing executions and stored in process and service logs include identifiers that allow associating each event to the process or service execution they belong to (e.g., can correlate all events related to the processing of a certain purchase order or to the hiring of a given employee). In reality, however, such information rarely exists. In this paper, we present a framework for discovering correlations among messages in service logs. We characterize the problem of message correlation and propose novel algorithms and techniques based on well-funded principles and heuristics on the characteristics of conversations and of message attributes that can act as identifier for such conversations. As we will show, there is no right or wrong way to correlate messages, and such correlation is necessarily subjective. To account for this subjectiveness, we propose an approach where algorithms suggest candidate correlators, provide measures that help users understand the implications of choosing a given correlators, and organize candidate correlators in such a way to facilitate visual exploration. The approach has been implemented and experimental results show its viability and scalability on large synthetic and real-world datasets. We believe that message correlation is a very important and challenging area of research that will witness many contributions in the near future due to the pressing industry needs for process and service execution analysis.

0708

SPARK: Top-k Keyword Query in Relational Databases

Yi Luo (1), Xuemin Lin (1), Wei Wang (1), and Xiaofang Zhou (2)

1: School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {luoyi, lxue, weiw}@cse.unsw.edu.au

2: School of Information Technology and Electrical Engineering
University of Queensland
Australia
E-mail: zxf@itee.uq.edu.au

With the increasing amount of text data stored in relational databases, there is a demand for RDBMS to support keyword queries over text data. As a search result is often assembled from multiple relational tables, traditional IR-style ranking and query evaluation methods cannot be applied directly. In this paper, we study the effectiveness and the efficiency issues of answering top-k keyword query in relational database systems. We propose a new ranking formula by adapting existing IR techniques based on a natural notion of virtual document. Compared with previous approaches, our new ranking method is simple yet effective, and agrees with human perceptions. We also study efficient query processing methods for the new ranking method, and propose algorithms that have minimal accesses to the database. We have conducted extensive experiments on large-scale real databases using two popular RDBMSs. The experimental results demonstrate significant improvement to the alternative approaches in terms of retrieval effectiveness and efficiency.

0707

Adapting Web Service Interfaces and Protocols Using Adapter Simulation

Hamid R. Motahari Nezhad, Boualem Benatallah
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

Axel Matren, Francisco Curbera
IBM TJ Watson Research Center
New York, USA

Fabio Casati
University of Trento
Trento, Italy

In today’sWeb, many functionality-wise similarWeb services are offered through heterogeneous interfaces (operation definitions) and business protocols (ordering constraints defined on legal operation invocation sequences). The typical approach to enable interoperation in such a heterogeneous setting is through developing adapters. There have been approaches for classifying possible mismatches between service interfaces and business protocols to facilitate adapter development. However, the hard job is that of identifying, given two service specifications, the actual mismatches between their interfaces and business protocols. In this paper we present novel techniques and a tool that provides semi-automated support for identifying and resolution of mismatches between service interfaces and protocols, and for generating adapter specification. We make the following main contributions: (i) we identify mismatches between service interfaces, which leads to finding mismatches of type of signature, merge/split, and extra/missing messages; (ii) we identify all ordering mismatches between service protocols and generate a tree, called mismatch tree, for mismatches that require developers’ input for their resolution. In addition, we provide semi-automated support in analyzing the mismatch tree to help in resolving such mismatches. We have implemented the approach in a tool inside IBM WID (WebSphere Integration Developer). Our experiments with some real-world case studies show the viability of the proposed approach. The methods and tool are significant in that they considerably simplify the problem of adapting services so that interoperation is possible.

0706

The Operational Semantics of Dual Logic Programming

Eric A. Martin
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

Many developments in the field of Logic programming reveal poor choices of basic concepts, and misleading views on negation. We show that Logic programming can enjoy a general, simple and clean foundation, provided that the basic concepts be revisited, and that any nonclassical form of negation, in particular, negation as finite failure, be disregarded. We propose a framework that starts with a ruled-based notion of dual logic program, allowing negation to appear in the heads as well as in the bodies of the rules. Dual logic programs can be treated as very general logic programs, but it is conceptually more beneficial to view them as redefined logic programs. Classical semantics, such as the Kripke-Kleene semantics, the well-founded semantics, and the stable model semantics, are redefined as natural program transformations of the same kind, resulting into dual logic programs whose behaviors can be described in terms of the same notion of logical consequence in a classical semantics. A kind of inference `in the style of Logic programming' from arbitrary theories is presented, together with a natural method to transform arbitrary theories into dual logic programs.

0705

WS-Policy4MASC – A WS-Policy Extension Used in the Manageable and Adaptable Service Compositions (MASC) Middleware

Vladimir Tosic, Abdelkarim Erradi, Piyush Maheshwari
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

WS-Policy4MASC is a new XML language that we have developed for policy specification in the Manageable and Adaptable Service Compositions (MASC) middleware. It can be also used for other Web service middleware. It extends the Web Services Policy Framework (WS-Policy) by defining new types of policy assertions. Goal policy assertions specify requirements and guarantees (e.g., maximal response time) to be met in desired normal operation. They guide monitoring activities in MASC. Action policy assertions specify actions to be taken if certain conditions are met or not met (e.g., some guarantees were not satisfied). They guide adaptation and other control actions. Utility policy assertions specify monetary values assigned to particular situations (e.g., execution of some action). They can be used by MASC for billing and for selection between alternative action policy assertions. Meta-policy assertions can be used to specify which action policy assertions are alternative and which conflict resolution strategy (e.g., profit maximization) should be used. In addition to these 4 new types of policy assertions, WS-Policy4MASC enables specification of additional information that is necessary for run-time policy-driven management. This includes information about conditions when policy assertions are evaluated/ executed, parties performing this evaluation /execution, a party responsible for meeting a goal policy assertion, ontological meaning, monitored data items, states, state transitions, schedules, events, and various expressions. We have evaluated feasibility of the WS-Policy4MASC solutions by implementing a policy repository and other modules in MASC. Further, we have examined their usefulness on a set of realistic stock trading scenarios.

0704

Localized Minimum-Latency Broadcasting in Multi-rate Wireless Mesh Networks

Junaid Qadir (^1), Chun Tung Chou (^1), Archan Misra (^2) and Joo Ghee Lim
(^1)

1: School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: [junaidq, ctchou, jool]@cse.unsw.edu.au

2: IBM T J Watson Research Center
19 Skyline Drive,
Hawthorne, NY 10532, USA
E-mail: archan@us.ibm.com

We address the problem of minimizing the worst-case broadcast delay in multi-rate wireless mesh networks (WMN) in a distributed and localized fashion. Efficient broadcasting in such networks is especially challenging due to the multi-rate transmission capability and the interference between wireless transmissions of WMN nodes. We propose connecting dominating set (CDS) based broadcast routing approach which calculates the set of forwarding nodes and the transmission rate at each forwarding node independent of the broadcast source. Thereafter, a forwarding tree is constructed taking into consideration the source of the broadcast. In this paper, we propose three distributed and localized rate-aware broadcast algorithms. We compare the performance of our distributed and localized algorithms with previously proposed centralized algorithms and observe that the performance gap is not large. We show that our algorithms greatly improve performance of rate-unaware broadcasting algorithms by incorporating rate-awareness into the broadcast tree construction algorithm process.

0703

Sensing Data Market: Architecture, Applications and Challenges

Chun Tung Chou
School of Computer Science and Engineering,
University of New South Wales, Australia
ctchou@cse.unsw.edu.au

Nirupama Bulusu
Department of Computer Science,
Portland State University,
USA
nbulusu@cs.pdx.edu

Salil Kanhere
School of Computer Science and Engineering,
University of New South Wales, Australia
salilk@cse.unsw.edu.au

With the rapid development of the Internet and various form of wireless communication technologies, information-on-demand has become a reality, e.g. people today routinely receive news items, stock prices etc. via their mobile phones or RSS feeds. We believe there is a real demand from users for all kind of information and especially sensing data. This paper proposes a new network based service called Sensing Data Market (SenseMart). The defining characteristic of SenseMart is that users share their sensing data among themselves. In other words, SenseMart facilitates the exchange (in the sense of a marketplace) of sensing data and can be viewed as the "Napster" of sensing data. This paper discusses possible architectures for SenseMart and the research challenges to realise it.

0702

WS-Policy4MASC Version 0.8

Vladimir Tosic, Abdelkarim Erradi, Piyush Maheshwari
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia

WS-Policy4MASC is a new XML language that we have developed for policy specification in the Manageable and Adaptable Service Compositions (MASC) middleware. It can be also used for other Web service middleware. It extends the Web Services Policy Framework (WS-Policy) by defining new types of policy assertions. Goal policy assertions specify requirements and guarantees (e.g., maximal response time) to be met in desired normal operation. They guide monitoring activities in MASC. Action policy assertions specify actions to be taken if certain conditions are met or not met (e.g., some guarantees were not satisfied). They guide adaptation and other control actions. Utility policy assertions specify monetary values assigned to particular situations (e.g., execution of some action). They can be used by MASC for billing and for selection between alternative action policy assertions. Meta-policy assertions can be used to specify which action policy assertions are alternative and which conflict resolution strategy (e.g., profit maximization) should be used. In addition to these 4 new types of policy assertions, WS-Policy4MASC enables specification of additional information that is necessary for run-time policy-driven management. This includes information about conditions when policy assertions are evaluated/ executed, parties performing this evaluation /execution, a party responsible for meeting a goal policy assertion, ontological meaning, monitored data items, states, state transitions, schedules, events, and various expressions. This research report provides technical details about WS-Policy4MASC solutions. First, we summarize the need for the language. Then, we list the requirements we have identified for a policy language to support middleware for QoS-aware and adaptive Web service composition. Then, we explain and discuss many architectural decisions in the language. They are illustrated with diagrams (XmlSpy diagrams of XML Schemas and UML diagrams) and examples. The Appendices contain XML files of detailed examples and XML schemas of the WS-Policy4MASC language grammar.

0701

AC-Index: An Efficient Adaptive Index for Branching XML Queries

Bo Zhang (^1), Wei Wang (^2), Xiaoling Wang (^1) and Aoying Zhou

1. Department of Computer Science and Engineering
Fudan University
Shanghai 200433, P. R. China
E-mail: {zhangbo, wxling, ayzhou}@fudan.edu.cn

2. School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: weiw@cse.unsw.edu.au

Query-adaptive XML indexing has been proposed and shown to be an efficient way to accelerate XML query processing, because it dynamically adapts to the workload. However, existing adaptive index suffers from a number of issues, such as lack of support for general types of XML queries, and unsatisfactory query and update performances. In this paper, we propose a new query-adaptive index named AC-Index. It is designed to supports XML path queries with branching predicates. We propose efficient index construction, query processing, and index adaptation algorithms for the AC-Index, together with a number of optimizations to further boost the performance of the index. Our experimental results demonstrate that the AC-Index significantly outperformed previous approaches in terms of query processing and adaptation efficiencies.

0625

Protocol Compatibility and Converter Synthesis

Karin Avnit
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: kavnit@cse.unsw.edu.au

Vijay D'Silva
Department of Computer Science,
ETH Zurich
CH-8092 Zurich, Bwitzerland
E-mail: vdsilva@inf.ethz.ch

Arcot Sowmya
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sowmya@cse.unsw.edu.au

S. Ramesh
Department of Computer Science and Engineering
Indian Institute of Technology Poway, Bombay 400 076
E-mail: ramesh@cse.iitb.ac.in

Sri Parameswaran
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: sridevan@cse.unsw.edu.au

With increasing complexity of chip architecture and growing pressure for short time to market, hardware module reuse is common practice. However, in the absence of module interface standards, use of pre-designed modules in a "plug and play" fashion usually requires a mediator between mismatched interface protocols. Though several approaches to such mediation have been proposed, automation of protocol converter synthesis is yet to be realized. In this work we focus on the framework of state based protocol models. We present a formalism for modeling bus based communication protocols, the notion of compatibility and a protocol converter. Using this formalism, we provide algorithms for checking compatibility and demonstrate the process of automatic converter synthesis for commercial bus protocols.

0624

System F with Type Equality Coercions

Martin Sulzmann
National University of Singapore
Email: sulzmann@comp.nus.edu.sg

Manuel M. T. Chakravarty
Computer Science and Engineering
University of New South Wales
Email: chak@cse.unsw.edu.au

Simon Peyton Jones and Kevin Donnelly
Microsoft Research Ltd
Cambridge, England
Email: {simonpj,t-kevind}@microsoft.com

We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric type functions, given meaning by top-level equality axioms. Unlike System F, FC is expressive enough to serve as a target for several different source-language features, including Haskell's \code{newtype}, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides.

0623

A Framework for Protocol Discovery from Real-World Service Conversation Logs

Understanding the business (interaction) protocol supported by a service is very important for both clients and service providers: it allows developers to know how to write clients that interact with a service, and it allows development tools and runtime middleware to deliver functionality that simplifies the service development lifecycle. It also greatly facilitates the monitoring, visualization, and aggregation of interaction data. This paper presents a framework for discovering protocol definitions from realworld service interaction logs. It first describes the challenges in protocol discovery in such a context. Then, it presents a novel discovery approach, which is widely applicable, robust to different kinds of imperfections often present in real-world service logs, and helps to derive protocols of small sizes, thanks to heuristics. As finding the most precise and the smallest model is algorithmically not feasible from imperfect service logs, finally, the paper presents an approach to refine the discovered protocol via user interaction, to compensate for possible imprecision introduced in the discovered model. The approach has been implemented and experimental results show its viability on both synthetic and real-world datasets.

0622

Securing Channel Assignment in Multi-Radio Multi-Channel Wireless Mesh Networks

Aftabul Haq, Anjum Naveed and Salil Kanhere
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {ahaq,anaveed,salilk}@cse.unsw.edu.au

In order to fully exploit the aggregate bandwidth available in the radio spectrum, future Wireless Mesh Networks (WMN) are expected to take advantage of multiple orthogonal channels, where the nodes have the ability to communicate with multiple neighbours simultaneously using multiple radios (NICs) over orthogonal channels. Dynamic channel assignment is critical for ensuring effective utilization of the non-overlapping channels. Several algorithms have been proposed in recent years, which aim at achieving this. However, all these schemes inherently assume that the mesh nodes are well-behaved without any malicious intentions. A recent work has exposed the vulnerabilities in channel assignment algorithms. In this paper, a mechanism is proposed to secure the channel assignment algorithms, addressing the security vulnerabilities in the existing algorithms. The proposed mechanism successfully prevents the WMN from the recently exposed attacks. The simulation based experiments show the effectiveness of the proposed solution. The experiments also show that the incurred overhead because of security is negligible.

0620

Patterns and the B Method: Bridging Formal and Informal Development

Edward Chan
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: ekfchan@gmail.com

Brett Welch
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: brett.welch@gmail.com

Ken Robinson
School of Computer Science and Engineering
University of New South Wales
NSW 2052, Australia
E-mail: k.robinson@unsw.edu.au

In a world increasingly dependent on software controlled systems, the need for the verification of software safety and correctness has never been greater. Traditional software development methods leave much to be desired in this aspect, relying heavily on testing which can be costly and time inefficient. A more efficient and less error prone approach is to use formal methods, in particular the B method, to develop software. This thesis explores concepts and methods to assist developers in using formal methods by borrowing concepts from the Object Oriented world of software development. Previous attempts at doing this have attempted to adapt the B method to the Object Oriented paradigm. This thesis presents an alternative approach that adapts concepts borrowed from the Object Oriented paradigm, to the B method. By concentrating on commonly occurring patterns in software development and drawing inspiration from the traditional Gang of Four design patterns, this thesis presents a series of patterns adapted to and specialised for the B method, demonstrating how the beginnings of complex and significant systems can be modelled in B.

0619

Energy Driven Application Self-Adaptation at Run-time

Jorgen Peddersen and Sri Parameswaran
School of Computer Science and Engineering
National ICT Australia
University of New South Wales
Sydney 2052 Australia
E-mail: {jorgenp, sridevan}@cse.unsw.edu.au

Until recently, there has been a lack of methods to trade-off energy use for quality of service at run-time in stand-alone embedded systems. Such systems are motivated by the need to increase the apparent available battery energy of portable devices, with minimal compromise in quality. The available systems either drew too much power or added considerable overheads due to task swapping. In this paper we demonstrate a feasible method to perform these trade-offs. This work has been enabled by a low-impact power/energy estimating processor which utilizes counters to estimate power and energy consumption at run-time. Techniques are shown that modify multimedia applications to differ the fidelity of their output to optimize the energy/quality trade-off. Two adaptation algorithms are applied to multimedia applications demonstrating the efficacy of the method. The method increases code size by 1% and execution time by 0.02%, yet is able to produce an output which is acceptable and processes up to double the number of frames.

0618

CLIPPER: Counter-based Low Impact Processor Power Estimation at Run-time

Jorgen Peddersen and Sri Parameswaran
School of Computer Science and Engineering
National ICT Australia
University of New South Wales
Sydney 2052 Australia
E-mail: {jorgenp, sridevan}@cse.unsw.edu.au

Numerous dynamic power management techniques have been proposed which utilize the knowledge of processor power/energy consumption at run-time. So far, no efficient method to provide run-time power/energy data has been presented. Current measurement systems draw too much power to be used in small embedded designs and existing performance counters can not provide sufficient information for run-time optimization. This paper presents a novel methodology to solve the problem of run-time power optimization by designing a processor that estimates its own power/energy consumption. Estimation is performed by the addition of small counters that tally events which consume power. This methodology has been applied to an existing processor resulting in an average power error of 2% and energy estimation error of 1.5%. The system adds little impact to the design, with only a 4.9% increase in chip area and a 3% increase in average power consumption. A case study of an application that utilizes the processor showcases the benefits the methodology enables in dynamic power optimization.

0617

Modeling Path Length in Wireless Ad-hoc Network

Quan Jun Chen, Salil S. Kanhere, Mahbub Hassan
School of Computer Science and Engineering
University of New South Wales, Australia
E-mail: {quanc, salilk, mahbub}@cse.unsw.edu.au

Path length(i.e: the number of hops), the fundamental metric of multi-hop wireless network, has a determinative effect on the performance of wireless network, such as throughput, end-to-end delay and energy consumption. In this paper, we propose a stochastic process based mathematical model to analyze the shortest path length. The model is based on the observation that greedy forwarding in geographic routing can approximately find the shortest path in reasonably dense network. We present formula for the probability mass function of path length, given the distance between source and destination. In addition, we also propose a simple but efficient formula to estimate the mean path length. Our analytical results are well justified by a rich set of simulations, in which both random and realistic mobility scenarios have been investigated.

0615

GOLD: An Overlay Multicast Tree with Globally Optimized Latency and Out-Degree

Jun Guo, Sanjay Jha
School of Computer Science and Engineering
The University of New South Wales, Australia
Email: {jguo,sjha}@cse.unsw.edu.au

Suman Banerjee
Department of Computer Sciences
University of Wisconsin-Madison, USA
Email: suman@cs.wisc.edu

End-to-end delay and interface bandwidth usage are two important performance metrics in overlay multicast networks. This paper demonstrates that, by jointly optimizing the placement of multicast service nodes and the routing strategy for overlay multicast networks, it is possible to find an overlay multicast tree that both minimizes the maximum end-to-end delay between the source and the destinations, and balances the interface bandwidth usage within the set of multicast service nodes. Motivated by this important observation, we propose in this paper a joint optimization problem for overlay mutlicast networks, where we wish to find a globally optimized overlay multicast tree with minimum average end-to-end delay subject to two stringent constraints: 1) The maximum end-to-end delay is bounded by the unicast latency from the source to the farthest destination in the physical topology; 2) The interface bandwidth usage is balanced within the set of multicast service nodes. This problem is shown to be NP-hard. We present a low complexity greedy algorithm that obtains good quality approximate solutions to the problem. We further show how the greedy algorithm enables the design of a weight-coded genetic algorithm that achieves closer-to-optimal solutions with reasonable computational complexity.

0614

System F with Type Equality Coercions (superseded by TR 0624)

We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) non-parametric type functions, given meaning by top-level equality axioms. Unlike System F, FC is expressive enough to serve as a target for several different source-language features, including Haskell's newtype, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides. FC can therefore serve as a typed intermediate language in a compiler that supports these features.

0613

An Interim Report of XML Process Models

Tu Tak Tran
School of Computer Science and Engineering
University of New South Wales
Sydney NSW 2052 Australia
Email: ttt@cse.unsw.edu.au

This report presents preliminary models for XML processes, and a general framework for its usage. The set of models are at an early stage of development and are not as yet complete. This report serves as an interim for further development in XML process modeling.

0611

A Graph Drawing Approach to Sensor Network Localization

Muhammad S. Nawaz and Sanjay K. Jha
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {mnawaz,sjha}@cse.unsw.edu.au

In this work, we present a centralized localization mechanism for wireless sensor networks. Our method is based on a graph drawing algorithm and utilizes inter node distances to localize sensor nodes in a local coordinate system upto a global translation, rotation and reflection without any absolute reference positions such as GPS or other anchor nodes. We show through simulations that, it is possible to avoid folds and flips in the localized network layout if the entire topology is considered as a whole as opposed to distances to immediate neighbors only. We assess the effect of different parameters like scale, node degree and ranging noise on our algorithm. Finally, we propose a hierarchical approach to make the algorithm scalable for large networks, which we would like to pursue as future work.

0610

Patching Approximate Solutions in Reinforcement Learning

Min Sub Kim
ARC Centre of Excellence for Autonomous Systems
School of Computer Science and Engineering
University of New South Wales
Sydney NSW 2052 Australia
msk@cse.unsw.edu.au

William Uther
National ICT Australia
Sydney NSW 2052 Australia
william.uther@nicta.com.au

This report introduces an approach to improving an approximate solution in reinforcement learning by augmenting it with a small overriding patch. Many approximate solutions are smaller and easier to produce than a flat solution, but the best solution within the constraints of the approximation may fall well short of global optimality. We present an algorithm for efficiently learning a small patch to reduce this gap. Empirical evaluation demonstrates the effectiveness of patching, producing combined solutions that are much closer to global optimality.

0609

On building 3D maps using a Range Camera: Applications to Rescue Robotics

Raymond Sheh, M. Waleed Kadous and Claude Sammut
ARC Centre of Excellence for Autonomous Systems
School of Computer Science and Engineering
The University of New South Wales
Sydney, NSW, 2052, Australia
[rsheh|waleed|claude]@cse.unsw.edu.au

It is critical in many mobile robotics applications to characterise the presence and position of objects around the robot. This is the case whether the mobile robot is under autonomous or teleoperative control. In this paper, we examine the use of a CSEM SwissRanger SR-2 3D range camera which allows the generation of dense, accurate 3D point clouds around a mobile robot. Combined with other data sources, such as video cameras, this allows the creation of 3D maps that can be used for .fly throughs.. Furthermore, this same technique allows a teleoperator to very accurately place landmarks within the 3D maps. As this device is still somewhat prototypical, we also discuss some of the issues associated with the use of this device. The test application was the 2005 RoboCup Rescue Robot League, a competition that simulates robot-assisted Urban Search and Rescue (USAR) tasks and places great importance on effectively generating maps. Novel techniques for processing the raw measurements from the sensor, and its use to create maps of mock disaster sites are discussed. The maps generated, part of Team CASualty.s entry, were received very well by the judges of the competition and were unique in their combination of 3D, colour and thermal information, and the automated way in which the placement of landmarks and other annotations were performed. The maps were instrumental in the team.s achievement of 3rd place.

0608

Minimum Latency Broadcasting in Multi-Radio Multi- Channel Multi-Rate Wireless Mesh Networks

Junaid Qadir, Chun Tung Chou, Archan Misra*
School of Computer Science and Engineering, University of New South Wales, Australia
IBM T J Watson Research Center, Hawthorne, New York, USA*
Email: {junaidq, ctchou}@cse.unsw.edu.au,archan@us.ibm.com

We address the problem of minimizing the worst-case broadcast delay in multi-radio multi-channel multi-rate (MR2-MC) wireless mesh networks (WMN). The problem of `efficient' broadcast in such networks is especially challenging due to the numerous inter-related decisions that have to be made. The multi-rate transmission capability of WMN nodes, interference between wireless transmissions, and the hardness of optimal channel assignment adds complexity to our considered problem. We present four heuristic algorithms to solve the minimum latency broadcast problem for such settings and show that the `best' performing algorithms usually adapt themselves to the available radio interfaces and channels. We also study the effect of channel assignment on broadcast performance and show that channel assignment can affect the broadcast performance substantially. More importantly, we show that a channel assignment that performs well for unicast does not necessarily perform well for broadcast/multicast. To the best of our knowledge, this work constitutes the first contribution in the area of broadcast routing for MR2-MC WMN.

0607

Security Vulnerabilities in Channel Assignment of Multi-Radio Multi-Channel Wireless Mesh Networks

Anjum Naveed and Salil Kanhere
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: {anaveed,salilk}@cse.unsw.edu.au

In order to fully exploit the aggregate bandwidth available in the radio spectrum, future Wireless Mesh Networks (WMN) are expected to take advantage of multiple orthogonal channels, with nodes having the ability to communicate with multiple neighbors simultaneously using multiple radios (NICs) over orthogonal channels. Dynamic channel assignment is critical for ensuring effective utilization of the non-overlapping channels. Several algorithms have been proposed in recent years, which aim at achieving this. However, all these schemes inherently assume that the mesh nodes are well-behaved without any malicious intentions. In this report, we expose the vulnerabilities in channel assignment algorithms and unveil three new security attacks: Network Endo-Parasite Attack (NEPA), Channel Ecto-Parasite Attack (CEPA) and low-cost ripple effect attack (LORA). These attacks can be launched with relative ease by a malicious node and can cause significant degradation in the network performance. We also evaluate the effectiveness of these attacks through simulation based experiments and briefly discuss possible solutions to counter these new threats.

0606

Piggy Back Challenge Based Security Mechanism for IEEE 802.11i Wireless LAN CCMP Protocol

M. Junaid Hussain , M. Akbar, Muid Mufti & Salil Kanhere
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: junaid-mcs@nust.edu.pk , makber59@hotmail.com , muid@uetaxila.edu.pk, salilk@cse.unsw.edu.au

Counter mode is used for data confidentiality within IEEE 802.11 Wireless LANs. Counter mode utilizes temporal key and counter value for encryption . The temporal key is derived as a result of successful authentication. It is shown in this paper that Counter mode is vulnerable to attacks by intruders. This paper presents a piggy back challenge based security mechanism. It is shown that the nonce and initial counter are derived from the session key and are kept secret. The same nonce is used as a challenge text from authenticator to supplicant. The supplicant utilizes the nonce as encryption key for the subsequent packets. The proposed challenge response mechanism is a continuous process and thus provides freshness, per packet encryption key and unpredictability of counter value. The freshness provides protection against replay attacks, the unpredictability of counter value prevents precomputation attack and the per-packet challenge response mechanism using separate encryption key for each packet strengthens the security of the connection against unauthorized access by immediately discarding the packet if Per-Packet Authentication fails. Our piggy back challenge based Security mechanism provides a fundamental base for strengthening the security of WLAN.

0605

Lock Selection in Practice

Abdelsalam Shanneb and John Potter
{shanneba,potter}@cse.unsw.edu.au

Programming Languages and Compilers Group
School of Computer Science and Engineering
The University of New South Wales
Sydney, NSW 2052, Australia

This report is a continuation of our last report (UNSW-CSE-TR-604). Here, we present our algorithm for offering lock choices. We show all the details involved in making lock choices for programmers. We offer different approaches to lock selection; we propose top-down and bottom-up strategies, as well as, additive and subtractive techniques. These lock choices are based on the previously established Galois connection between the layers of a composite. We also present several examples that demonstrate our prototype tool for lock selection, the output of which is in Appendix A.

0604

A Galois Connection in Composite Objects

With the advent of multiprocessors on the desktop, software applications are increasingly likely to adopt multithreaded architectures. To cope with the complexity of concurrent systems, programmers build systems from thread-safe components. This produces excessive and redundant locking, restricting the potential for concurrency within the system. Rather than deploying individual thread-safe components, we advocate deferring the deployment of locks until the code dependencies are known. This avoids redundant locking, and allows the granularity of concurrency to be chosen in a flexible way. In earlier work we identified a formal relationship, known as a Galois connection, between the potential for concurrency in a composite system and the locking requirements for its components. This report highlights the role of fixpoints for lock selection. The subsequent report (UNSW-CSE-TR-605) will investigate strategies for selecting locks in a composite system.

0603

COMMA: A Communications Methodology for Dynamic Module-based Reconfiguration of FPGAs

Shannon Koh and Oliver Diessel
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: shannonk@cse.unsw.edu.au and odiessel@cse.unsw.edu.au

On-going improvements in the scaling of FPGA device sizes and time-to-market pressures motivate the adoption of a module-oriented design flow for the development of applications. At the same time, economic factors encourage the reuse of smaller devices for high performance computational tasks. Like other researchers, we therefore envisage a need for dynamic reconfiguration of FPGAs at the module level. However, proposals to date have not focussed on communications issues, have advocated use of specific protocols, cannot be readily implemented, and/or do not support current device architectures. This paper proposes a methodology for the rapid deployment of a communications infrastructure that efficiently supports the communications needs of a collection of dynamic modules when these are known at design time. The methodology also provides a degree of flexibility to allow a range of unknown communication requirements to be met at run time. Our aim is to support new tiled dynamically reconfigurable architectures such as Virtex-4, as well as mature device families. We assess a prototype of the communications infrastructure and outline opportunities for automating the design flow.

0601

OCEAN -- Scalable and Adaptive Infrastructure for On-board Information Access

Boualem Benatallah, Mahbub Hassan, Lavy Libman*, Aixin Sun
School of Computer Science and Engineering
University of New South Wales
Sydney, NSW 2052, Australia
Email: {boualem,mahbub,aixinsun}@cse.unsw.edu.au

*National ICT Australia
Bay 15, Australian Technology Park
Eveleigh, NSW 1430, Australia
Email: Lavy.Libman@nicta.com.au

The idea of providing seamless connectivity and information access to users on-board public transport vehicles has attracted increasing popularity in recent years, as is evidenced by several commercially available systems that have attempted to implement it. In this article, we overview the specific technological challenges, research issues, as well as opportunities, that arise in the context of providing communication and information access on public transport. We focus on both the networking perspective --- in particular, discussing extensions required to existing TCP/IP mechanisms to support the moving on-board networks --- and the data management perspective, e.g. personalization of information and caching/pre-fetching for a highly dynamic and heterogeneous population of users. We contend that, to offer the best performance and flexibility, the design of public transport information systems ought to take advantage of the synergy between these two areas.

0524

Validation of SECI Model in Education

Cat Kutay
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: ckutay@cse.unsw.edu.au

Aybuke Aurum
School of Information Systems, Technology and Management
University of New South Wales
Sydney 2052 Australia
E-mail: aybuke@unsw.edu.au

The use of Knowledge Management (KM) is increasingly relevant to education as our knowledge of factors influencing the effective managing of information and knowledge resources. It is important that educational organizations understand the application of strategies for managing the knowledge resources and providing appropriate access to this information within the University context. This article examines data collected from students doing the Software Engineering Program at UNSW. This data is used to analyse the industrial SECI model of KM as applied to the educational domain. We are looking at the validity of the empirical evidence. Results indicated that the data provided a valid study of KM in this context.

0523

Redback: A Low-Cost Advanced Mobility Robot

Raymond Sheh
School of Computer Science and Engineering
and The National ICT Australia
University of New South Wales
Sydney 2052 Australia
E-mail: rsheh@cse.unsw.edu.au

Many of the more interesting applications of mobile robotics involve robots that are able to traverse unstructured environments. Unfortunately, currently available robots for such a purpose tend to be limited in their mobility (very few can climb stairs for instance), are excessively heavy, must be custom built or are very expensive. This article describes preliminary work on construction of an advanced mobility robot based on a Tarantula radio controlled toy, sold by MGA Entertainment. Despite being very low in cost (sub-$200AUD), this toy can easily climb stairs and overcome obstacles that challenge much larger robots. It can easily carry an onboard computer which can directly interface with the existing motor controllers as well as additional cameras, small laser rangefinders and other sensors. The full cost of parts for the basic robot, including computer and simple sensors, is expected to be around the $1,000AUD mark with basic computer-less versions starting below $300AUD. The modified robot has been dubbed Redback, after the Australian spider of the same name.

0522

The Shadow Knows: Refinement of ignorance in sequential programming

Carroll Morgan
School of Computer Science and Engineering
University of New South Wales
Sydney 2052 Australia
E-mail: carrollm@cse.unsw.edu.au

Sequential-program state can be separated into "visible" and "hidden" parts in order to allow knowledge-based reasoning about the hidden values. Ignorance-preserving refinement should ensure that observing the visible part of an implementation can reveal no more about the hidden part than could be revealed by its specification. Possible applications are zero-knowledge protocols, or security contexts where the "high-security" state is considered hidden and the "low-security" state is considered visible. Rather than checking for ignorance preservation at each stage, we suggest program-algebraic "refinement rules" that preserve ignorance by construction. The Dining Cryptographers is a motivating example, in which ignorance of certain variables (coins) is intended to contribute to an ignorance property of the overall protocol. Our algebra is powerful enough to derive the Dining Cryptographers' Protocol, while retaining soundness by avoiding (for example) the Refinement Paradox. We formulate and justify general principles about which refinement rules should be retained, for algebraic power and utility, and which should be discarded, for soundness.

0521

ASEHA: A Web Services Protocol Modelling Formalism

Pemadeep Ramsokul and Arcot Sowmya
School of Computer Science and Engineering
University of Ne