Designing, Modeling and Analysis of GALS Software Systems

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.