ECLAIR
はソフトウェアについてです。その他の使用法については、
Éclairを参照して
「ECLAIR」
ECLAIRは、 CおよびC ++プログラムの自動分析、検証、テスト、および変換のためにBUGSENG、LLCによって開発された商用の静的コード分析ツールです。
エクレア
開発者 BUGSENG、LLC 安定リリース
3.11.0 / 2021年7月15日 ; 6か月前 （2021-07-15）
オペレーティング・システム
クロスプラットフォーム
タイプ
静的コード分析
ライセンス
専有
Webサイト
www .bugseng .com / eclair
コンテンツ
1 機能
2 も参照してください
3 参考文献
4 外部リンク
機能
ECLAIRは、パルマ大学の応用形式手法研究所で開発された一連のプロトタイプの完全なリエンジニアリングです。抽象解釈やモデル検査などの形式手法ベースの静的コード分析手法を制約充足手法と組み合わせて使用し、ソースコードに特定の実行時エラーがないことを検出または証明し、プログラム分析と検証、プログラムテスト生成およびプログラム変換。
プログラムの分析と検証に関して、ECLAIRは、実行時の異常がないことを静的に検出または証明できるだけでなく、 MISRA C、MISRA C ++、CERT C Secure Coding Standard、CERT C ++ Secureなどのいくつかのコーディング標準に関する適合性を自動的にチェックできます。コーディング標準、 High-Integrity C ++、NASA / JPL C、ESA / BSSC C / C ++、JSF C ++、EC-、 Netrino Embedded C、 The Power of Ten（C）、産業強度C ++。
プログラムテストの場合、ECLAIRは、ユーザー指定のカバレッジ基準に達する単体テスト入力のセットを自動的に合成し、プログラムの実行不可能な条件のためにこのカバレッジを達成できない場合にユーザーに警告します。
プログラム変換に関しては、ECLAIRを使用して複雑なプログラム変換を実行できます。これらは構文およびセマンティクスベースの基準によって指定されます。これらの基準に一致するソース内のプログラム領域は、オプションでパラメーター化された置換に置き換えることができます。
も参照してください
抽象解釈
モデル検査
静的コード分析
静的コード分析のためのツールのリスト
参考文献
^ 「ニュース-BUGSENG」。bugseng.com 。2021-04-04を取得。
^ R。バグナラ; PMヒル; E.ザファネッラ（2007）。「プログラミング言語について推論するためのPrologベースの環境」。arXiv：0711.0345 。
^ Seacord、Robert C.（2013）。CおよびC ++でのセキュアコーディング。ソフトウェア工学のSEIシリーズ（第2版）。アディソン-ウェスリープロフェッショナル。ISBN 978-0-321-82213-0。
^ Hatton、L。（2005）。「EC—組み込みシステム開発に適したISOCの測定ベースのより安全なサブセット」。情報およびソフトウェア技術。47（3）：181–695。CiteSeerX10.1.1.101.7828。_ 土井：10.1016 /j.infsof.2004.08.001。 ^ バー、マイケル（2008）。組み込みCコーディング標準。バーグループ。ISBN 978-1442164826。
^ Gerald、J。（2006）。「10の力：安全クリティカルコードを開発するためのルール」。コンピューター。39（6）：95–97。土井：10.1109 /MC.2006.212。
^ ヘンリクソン、マット; ナイキスト、エリック（1997）。産業用強度C ++。Prentice-HallPTR。ISBN 978-0131209657。
外部リンク
ECLAIRの公式ウェブサイト