Detecting Data Anomalies from Their Formal Specifications: A Case Study in IoT Systems

We present in this paper a new method in detecting anomalies in datasets representing systems behaviour, which is based on comparing a dataset to the data blueprint of the system representing its normal behaviour. This method removes some of the need for applying complex machine learning algorithms that aim at detecting abnormalities in such datasets and gives a more assured outcome of the presence of abnormalities. Our method first models a system using the formal language of the π -calculus, and then applies an abstract interpretation that ultimately generates an abstract multiset representing the messages exchanged in the system model. We term this multiset as the data blueprint of the system, and it represents the normal behaviour expected. We apply this method to the case of a recent study in literature, which attempts to analyse normal and abnormal behaviour in datasets representing runs of the MQTT protocol, both under attack and no attack conditions. We show that our method is able to detect these conditions in an easier and more straightforward manner than the original case study attempts to.