Formal Methods and Event Notification Systems in Mobile Computing Environment

In this report, we have explored the issues associated with the specification of event-based systems in a mobile environment using Unity \cite{unity}. We used a few constructs and concepts from Mobile UNITY which was proposed as an extension of UNITY by Roman and McCann \cite{intro}. Our aim in this report is to show that some of the constructs proposed in Mobile UNITY are not unnecessary. Those constructs are overly powerful and put a hindrance on the mapping from UNITY specification to particular architectures, which is one of the key simplicity of UNITY specification. Using an example of a message-based event notification system we have shown that a system with a simple modification to the structure of assign section of the UNITY programs could serve well in mapping and implementation at the same time preserve the small and compact proof logic of UNITY.