Towards Automatic Program Specification Using SME Models

This paper introduces a method to simplify hardware modeling and verification thereof in order for software programmers to, more easily, meet the demands of the growing embedded device industry. We describe a simple method for transpiling from the new SME Implementation Language into CSPMand using formal verification to verify properties within the generated program. We present a small example consisting of a seven segment display clock network and introduce how to verify the widths of the channels in the network.