文献

J-GLOBAL ID：202102255563063926   整理番号：21A2350902

シナリオベース仕様のSATおよびLP協調有界タイミング解析【JST・京大機械翻訳】

SAT and LP Collaborative Bounded Timing Analysis of Scenario-Based Specifications

著者 (4件)： Lu Longlong (Nanjing University, CN) ,  Yang Wenhua (Nanjing University of Aeronautics and Astronautics, CN) ,  Pan Minxue (Nanjing University, CN) ,  Zhang Tian (Nanjing University, CN)
資料名： ACM Proceedings  (ACM Proceedings)
号： Internetware’20  ページ： 229-239  発行年： 2020年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： メッセージシーケンスチャートとUML相互作用モデルのようなシナリオベース仕様(SBS)のタイミング解析は,リアルタイムシステム開発の設計段階で本質的な役割を果たす。しかし,タイミング制約の充足可能性に関する解析を行うためには時間がかかり,労働集約的である。本論文では,SBSのためのTASSATと名付けた新しいSATおよび線形計画法(LP)協調タイミング解析手法を提案した。深さ優先横断アルゴリズムを使用する代わりに,TASSATはSBSの構造を命題式に符号化し,SATソルバを用いて候補経路を見つける。次に,候補経路のタイミング解析をLP問題に縮小し,そこでは,実行不可能な経路の既約実行不可能な集合をSATソルバの不要な探索空間を剪定するために使用できる。実験結果は,TASSATが効果的であり,時間消費とメモリフットプリントの両方に関して既存のツールより良い性能を提供することを示した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  記憶装置 ,  線形計画法 ,  相互作用 ,  実時間処理 ,  命題 ,  *タイミング解析 ,  モデル検査
準シソーラス用語： 探索空間 ,  フットプリント ,  ソルバ ,  *有界 ,  タイミング制約 , 【Automatic Indexing@JST】

著者キーワード (5件)： SAT ,  シナリオベース仕様 ,  UML相互作用モデル ,  モデル検査 ,  到達可能性解析

分類 (5件)： 計算機システム開発  (JD02010R) ,  ディジタル計算機方式一般  (JC02010O) ,  CAD,CAM  (JE10000A) ,  無線通信一般  (ND08010L) ,  集積回路一般  (NC03161C)

タイトルに関連する用語 (7件)： シナリオ ,  仕様 ,  SAT ,  LP ,  協調 ,  有界 ,  タイミング解析