文献

J-GLOBAL ID：200902286595281868   整理番号：09A0864551

データ構造に関する仕様を含め検証できるC言語プログラム部品検証ツールCForge

CForge Modular Verification Tool for C Programs Including Specifications of Data Structures

著者 (3件)： 酒井政裕 (東芝) ,  今井健男 (東芝) ,  片岡欣夫 (東芝)
資料名： 東芝レビュー  (Toshiba Review)
巻： 64  号： 8  ページ： 20-23  発行年： 2009年08月01日 
JST資料番号： F0360A  ISSN： 0372-0462  CODEN： TORBA  資料種別： 逐次刊行物 (A)
記事区分： 解説  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 東芝は,“仕様を基点としたソフトウェア高信頼化”というコンセプトで,ソフトウェアの信頼性向上に取り組んでいる。その一環として,仕様とプログラム部品を対応付けながらメンテナンスを行うことで,プログラムの改変・拡張時の信頼性を確保することを目指している。今回,仕様とC言語プログラム部品の整合性の静的検証を行うツールCForgeを開発した。これはデータ構造とポインタを扱うことができ,また,仕様に基づいて網羅的に検証できる。(著者抄録)

シソーラス用語： *データ構造 ,  *C言語 ,  *プログラム検証 ,  ソフトウェア開発 ,  *仕様記述 ,  二分探索 ,  仕様記述言語 ,  ソフトウェア仕様

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

引用文献 (8件)：

• Parnas, D. “Software Aging”. Proceedings of the 16th International Conference on Software Engineering. Sorrento. Italy.1994-05, ACM and IEEE Computer Society. p. 279-287.
• 経済産業省: 情報処理推進機構. “2008年度組込みソフトウェア産業実態調査報告書”. 情報処理推進機構ソフトウェアエンジニアリング.<http://sec.ipa.go.jp/reports/20080715.html>,(参照2009-04-15).
• 酒井政裕, ほか. “CForge: C言語プログラムのための有界検査ツール”. 第11回プログラミングおよびプログラミング言語ワークショップ論文集. 岐阜.2009-03. 日本ソフトウェア科学会プログラミング論研究会. p. 118-132.
• Jackson, D. Software Abstractions: Logic, Language, And Analysis. Cambridge, MA, The MIT Press, 2006, 366p.
• Dennis, G; Yessenov, K. Forge: Bounded Program Verification. <http://sdg.csail.mit.edu/forge/>, 2009-04-15).

タイトルに関連する用語 (5件)： データ構造 ,  仕様 ,  検証 ,  C言語 ,  ツール