ABSTRACT. Organizations and researchers alike have widely recognised the multiple advantages of adapting Network Intrusion Detection Systems (NIDS) as the norm to monitor against DoS attacks on their systems. Although effective, implementation within the Internet of Things (IoT) is complicated as the setups and protocols used vary, necessitating data collection to be bespoke to an individual system. Standard approaches used to train NIDS include; 1) Use a database of known attacks or 2) testing systems to create a ``benchmark" behaviour and flag any anomaly as a potential attack. It is not feasible to establish a benchmark behaviour in dynamic IoT systems where devices may constantly shift, new devices might join and behaviours might change. The IoT is by its very nature ubiquitous and therefore time consuming to benchmark, we therefore focus on the first approach. This approach has its own drawbacks amplified for IoT systems as: 1) Collecting data unique to a system and for each attack is time consuming and 2) some system changes can require to collect the data or part of the data from scratch (e.g. interactive smart homes where devices can change frequently)

To address these limitations we present a novel modelling approach which we call Lightweight IoT System under Attack (LISA) to represent the effects of Power Drain and DDoS attacks on IoT Systems. We begin with a precise formalization of properties of IoT devices using measurements from the real system and run verification on the model to assure matching behaviour. We then model specific attacks on the systems and generate synthetic dataset.