In the first report, we show that the finite state machine (FSM) can be extracted from the Japanese requirements specification text using the natural language processing techniques. In this report, we also the more detailed model by the SPARK language, which has the strong verification mechanism, and is runnable on the computer.
By this approach, we can create the more strict requirements specification of the compound embedded system of the automobile, and it is useful from the viewpoint of validation in the early development phase.