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.