Verifying Ignition Timing of Gasoline Direct Injection Engine's PCM

A powertrain control module (PCM) is an electronic control unit for an engine. PCMs are used for almost all automobiles, so faulty software for a PCM may cause a hazardous event or a fatal accident. For software of a gasoline direct injection engine's PCM, a formal modeling was introduced with a formal specification language; specifically, two I/O-automata - a concrete version and an abstract version - were described with a specification language based on I/O-automaton theory. In this paper we theorem-prove a trace inclusion between the two automata. If we prove a binary relation over states satisfies conditions for a forward simulation in I/O-automaton theory, we can prove the trace inclusion. The abstract version is a specification for a timing of engine's ignition, so the inclusion leads to the correctness of concrete version's ignition timing.