Compatibility checking for cyber-physical systems based on microservices

Microservices architecture provides a promising solution for developing sustainable cyber-physical systems (CPSs). However, checking the compatibility of CPSs over a set of microservices communicating asynchronously via unbounded buffers are undecidable due to their infinite state spaces. In this article, we propose a new approach for checking the compatibility of CPSs with infinite state spaces without restricting the size of buffers or the number of communication cycles. First, we integrate CPSs with microservice architecture and design the system architecture for building CPSs over a set of cyber-physical microservices with unbounded buffers. Second, we model CPSs composed of asynchronously communicating cyber-physical microservices via FIFO buffers as labelled transition systems. Third, we adopt the stability notion and present a sufficient condition for checking the unspecified receptions of CPSs through stability checking. Finally, we implement our approach in Process Analysis Toolkit for automatic compatibility checking and conduct experiments to show our approach is effective and efficient.