Tags:Aerospace Engineering, Avionics, explicit model checking, linear temporal logic, Model Checking, Specification Debugging, symbolic model checking, Teaching Formal Methods and Theorem Proving
Abstract:
As formal methods come into broad industrial use for verification of safety-critical hardware, software, and cyber-physical systems, there is an increasing need to teach practical skills in applying formal methods at both the undergraduate and graduate levels. In the Aerospace industry, flight certification requirements like the FAA's DO-178B, DO-178C, DO-333, and DO-254, along with a series of high-profile accidents, have helped turn knowledge of formal methods into a desirable job skill for a wide range of engineering positions. We approach the question of verification from a safety-case perspective: the primary teaching goal is to impart students with the ability to look at a verification question and identify what formal methods are applicable, which tools are available, what the outputs from those tools will say about the system, and what they will not, e.g., what parts of the safety case need to be provided by other means. We overview the lectures, exercises, exams, and student projects in a mixed-level (undergraduate/graduate) Applied Formal Methods course taught in an Aerospace Engineering department. We highlight the approach, tools, and techniques aimed at imparting a good sense of both the state of the art and the state of the practice of formal methods in an effort to effectively prepare students headed for jobs in an increasingly formal world.
On Teaching Applied Formal Methods in Aerospace Engineering