WYPIWYE automation systems — An intelligent manufacturing system case study

We present a novel approach for design of manufacturing automation systems with formal verification of selected properties based on the use of Globally Asynchronous Locally Synchronous programming language SystemJ and industrial-proof verification tools. By being able to prove properties of the automation control logic that consists of multiple concurrent controllers, represented by FSMs that correspond to asynchronous processes of SystemJ program, using Spin model checker, we demonstrate that the program features can be formally verified. Moreover, by also guaranteeing preservation of features and GALS model of the SystemJ program after compilation (correct by construction specification), we actually close the design process within What You Prove Is What You Execute (WYPIWYE) Paradigm.