Automated Model Checking of Distributed Cyber Physical Systems Software

Developed an automated model translation and generation tool for validation and timing analysis of software components for distributed cyber physical systems using Timed Automata and UPPAAL. The tool uses AST based respresentations to parse Python source code of individual software compnents of a distributed system and then merge them with user specified timing properties in the form of specially formatted comments, to generate a composite network of timed automata processes. It preserves the communication patterns of the individual software components using timed automata features suc as channels and synchronization labels. The generated automata can then be read using UPPAAL model checker and verified using formal verification queries such as the stimulus-to-response delay, buffer overflow etc. The tool was tested on a distributed data streaming and processing workflow using two different deployment architectures.

This work is currently submitted for review at the 2023 IEEE International Symposium on Real-Time Distributed Computing