| Presentation | 2010-06-22 Semi-automated Modeling of Interrupt Behavior Control with Promela Kenji TADANO, Yoshinao ISOBE, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Reverse engineering using model checking techniques is effective as a method to improve embedded software quality. However, modeling interrupt behavior control is a highly challenging task for a designer and manually-modeling can cause some errors. This study proposes a semi-automated modeling method of interrupt behavior control while developing an automatic transformation tool and applying it to a real system. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | model checking / embedded software / Promela / interrupt |
| Paper # | CAS2010-24,VLD2010-34,SIP2010-45,CST2010-24 |
| Date of Issue |
| Conference Information | |
| Committee | VLD |
|---|---|
| Conference Date | 2010/6/14(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | VLSI Design Technologies (VLD) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Semi-automated Modeling of Interrupt Behavior Control with Promela |
| Sub Title (in English) | |
| Keyword(1) | model checking |
| Keyword(2) | embedded software |
| Keyword(3) | Promela |
| Keyword(4) | interrupt |
| 1st Author's Name | Kenji TADANO |
| 1st Author's Affiliation | FeliCa Networks, inc.() |
| 2nd Author's Name | Yoshinao ISOBE |
| 2nd Author's Affiliation | National Institute to Advanced Industrial Science and Technology |
| Date | 2010-06-22 |
| Paper # | CAS2010-24,VLD2010-34,SIP2010-45,CST2010-24 |
| Volume (vol) | vol.110 |
| Number (no) | 87 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |