| Presentation | 2017-06-20 Deductive Verification Method of real-time safety 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 deductive verification method in order to verify real-time safety properties based on discrete time as folllows: (1)First we construct a state transition system including the execution time. (2)Next we verify whether a state transition system satisfies RTLTL formulas by deductive verification. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | embedded assembly program / verifying real-time safety properties / deductive verification / real-time temporal logic |
| Paper # | CAS2017-12,VLD2017-15,SIP2017-36,MSS2017-12 |
| Date of Issue | 2017-06-12 (CAS, VLD, SIP, MSS) |
| Conference Information | |
| Committee | SIP / CAS / MSS / VLD |
|---|---|
| Conference Date | 2017/6/19(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Niigata University, Ikarashi Campus |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Masahiro Okuda(Univ. of Kitakyushu) / Mitsuru Hiraki(Renesas) / Morikazu Nakamura(Univ. of Ryukyus) / Hiroyuki Ochi(Ritsumeikan Univ.) |
| Vice Chair | Shogo Muramatsu(Niigata Univ.) / Naoyuki Aikawa(TUS) / Hideaki Okazaki(Shonan Inst. of Tech.) / Shigemasa Takai(Osaka Univ.) / Noriyuki Minegishi(Mitsubishi Electric) |
| Secretary | Shogo Muramatsu(Chiba Inst. of Tech.) / Naoyuki Aikawa(Takushoku Univ.) / Hideaki Okazaki(Renesas) / Shigemasa Takai(Shonan Inst. of Tech.) / Noriyuki Minegishi(Toshiba) |
| Assistant | Masayoshi Nakamoto(Hiroshima Univ.ひろ) / Yohei Nakamura(Hitachi) / Hideki Kinjo(Okinawa Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Signal Processing / Technical Committee on Circuits and Systems / Technical Committee on Mathematical Systems Science and its applications / Technical Committee on VLSI Design Technologies |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Deductive Verification Method of real-time safety properties for embedded assembly program |
| Sub Title (in English) | □≦TIME q = □(q∧(time≦TIME)) |
| Keyword(1) | embedded assembly program |
| Keyword(2) | verifying real-time safety properties |
| Keyword(3) | deductive verification |
| Keyword(4) | real-time temporal logic |
| 1st Author's Name | Satoshi Yamane |
| 1st Author's Affiliation | Kanazawa University(Kanazawa Univ.) |
| Date | 2017-06-20 |
| Paper # | CAS2017-12,VLD2017-15,SIP2017-36,MSS2017-12 |
| Volume (vol) | vol.117 |
| Number (no) | CAS-96,VLD-97,SIP-98,MSS-99 |
| Page | pp.pp.59-64(CAS), pp.59-64(VLD), pp.59-64(SIP), pp.59-64(MSS), |
| #Pages | 6 |
| Date of Issue | 2017-06-12 (CAS, VLD, SIP, MSS) |