Designing software systems underpinned by a formal model of computation (MoC) is crucial for safety-critical, real-time and all industrial applications as it allows formal analysis of those designs and support for correct by design systems. In this paper, we focus on Globally Asynchronous Locally Synchronous (GALS) software systems and Coloured Petri Nets (CPNs) based approach to formally model and analyse GALS software systems specified in SystemJ GALS programming language. The approach translates SystemJ constructs into CPN modules and composes them into CPN GALS model based on control flow and concurrency specified in the SystemJ program. It preserves GALS MoC by automatically integrating synchronizer modules, asynchronous channel interface modules, and scheduling modules to result in the execution model of SystemJ program equivalent CPN. The created CPN GALS model allows system developers to verify the properties of the design formally with the use of Computation Tree Logic (CTL). An industrial automation example is provided as a use case.

SystemJ is a programming language developed for implementing safety critical cyber-physical systems, including industrial automation systems. However, the current tools do not support an efficient mechanism to verify SystemJ programs formally. This paper presents a semantics-preserving translation of the synchronous subset of SystemJ to Coloured Petri Net (CPN), which in turn enables leveraging the plethora of analysis and verification tools for CPN to verify SystemJ programs. The translation and verification approach is illustrated on a pedagogical industrial automation example of a SystemJ program.