文献

J-GLOBAL ID：201802266897979346   整理番号：18A1144551

サイバー物理システムのモデルベース解析のためのPVS-Simulink統合環境【JST・京大機械翻訳】

A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems

著者 (3件)： Bernardeschi Cinzia (Department of Information Engineering, University of Pisa, PI, Italy) ,  Domenici Andrea (Department of Information Engineering, University of Pisa, PI, Italy) ,  Masci Paolo (HASLab/INESC TEC and Universidade do Minho, Braga, Portugal)
資料名： IEEE Transactions on Software Engineering  (IEEE Transactions on Software Engineering)
巻： 44  号： 6  ページ： 512-533  発行年： 2018年 
JST資料番号： D0480D  ISSN： 0098-5589  CODEN： IESEDJ  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 本論文では,サイバー物理システムにおけるソフトウェア部品の形式的モデリングと解析のための支援ツールを用いた方法論を提示した。著者らのアプローチを用いて,開発者はソフトウェアコンポーネントの論理ベース仕様のシミュレーションと連続プロセスのSimulinkモデルを統合することができる。統合シミュレーションは,開発過程における初期の離散システム構成要素の特性を検証するために有用である。同じ論理ベースの仕様も,プロトタイプ検証システム(PVS)を用いて形式的に検証することができ,ソフトウェア設計が特定の安全要件に従うという付加的な信頼性を得ることができる。モデリングパターンは,より身近なオートマトンベースの形式から論理ベースの仕様を生成するために定義される。本研究の究極の目的は,典型的に異なる形式とツールの統合使用を必要とするサイバー物理システムのソフトウェア開発プロセスにおける形式的検証技術の導入を容易にすることである。医療領域からの事例研究を用いてアプローチを説明した。ペースメーカーのPVSモデルをヒト心臓のSimulinkモデルと結びつけた。全体的なサイバー物理システムは,関連する試験シナリオの調査を通して設計要件を検証するために共同シミュレーションされる。ペースメーカー設計の特定の安全性に対するペースメーカーモデルに対して,PVS定理証明器による形式的検証を示した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【JST・京大機械翻訳】

シソーラス用語： 事例研究 ,  ソフトウェアコンポーネント ,  離散系 ,  シミュレーション ,  心臓 ,  定理証明 ,  *モデリング ,  信頼性 ,  ソフトウェアプロセス ,  ヒト ,  ソフトウェア設計 ,  安全性 ,  プロトタイプ
準シソーラス用語： 支援ツール ,  *Simulink , 【Automatic Indexing@JST】

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (5件)： 物理 ,  モデルベース解析 ,  Simulink ,  統合 ,  環境