Formal Methods and Event Notification Systems in Mobile Computing Environment

TL;DR

This paper examines the specification of event-based systems in mobile computing environments, critiquing Mobile UNITY constructs and proposing a simplified approach that maintains UNITY's simplicity and facilitates implementation.

Contribution

It demonstrates that certain Mobile UNITY constructs are unnecessary and introduces a simplified modification to UNITY for better mapping and implementation in mobile environments.

Findings

Mobile UNITY constructs can be overly complex.

A simplified UNITY modification improves mapping to architectures.

The approach preserves UNITY's proof logic.

Abstract

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.