Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1109/ICIS.2015.7166639 | 2015 IEEE/ACIS 14th International Conference on Computer and Information Science (ICIS) |
Keywords | Field | DocType |
gasoline direct injection engine PCM,powertrain control module,PCM,electronic control unit,faulty software,formal modeling,formal specification language,I/O-automaton theory,forward simulation,trace inclusion,abstract version,engine ignition timing,theorem-proving | Specification language,Ignition system,Automotive engineering,Ignition timing,Powertrain control module,Simulation,Computer science,Correctness,Gasoline direct injection,Formal specification,Electronic control unit | Conference |
Citations | PageRank | References |
0 | 0.34 | 3 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yamauchi, M. | 1 | 1 | 0.77 |
| Nobuhiro Ito | 2 | 6 | 2.40 |
| Kawabe, Y. | 3 | 1 | 1.79 |