Search

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.

We face a glut of languages for programming distributed software today. However, only a few languages have proven their potential with wider practical use in different domains of computing. We picked two such languages, meant for different domains, to see if they could cross-pollinate and enrich one another. Specifically, we chose SystemJ, a language to program distributed embedded systems, and IEC61499, the next generation standard for distributed industrial automation control software. Unsurprisingly, we found similar structures and artifacts between the two. We also found significant differences mainly due to differing domain-specific requirements. This comparison leads to observations and guidelines for improving both languages, and we discuss directions towards an “ideal” distributed software programming language.