Recent embedded software development is becoming larger and more complicated at a rapid pace.
Conventional development focuses on designing basic cases. Therefore, oversights and omissions are often seen in abnormal cases and exceptional cases. Also, designing with sentences or free formats tends to cause discrepancies from specifications because only code parts are modified for errors.
In addition, a lot of man-hours for development are wasted by considerable reworking when errors become obvious for the first time after the program was completed because dynamic verification cannot be done until implementation.
Not only for the areas required to meet functional safety standards, but also for supporting larger and more complicated development, it is necessary to design with formal or semi-formal notation.