文献

J-GLOBAL ID：202202220074758208   整理番号：22A0795901

安全臨界システムのためのシーケンス図の形式検証一貫性【JST・京大機械翻訳】

Formally verifying consistency of sequence diagrams for safety critical systems

著者 (6件)： Chen Xiaohong (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China) ,  Liu Qianqian (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China) ,  Mallet Frederic (Universite Cote d’Azur, CNRS, Inria, I3S, France) ,  Li Qin (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China) ,  Cai Shubin (College of Computer Science and Software Engineering, Shenzhen University, China) ,  Jin Zhi (School of Computer Science, Peking University, Beijing, China)
資料名： Science of Computer Programming  (Science of Computer Programming)
巻： 216  ページ： Null  発行年： 2022年 
JST資料番号： H0806A  ISSN： 0167-6423  CODEN： SCPGD4  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： UML相互作用,akaシーケンスダイアグラムは,設計下のシステムの良好なまたは悪い挙動の期待されるシナリオを記述するために,技術者によって頻繁に使用され,それらは,非常に多様な挙動を表現するための単純な十分な構文を提供する。本論文では,要求の一貫性をチェックする後に,シナリオが次第に精緻化される,インクリメンタルな方法で安全クリティカルシステムに対する安全要求を表現するためにそれらを使用した。これらのシナリオの意味論は,それらを形式的検証に従う中間意味モデルに変換することによって表現される。本論文では,中間の意味言語としてクロック制約仕様言語(CCSL)に依存する。いくつかの意味で,シーケンス図とCCSL制約は,有限実行トレースの有限集合によって与えられた挙動を含む,許容できる無限トレースのファミリーを表現し,それに対して検証した。これらの要求を実際の実行トレースと比較し,著者らの変換の妥当性を証明した。シーケンスダイアグラムの一貫性をチェックするために,SMTとクロックグラフに基づく2つの検証方法をそれぞれ提示する。SMTベースの方法は,CCSL制約を分析するためにMyCCSLと呼ばれる解析ツールに依存する。クロックグラフベースの方法は,クロックグラフにCCSL制約条件を変換して,クロックグラフを横断することによって解析を行う。最後に,これらの2つの方法を鉄道輸送システムからの実際の事例に対して評価した。結果は,SMTベースの方法が正確で遅い解析を提供するのに対して,クロックグラフベースの方法は,SMTベースの方式によって見つかる2種類の典型的不整合を狙って,検証効率を劇的に増加させることを示した。Copyright 2022 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 相互作用 ,  *安全性 ,  意味論 ,  言語 ,  クロック ,  鉄道輸送 ,  *臨界 ,  *図面 ,  挙動 ,  *検証 ,  制約条件 ,  トレース【計算機】 ,  シナリオ ,  仕様記述言語
準シソーラス用語： *シーケンス図 ,  構文 , 【Automatic Indexing@JST】

著者キーワード (5件)： 安全臨界システム ,  シーケンス図 ,  行動モデル ,  クロックグラフ ,  形式的検証

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： 臨界 ,  シーケンス図 ,  形式検証