Towards Formal Modeling and Analysis of SystemJ GALS Systems using Coloured Petri Nets

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.