MALPAS ソフトウェア静的解析ツールセット
MALPAS ソフトウェア静的解析ツールセット
開発者アトキンス
オペレーティング·システムウィンドウズ
タイプ静的プログラム解析
ライセンス独自の
Webサイトwww.malpas-global.com​​

MALPASは、厳密な静的プログラム解析を適用することで、ソフトウェアの正しさを調査および証明する手段を提供するソフトウェアツールセットです。このツールは、有向グラフと正規代数を用いて解析対象プログラムを表します。MALPASの自動化ツールを使用することで、解析者はプログラムの構造を記述し、データの使用状況を分類し、入力データと出力データ間の情報関係を提供できます。また、コードが仕様を満たしていることを 正式に証明することもできます。

MALPASは、原子力[ 1 ] 、航空宇宙[ 2 ]、防衛[ 3 ]産業における安全性が極めて重要なアプリケーションの正当性を確認するために使用されています。また、原子力産業において、 Sizewell B [ 4 ]におけるコンパイラの正当性を確認するためにも使用されています。分析対象言語には、Ada、C、PLM、Intelアセンブラなどがあります。

MALPASは、多くのプログラミング言語を扱う際の厳密さと柔軟性により、英国健康安全執行部の原子炉用コンピュータベース保護システムのガイダンスで要求される独立した静的解析に適しています。 [ 5 ]

技術概要

MALPASツールセットは、プログラムの様々な特性に対応する5つの特定の解析ツールで構成されています。アナライザーへの入力は、MALPAS中間言語（IL）で記述する必要があります。これは、手書きすることも、元のソースコードから自動翻訳ツールで生成することもできます。自動翻訳ツールは、Ada、C、Pascalなどの一般的な高級プログラミング言語、およびIntel 80*86、PowerPC、68000などのアセンブラ言語用として存在します。ILテキストは、「ILリーダー」を介してMALPASに入力され、分析対象プログラムの有向グラフと関連するセマンティクスを構築します。グラフは、一連のグラフ縮小技術を使用して縮小されます。

MALPASツールセットは5つのアナライザーで構成されています: [ 6 ]

  1. 制御フローアナライザー。プログラム構造を解析し、エントリポイント/終了ポイント、ループ、分岐、到達不能コードといった主要な特徴を特定します。望ましくない構造に注意を喚起し、プログラム構造の複雑さを示す概要レポートを提供します。
  2. データ使用アナライザー。プログラムで使用される変数とパラメータを、その用途に応じて異なるクラスに分類します。（例：書き込み前に読み取られるデータ、読み取られずに書き込まれるデータ、または読み取りを挟まずに2回書き込まれるデータ）。このレポートでは、初期化されていないデータや、すべてのパスに書き込まれていない関数出力などのエラーを特定できます。
  3. 情報フローアナライザー。これは、各出力変数またはパラメータのデータと分岐の依存関係を特定します。コード全体のパスにおいて、不要な依存関係や予期しない依存関係を明らかにすることができます。また、未使用の変数や冗長なステートメントに関する情報も提供されます。
  4. セマンティックアナライザー（シンボリック実行とも呼ばれます）。これは、コード内の意味的に実行可能なすべてのパスにおける、すべての入力と出力間の正確な機能的関係を明らかにします。
  5. コンプライアンスアナライザー。これは、コードの数学的動作を正式なIL仕様と比較し、両者の相違点を詳細に示します。IL仕様は、前提条件と事後条件、そしてオプションのコードアサーションとして記述されます。コンプライアンス分析は、仕様に対するコードの機能的正確性について、非常に高いレベルの信頼性を得るために使用できます。

歴史

このツールセットのオリジナル研究と初期世代は、英国マルバーンにある英国王立信号・レーダー研究所（RSRE）によって開発されました（これがMALvern Programming Analysis Suiteという名称の由来です）。1980年代には、民生用原子力・兵器分野で広く使用され、Rex, Thompson and Partners社による支援を受け、MALPASユーザーグループが設立されました。初代議長はDavid H. Smith氏（現Frazer-Nash社）で、その後Advantage Technical Consulting社（ 2008年にAtkins社に買収）が務めました。

最初の大規模静的解析タスクは、サイズウェルB発電所の一次原子炉保護システムでした。これは、壊滅的な故障に対する第一防衛線としてコンピュータベースの保護システムを採用した英国初の原子力発電所でした。さらに、チェコ共和国のCEZは、テメリン原子力発電所の原子炉保護システムの信頼性を高めるためにMALPASを採用しました。1995年、英国空軍は、安全性が重要と評価されたロッキード・マーティンC130Jの航空電子機器ソフトウェアの独立した解析を委託しました。MALPASは、Spark Adaで記述され、Sparkツールセットで検証されたミッションコンピュータソフトウェアとは別に、このソフトウェアの解析に使用されました。[ 7 ] MALPASは現在、ヒンクリーポイントCの2基の原子炉を監視する原子炉保護システムのソフトウェアを独立して評価するために使用されています。[ 8 ]

参考文献

  1. ^英国原子力発電所におけるプログラム可能な保護：10年後、D Pavey、ブリティッシュ・エナジー。http ://entrac.iaea.org/I-and-C/TM_VTT_2005_11/IAEA_papers/051124_Thursday/IAEA_paper_Pavey.pdf
  2. ^ 「C-130J ヘラクレスの安全性重視ソフトウェアの静的コード分析、Eur Ing KJ Harrison、BSc CPhys MinstP CEng MRAeS MBCS、Aerosystems International、英国」(PDF) 。 2011年9月27日時点のオリジナル(PDF)からアーカイブ。 2011年3月18日閲覧。
  3. ^ MALPASツールを用いた兵器ソフトウェアの分析、Hayman, K.、国防科学技術機関、ソールズベリー、SA。http ://www.dsto.defence.gov.au/publications/scientific_record.php ?record=9074
  4. ^ソースコードとPROMの内容の等価性の形式的証明、IMAディペンダブルシステム数学会議議事録、オックスフォード大学出版局、1995年、pp225-248D J PaveyおよびLA Winsborrow
  5. ^ 「コンピュータベースの安全システム - デジタルコンピュータベースの保護システムのソフトウェア的側面を評価するための技術ガイダンス」 。2011年7月4日時点のオリジナルよりアーカイブ。
  6. ^静的解析に関する産業的視点。ソフトウェアエンジニアリングジャーナル、1995年3月号、69-75ページ。Wichmann, BA, AA Canning, DL Clutterbuck, LA Winsbarrow, NJ Ward, DWR Marsh. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf 2011年9月27日アーカイブ、 Wayback Machineより
  7. ^ C-130J ヘラクレス機の安全性重視ソフトウェアの静的コード分析「アーカイブコピー」（PDF） 。 2011年9月27日時点のオリジナル（PDF）からアーカイブ。 2011年3月18日閲覧。{{cite web}}: CS1 maint: アーカイブされたコピーをタイトルとして (リンク)
  8. ^ Horgan, Rob (2020年4月26日). 「アトキンス社がヒンクリー・ポイントCの安全契約を獲得」 .
「 https://en.wikipedia.org/w/index.php?title=MALPAS_Software_Static_Analysis_Toolset&oldid=1305898039」から取得