The purpose of the project is to synthesize a monitoring application in an automated way, which is able to check the behaviour of Android applications running on Android platform, on the basis of specified requirements. Specifying the requirements is possible using Linear Temporal Logic (LTL) as a formal requirement specification language. The specified LTL expressions may contain elements of the set of observable events (as operands), as well as Boolean and temporal operators. The developed Java-based code generator tool takes an LTL expression as input, and synthesizes a monitoring application runnable on the Android platform. The monitor is able to inspect whether the requirements specified by the LTL expression are met by the behaviour of the monitored application, and also intervene to its operation, for example by terminating it in case of violating the requirements.
The synthesized monitoring application and the monitored application must be able to communicate with each other to exchange informations. To satisfy this requirement, an independent middleware has been developed for effective communication. The central part of this middleware is a module, to which the endpoints can connect and with which the endpoints can communicate without having to directly identify each other. The communication is based on the publisher-subscriber design pattern, because the characteristic of this pattern is that it allows several subscribers to subscribe to an event published by a publisher. It means that a checked application can be monitored by several monitoring applications, each of them checking its behaviour on the basis of requirements. The central module has the ability to serve the endpoints. The publishing behaviour of the monitored application is freely configurable by instrumenting it, injecting some callbacks to a contractor module (that was also developed in the context of this project). The contractor module provides an API for the applications, which enables them to connect to the central module, send their relevant messages (events) towards, and also receive messages backwards. Configuration of processing the incoming messages is also possible by instrumenting the endpoints, thereby the interactions induced by incoming messages can be fully customized.