論文

査読有り
2017年

Specifying a Distributed Snapshot Algorithm as a Meta-program and Model Checking it at Meta-level

2017 IEEE 37TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS (ICDCS 2017)
  • Ha Thi Thu Doan
  • ,
  • Kazuhiro Ogata
  • ,
  • Francois Bonnet

開始ページ
1586
終了ページ
1596
記述言語
英語
掲載種別
研究論文(国際会議プロシーディングス)
DOI
10.1109/ICDCS.2017.176
出版者・発行元
IEEE COMPUTER SOC

The paper proposes a new approach to model checking Chandy-Lamport Distributed Snapshot Algorithm (CLDSA). The essential of the approach is that CLDSA is specified as a meta-program in Maude such that the meta-program takes a specification of an underlying distributed system (UDS) and generates the specification of the UDS on which CLDSA is superimposed (UDS-CLDSA). To model check that a UDS-CLDSA enjoys a desired property, it suffices that human users specify the UDS for the proposed approach, while human users need to specify the UDS-CLDSA for the existing approach for each UDS. Since the proposed approach conducts model checking at meta-level, it produces a counterexample if a UDS-CLDSA does not enjoy the property, while the existing approach does not. Our method specifying CLDSA as a meta-program can be applied to formal specification of the class of distributed algorithms that are superimposed on UDSs.

リンク情報
DOI
https://doi.org/10.1109/ICDCS.2017.176
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000412759500147&DestApp=WOS_CPL
ID情報
  • DOI : 10.1109/ICDCS.2017.176
  • ISSN : 1063-6927
  • Web of Science ID : WOS:000412759500147

エクスポート
BibTeX RIS