This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.
Critical Embedded Systems Development Using Formal Methods and Statistical Reliability Metrics