| Presentation | 2017-03-16 Verification Methods of real-time properties for embedded assembly program Satoshi Yamane, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | It is important to verify both the correctness and real-time properties for embedded systems. In this paper, we propose model checking and deductive verification method in order to verify real-time properties as folllows: (1)First we construct a state transition system including the execution time by dynamic program analysis. (2)Next we verify whether a state transition system satisfies RTCTL formulas by model checking. (3)Next we verify whether a state transition system satisfies RTLTL formulas by deductive verification. (4)Finally we explain CEGAR for model checking and deductive verification. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Embedded assembly program / verifying real-time properties / model checking / deductive verification / CEGAR |
| Paper # | MSS2016-83 |
| Date of Issue | 2017-03-09 (MSS) |
| Conference Information | |
| Committee | MSS |
|---|---|
| Conference Date | 2017/3/16(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Shimane Univ. |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Satoshi Yamane(Kanazawa Univ.) |
| Vice Chair | Morikazu Nakamura(Univ. of Ryukyus) |
| Secretary | Morikazu Nakamura(Yamaguchi Univ.) |
| Assistant | Hideki Kinjo(Okinawa Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Mathematical Systems Science and its applications |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Verification Methods of real-time properties for embedded assembly program |
| Sub Title (in English) | Model checking and deductive verification for embedded program |
| Keyword(1) | Embedded assembly program |
| Keyword(2) | verifying real-time properties |
| Keyword(3) | model checking |
| Keyword(4) | deductive verification |
| Keyword(5) | CEGAR |
| 1st Author's Name | Satoshi Yamane |
| 1st Author's Affiliation | Kanazawa University(Kanazawa Univ.) |
| Date | 2017-03-16 |
| Paper # | MSS2016-83 |
| Volume (vol) | vol.116 |
| Number (no) | MSS-525 |
| Page | pp.pp.11-16(MSS), |
| #Pages | 6 |
| Date of Issue | 2017-03-09 (MSS) |