文献

J-GLOBAL ID：201902251721585679   整理番号：19A0516453

スピンによる実生活SDL仕様のシミュレーションと検証のための自動モデル抽出の適用【JST・京大機械翻訳】

Applying Automated Model Extraction for Simulation and Verification of Real-Life SDL Specification With Spin

著者 (3件)： Vlaovic Bostjan (Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia) ,  Vreze Aleksander (Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia) ,  Brezocnik Zmago (Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, Slovenia)
資料名： IEEE Access  (IEEE Access)
巻： 5  ページ： 5046-5058  発行年： 2017年 
JST資料番号： W2422A  ISSN： 2169-3536  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 形式的に定義された仕様記述言語(SDL)は,複雑な安全性-臨界システムの設計と仕様のために使用される。製品の仕様における各変化は,要求仕様に対して直ちに形式的にチェックされなければならない。本論文は,半自動化システム抽象化,自動化モデル抽出,シミュレーション,および現実の複雑なSDL仕様の形式的検証を提示した。著者らのsdl2pml自動化モデル抽出ツールに実装された音響アルゴリズムは,SDLシステムのすべての特性を保存する。sdl2pmlは,離散時間,抽象化,および動的プロセス生成,合理的データタイプ,および1つ以上のプロセスインスタンスを有する通信のようなすべての関連するSDL機能性と構築のためのサポートの著者らのモデルを含んでいる。著者らの知る限りでは,それらのほとんどは他の既知のアプローチによって支持されていない。SpinRCPツールを用いて,Spinモデルチェッカーによる抽出モデルのシミュレーションと形式的検証を行った。著者らは,SI3000ソフトウェアスイッチからのISDNユーザ適応プロトコルに関する著者らのアプローチの適用性を実証した。抽出されたPromelaモデルはSpinによってこれまで処理された最大のものである。著者らは,Spinシミュレーションとモデル検査がそのような巨大なモデルにうまく適用できることを示した。Copyright 2019 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 自動化 ,  音響 ,  モデル検査 ,  データ型 ,  臨界 ,  アルゴリズム ,  スイッチ ,  適応性 ,  *モデル ,  仕様記述言語 ,  ソフトウェア ,  *シミュレーション
準シソーラス用語： 機能性 ,  動的プロセス ,  自動化システム , 【Automatic Indexing@JST】

分類 (5件)： 図形・画像処理一般  (JE04010I) ,  信号理論  (ND02020G) ,  パターン認識  (JE07000S) ,  音声処理  (JE05000E) ,  音響信号処理  (BB03050C)

タイトルに関連する用語 (6件)： スピン ,  SDL ,  仕様 ,  シミュレーション ,  検証 ,  モデル