|
|
 |
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? |
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 |
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 |
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 |
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 todaysWeb, 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 |
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 University of Trento Trento, Italy |
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) |
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) 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 |
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 |
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. |
| |
|