Extending the theory of Owicki and Gries with asynchronous message passing

We describe an extension of the theory of Owicki and Gries (1976) to a programming language that supports asynchronous message passing based on unconditional send actions and conditional receive actions. The focus is on exploring the fitness of the extension for distributed program derivation. A number of experiments are reported, based on a running example problem, and with the aim of exploring design heuristics and of streamlining derivations and progress arguments.

A synchronous multimedia annotation system for secure collaboratories

In this paper, we describe the Vannotea system - an application designed to enable collaborating groups to discuss and annotate collections of high quality images, video, audio or 3D objects. The system has been designed specifically to capture and share scholarly discourse and annotations about multimedia research data by teams of trusted colleagues within a research or academic environment. As such, it provides: authenticated access to a web browser search interface for discovering and retrieving media objects; a media replay window that can incorporate a variety of embedded plug-ins to render different scientific media formats; an annotation authoring, editing, searching and browsing tool; and session logging and replay capabilities. Annotations are personal remarks, interpretations, questions or references that can be attached to whole files, segments or regions. Vannotea enables annotations to be attached either synchronously (using jabber message passing and audio/video conferencing) or asynchronously and stand-alone. The annotations are stored on an Annotea server, extended for multimedia content. Their access, retrieval and re-use is controlled via Shibboleth identity management and XACML access policies.

Concurreny based transition refinement for the verification of distributed algorithms

We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.

An experiment in the design of distributed programs

This paper describes an experiment in the design of distributed programs. It is based on the theory of Owicki and Gries extended with rules for reasoning about message passing. The experiment is designed to test the effectiveness of the extended theory for designing distributed programs.

A software audit framework for spyware risk mitigation

Our research described in this paper identifies a three part premise relating to the spyware paradigm. Firstly the data suggests spyware is proliferating at an exponential rate. Secondly ongoing research confirms that spyware produces many security risks – including that of privacy/confidentiality breaches via illicit data collection and reporting. Thirdly, anti-spyware controls are improving but are still considered problematic for several reasons. Our research then concludes that control measures to counter this very significant challenge should merit compliance auditing – and this auditing may effectively target the vital message passing performed by all illicit data collection spyware. Our research then evolves into an experiment involving the design and implementation of a software audit tool to conduct the desired compliance auditing. The software audit tool is positioned at the protected network’s gateway. The software audit tool uses ‘phone-home’ IP addresses as spyware signatures to detect the presence of the offending software. The audit tool also has the capability to differentiate legitimate message passing software from that produced by spyware – and ‘learn’ both new spyware signatures and new legitimate message passing profiles. The testing stage of the software has proven successful – albeit using very limited levels of network message passing variety and frequency.

Towards a refinement calculus for concurrent real-time programs

We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms between the concurrent components of a program: communication via shared variables and asynchronous message passing (for different models of channels). The semantics is the basis for a refinement calculus to derive machine-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.

Effect of self-monitoring and national culture on follower perceptions of personal charisma and charismatic message

In this paper, a theory of charismatic relationships is examined with reference to the follower's personal characteristics. It is argued that a leader's charismatic message and personal charisma occupy different roles for individuals who vary in national culture and level of self-monitoring. In an empirical test of the theory, 387 undergraduates of Chinese and Australian cultural backgrounds completed self-monitoring and charismatic leadership instruments. High self-monitors placed more importance on personal charisma than the charismatic message. Chinese participants relied more than the Australians on the charismatic message, although this preference depended on self-monitoring orientation. These results indicate the influence of both individual-and cultural-level variables on leader-member relationships, and the need to consider these effects in future developments of a theory of charismatic leadership.

Relationships between pet ownership and health: Asking questions and passing criticisms

The literature examining purported relationships between ownership of companion animals and health is extremely heterogeneous. While much of the descriptive literature tends to support benefits of animal companionship, large scale, controlled research yields inconsistent and even contradictory findings on several issues, including associations with cardiovascular disease, mood and wellbeing. In an analysis of a large longitudinal data-set from the Australian Longitudinal Study on Women's Health, a prospective study of a nationally representative sample of more than 12,000 older women, difficulties with disentangling the effects of powerful demographic variables and age-related factors from the specific effects of pet ownership became apparent. Both cross-sectional and longitudinal analyses demonstrated that associations between mental and physical health and pet ownership as well as changes in pet ownership over time were weak and inconsistent compared to the large effects of living arrangements and other demographic variables. As sociodemographic variables relate strongly to both health and opportunities for pet ownership, this high level of confounding means it is unlikely that the impact of the specific variable of pet ownership on health can be ascertained from such studies. Rather, well-designed experimental studies, wherein the majority of such confounding variables can be held constant or at least somewhat controlled, are needed.

