文献

J-GLOBAL ID：202002275441746560   整理番号：20A0592065

MSVLによるpythonプログラムのモデル検査【JST・京大機械翻訳】

Model Checking Python Programs with MSVL

著者 (6件)： Shu Xinfeng (School of Computer Science and Technology, Xi’an University of Posts and Telecommunications, Xi’an, China) ,  Gao Fengyun (School of Computer Science and Technology, Xi’an University of Posts and Telecommunications, Xi’an, China) ,  Gao Weiran (School of Computer Science and Technology, Xi’an University of Posts and Telecommunications, Xi’an, China) ,  Zhang Lili (School of Computer Science and Technology, Xi’an University of Posts and Telecommunications, Xi’an, China) ,  Wang Xiaobing (Institute of Computing Theory and Technology and ISN Laboratory, Xidian University, Xi’an, China) ,  Zhao Liang (Institute of Computing Theory and Technology and ISN Laboratory, Xidian University, Xi’an, China)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12028  ページ： 205-224  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： Pythonプログラムの正当性を検証するために,MSVL(モデリング,シミュレーションおよび検証言語)によるPythonプログラムをチェックするための新しいアプローチを提唱した。この目的のために,MSVLのプロセス指向意味論によりPythonのオブジェクト指向意味論を復号化するためのルールを定義し,Pythonプログラムをその等価MSVLプログラムに自動的に書き換える手法を定式化し,モデル検査ツールMSVにより検証した。さらに,この手法がどのように動作するかを例示するための例を示した。このアプローチは,直接的な方法でPythonプログラムを検証するためにMSVLの強力な表現性を完全に利用し,ソフトウェアシステムの品質を改善するのに役立つ。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 復号化 ,  意味論 ,  品質 ,  *モデル検査 ,  定式化 ,  プログラム検証 ,  言語
準シソーラス用語： ソフトウェアシステム ,  表現力 ,  オブジェクト指向 ,  Python , 【Automatic Indexing@JST】

著者キーワード (4件)： MSVL ,  python ,  プログラム検証 ,  モデル検査

分類 (2件)： 計算機システム開発  (JD02010R) ,  その他の計算機利用技術  (JE14000C)

タイトルに関連する用語 (2件)： Python ,  モデル検査