Digitalization is transforming manufacturing systems to become more agile and smart thanks to the integration of sensors and connection technologies that help capture data at all phases of a product's life cycle.Digitalization promises to improve manufacturing flexibility, quality, productivity, and reliability.However, there is still a significant need of effective methods to develop models that could enhance the capabilities of manufacturing systems.Formal methods and tools are becoming essential to achieve this objective.Within this context, this paper introduces a formal software solution for the automatic generation of modular manufacturing control systems software.The proposed solution leverages software Model-Based Design (MBD) techniques to reduce development effort, time, and human error by automating several manual steps.

Safety violations in programmable logic controllers (PLCs), caused either by faults or attacks, have recently garnered significant attention. However, prior efforts at PLC code vetting suffer from many drawbacks. Static analyses and verification cause significant false positives and cannot reveal specific runtime contexts. Dynamic analyses and symbolic execution, on the other hand, fail due to their inability to handle real-world PLC programs that are event-driven and timing sensitive. In this paper, we propose VetPLC, a temporal context-aware, program analysis-based approach to produce timed event sequences that can be used for automatic safety vetting. To this end, we (a) perform static program analysis to create timed event causality graphs in order to understand causal relations among events in PLC code and (b) mine temporal invariants from data traces collected in Industrial Control System (ICS) testbeds to quantitatively gauge temporal dependencies that are constrained by machine operations. Our VetPLC prototype has been implemented in 15K lines of code. We evaluate it on 10 real-world scenarios from two different ICS settings. Our experiments show that VetPLC outperforms state-of-the-art techniques and can generate event sequences that can be used to automatically detect hidden safety violations.