Investigation of the relationship between protein, message and inducer concentrations in recombinant E-coli cells

Chloramphenicol acetyl transferase (CAT) protein and mRNA levels in E. coli were determined following induction of a tac::cat construct by isopropyl-beta-thiogalactopyranoside (IPTG). High cat mRNA levels did not directly reflect CAT protein levels, in either shakeflask experiments or fermentations. Furthermore, concentrations of IPTG resulting in the highest levels of expression of cat mRNA, were different to those resulting in highest levels of CAT protein. The data suggest that high transcriptional activities lead to limitations at the translational level.

Multi-threading and message communication in Qu-Prolog

This paper presents the multi-threading and internet message communication capabilities of Qu-Prolog. Message addresses are symbolic and the communications package provides high-level support that completely hides details of IP addresses and port numbers as well as the underlying TCP/IP transport layer. The combination of the multi-threads and the high level inter-thread message communications provide simple, powerful support for implementing internet distributed intelligent applications.

A review of the first year's experience with an automatic message-routing system for low-cost telemedicine

The Swinfen Charitable Trust has used email for some years as a low-cost telemedicine medium to provide consultant support for doctors in developing countries. A scalable, automatic message-routing system was constructed which automates many of the tasks involved in message handling. During the first 12 months of its use, 1510 messages were processed automatically. There were 128 referrals from 18 hospitals in nine countries. Of these 128 queries, 89 (70%) were replied to within 72 h; the median delay was 1.1 day. The 39 unanswered queries were sent to backup specialists for reply and 36 of them (92%) were replied to within 72 h. In the remaining three cases, a second-line (backup) specialist was required. The referrals were handled by 54 volunteer specialists from a panel of over 70. Two system operators, located 10 time zones apart, managed the system. The median time from receipt of a new referral to its allocation to a specialist was 0.2 days (interquartile range, IQR, 0.1-0.8). The median interval between receipt of a new referral and first reply was 2.6 days (IQR 0.8-5.9). Automatic message handling solves many of the problems of manual email telemedicine systems and represents a potentially scalable way of doing low-cost telemedicine in the developing world.

Automatic message handling for a national counselling service

An automatic email handling system (AutoRouter) was introduced at a national counselling service in Australia. In 2003, counsellors responded to a total of 7421 email messages. Over nine days in early May 2004 the administrator responsible for the management of the manual email counselling service recorded the time spent on managing email messages. The AutoRouter was then introduced. Since the implementation of the AutoRouter the administrator's management role has become redundant, an average of 12 h 5 min per week of staff time has been saved. There have been further savings in supervisor time. Counsellors were taking an average of 6.2 days to respond to email messages (n=4307), with an average delay of 1.2 days from the time counsellors wrote the email to when the email was sent. Thus the response was sent on average 7.4 days after receipt of the original client email message. A significant decrease in response time has been noted since implementation of the AutoRouter, with client responses now taking an average of 5.4 days, a decrease of 2.0 days. Automatic message handling appears to be a promising method of managing the administration of a steadily increasing email counselling service.

Mobile message services and communications policy

Something of a design after-thought, mobile phone SMS (Short-Message Services) have been enthusiastically adopted by consumers worldwide, who have created a new text culture. SMS is now being deployed to provide a range of services and transactions, as well as playing a critical role in offering an interactive path for television broadcasting. In this paper we offer a case study of a lucrative, new industry developing internationally at the intersection of telecommunications, broadcasting, and information services—namely, premium rate SMS/MMS. To explore the issues at stake we focus on an Australian case study of policy responses to the development of premium rate mobile messaging services in the 2002-2005 period. In the first part, we give a brief history of premium rate telecommunications. Secondly, we characterise premium rate mobile message services and examine their emergence. Thirdly, we discuss the responses of Australian policy-makers and industry to these services. Fourthly, we place the Australian experience in international context, and indicate common issues. Finally, we draw some conclusions from the peregrinations of mobile message services for regulators grappling with communications policy frameworks.