View article

Modern cyber-physical systems place ever-increasing reliance on high-assurance software. Recent high-profile safety and security incidents directly attributable to software point to a failure to develop sufficient assurance of software correctness through verification and validation. While formal methods provide techniques for proving that critical safety and security properties hold for all inputs and all execution paths, engineers typically rely on simulation and testing -- which can only establish the presence but not the absence of defects. A key reason for the lack of application of formal methods is the perception that they are difficult to learn and to use. In previous work, we introduced Simulink2PVS, a tool that converts SIMULINK models to the PVS specification language. In this paper, we extend Simulink2PVS to translate the checks associated with SIMULINK assertion blocks to putative theorems. This approach …