文献

J-GLOBAL ID：201802272832896139   整理番号：18A1575711

SMTに基づくクロック制約言語CCSLの形式的手法とツール【JST・京大機械翻訳】

SMT-Based Approach to Formal Analysis of CCSL with Tool Support

著者 (2件)： Ying Yunhui (華東師范大学計算机科学与軟件工程学院,上海200062;高可信軟件国家重点実験室(華東師范大学),上海200062) ,  Zhang Min (華東師范大学計算机科学与軟件工程学院,上海200062;高可信軟件国家重点実験室(華東師范大学),上海200062)
資料名： Ruanjian Xuebao  (Ruanjian Xuebao)
巻： 29  号： 6  ページ： 1595-1606  発行年： 2018年 
JST資料番号： C2542A  ISSN： 1000-9825  CODEN： RUXUEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： クロック制約言語CCSLは,リアルタイム組込みシステムにおけるイベント間の制約を記述するための形式的言語である。それはUMLがリアルタイム組込みシステムモデリングの拡張パッケージMARTE(modelingandanalysisofreal-timeandembeddedsystems)に時間モデリングに用いる一つの子言語である。CCSLによって定義されたクロック制約を与えられたとき,あるスケジューリング戦略が制約を満たしているかどうか,そして,これらの制約を満たすすべての行動が,システムデッドロックの分析を起こさないかどうかを判断した。現在、CCSLに対する正式な研究作業、例えば状態遷移システムと時間オートマトンに基づく方法などはすでにある。しかし、これらの方法はある特定の分析のみに対して、一部のCCSL制約にしか適用できないため、分析効率が低い。SMTに基づく統一的で効率的なCCSL形式解析法を提案した。統一性はその有効性証明、痕跡分析、デッドロック検出、LTLモデル検査などの方面の検証と分析に応用できる。この方法に基づいてプロトタイプツールを開発し,上記4つの検証機能を同時にサポートした。ツールは,現在の最も効率的なSMTソルバZ3とCVC4を統合した。SMTソルバーの高効率性により、実験中の大部分の検証は短時間で完成できる。Data from Wanfang. Translated by JST.【JST・京大機械翻訳】

シソーラス用語： 痕跡分析 ,  *クロック ,  モデル検査 ,  デッドロック ,  モデリング ,  *言語 ,  スケジューリング ,  プロトタイプ
準シソーラス用語： 高効率 ,  ソルバ ,  デッドロック検出 ,  時間付きオートマトン ,  状態遷移 ,  リアルタイム組込みシステム , 【Automatic Indexing@JST】

著者キーワード (7件)： CCSL ,  SMT ,  validity proving ,  trace analysis ,  deadlock detection ,  LTL model checking ,  tool

分類 (1件)： 計算機網  (JC03000K)

タイトルに関連する用語 (6件)： SMT ,  クロック ,  制約 ,  言語 ,  形式的手法 ,  ツール