| IEICE Technical Committee Submission System Conference Paper's Information |
Online Proceedings [Sign in] Tech. Rep. Archives |
| Go Top Page | Go Previous | [Japanese] / [English] |
| Paper Abstract and Keywords | ||
| Presentation | 2009-03-12 15:15 Formal verification of GALS system designs using UPPAAL Kazuaki Kirita, Tomoyuki Yokogawa, Hisashi Miyazaki, Yoichiro Sato, Michiyoshi Hayase (Okayama Pref. Univ.)  VLD2008-150 |
|
| Abstract | (in Japanese) | (See Japanese page) |
| (in English) | To design GALS (Globally Asynchronous Locally Synchronous) systems, it is necessary to verify the correctness of behavior of the system formally. To verify asynchronous systems such as the GALS systems, the systems need to be modeled as continuous time systems. The previous methods to verify GALS systems formally, however, modeled the systems in discrete time. In this paper, we propose a method to verify a design of GALS system using model checker UPPAAL which employs continuous time. We propose a method to translate STPN (Stochastic Timed Petri Nets) model which represents a GALS system into extended Timed Automata and implement the proposed method. Finally, we show the availability of the proposed method by applying it to an STPN which models a GALS system. |
|
| Keyword | (in Japanese) | (See Japanese page) |
| (in English) | GALS systems / STPN / UPPAAL / model checking / timed automaton / / / | |
| Reference Info. | IEICE Tech. Rep., vol. 108, no. 478, VLD2008-150, pp. 141-146, March 2009. | |
| Paper # | VLD2008-150 | |
| Date of Issue | 2009-03-04 (VLD) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| Copyright and reproduction |
All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| Download PDF | VLD2008-150 |
|
| Conference Information | |
| Committee | VLD |
| Conference Date | 2009-03-11 - 2009-03-13 |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Design Technology for a System-on-Silicon |
| Paper Information | |
| Registration To | VLD |
| Conference Code | 2009-03-VLD |
| Language | Japanese |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Formal verification of GALS system designs using UPPAAL |
| Sub Title (in English) | |
| Keyword(1) | GALS systems |
| Keyword(2) | STPN |
| Keyword(3) | UPPAAL |
| Keyword(4) | model checking |
| Keyword(5) | timed automaton |
| Keyword(6) | |
| Keyword(7) | |
| Keyword(8) | |
| 1st Author's Name | Kazuaki Kirita |
| 1st Author's Affiliation | Okayama Prefectural University (Okayama Pref. Univ.) |
| 2nd Author's Name | Tomoyuki Yokogawa |
| 2nd Author's Affiliation | Okayama Prefectural University (Okayama Pref. Univ.) |
| 3rd Author's Name | Hisashi Miyazaki |
| 3rd Author's Affiliation | Okayama Prefectural University (Okayama Pref. Univ.) |
| 4th Author's Name | Yoichiro Sato |
| 4th Author's Affiliation | Okayama Prefectural University (Okayama Pref. Univ.) |
| 5th Author's Name | Michiyoshi Hayase |
| 5th Author's Affiliation | Okayama Prefectural University (Okayama Pref. Univ.) |
| 6th Author's Name | |
| 6th Author's Affiliation | () |
| 7th Author's Name | |
| 7th Author's Affiliation | () |
| 8th Author's Name | |
| 8th Author's Affiliation | () |
| 9th Author's Name | |
| 9th Author's Affiliation | () |
| 10th Author's Name | |
| 10th Author's Affiliation | () |
| 11th Author's Name | |
| 11th Author's Affiliation | () |
| 12th Author's Name | |
| 12th Author's Affiliation | () |
| 13th Author's Name | |
| 13th Author's Affiliation | () |
| 14th Author's Name | |
| 14th Author's Affiliation | () |
| 15th Author's Name | |
| 15th Author's Affiliation | () |
| 16th Author's Name | |
| 16th Author's Affiliation | () |
| 17th Author's Name | |
| 17th Author's Affiliation | () |
| 18th Author's Name | |
| 18th Author's Affiliation | () |
| Speaker | Author-1 |
| Date Time | 2009-03-12 15:15:00 |
| Presentation Time | 25 minutes |
| Registration for | VLD |
| Paper # | VLD2008-150 |
| Volume (vol) | vol.108 |
| Number (no) | no.478 |
| Page | pp.141-146 |
| #Pages | 6 |
| Date of Issue | 2009-03-04 (VLD) |
[Return to Top Page]