MIST: monitor generation from informal specifications for firmware verification

This paper presents MIST, an all-in-one tool capable of generating a complete environment to verify C/C++ firmwares starting from informal specifications. Given a set of specifications written in natural language, the tool guides the user in translating each specification into an XML formal description that captures a temporal behaviour that must hold in the design. Our XML format guarantees the same expressiveness of linear temporal logic, but it is designed to be used by designers that are not familiar with formal methods. Once each behavior is formalized, MIST automatically generates the corresponding test-bench and checker to stimulate and verify the design. In order to guide the verification process, MIST employs a clustering procedure that classifies the internal states of the firmware. Such a classification aims at finding an effective ordering to check the expected behaviors and to advise for possible specification holes. MIST has been fully integrated into the IARSystem Embedded Workbench. Its effectiveness and efficiency have been evaluated to formalize and check a complex test-plan for an industrial firmware.