データ構造に関する仕様を含め検証できるC言語プログラム部品検証ツール CForge (CForge: Modular Verification Tool for C Programs Including Specifications of Data Structures) Export

@article{citeulike:5793852, abstract = {　東芝は， ” 仕様を基点としたソフトウェア高信頼化”というコンセプトで，ソフトウェアの信頼性向上に取り組んでいる。その一環として，仕様とプログラム部品を対応付けながらメンテナンスを行うことで，プログラムの改変・拡張時の信頼性を確保することを目指している。 　今回，仕様とC言語プログラムの整合性の静的検証を行うツールCForgeを開発した。これはデータ構造とポインタを扱うことができ，また，仕様に基づいて網羅的に検証できる。 Toshiba has been engaged in a software reliability project based on the concept of ” specification-leveraged dependability enhancement.” The basic object of this concept is to preserve consistency between a program and its specifications in the course of further modification or extention of the software. We have developed CForge, a new modular verification tool that can verify consistency between C functions and their specifications In addition it is capable of comprehensive verification including data structures and pointers.}, author = {Sakai, Masahiro and Imai, Takeo and Kataoka, Yoshio}, citeulike-article-id = {5793852}, citeulike-linkout-0 = {http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf}, journal = {東芝レビュー}, keywords = {alloy, c, model-checking}, month = {August}, number = {8}, pages = {20--23}, posted-at = {2009-09-17 02:14:50}, priority = {0}, title = {データ構造に関する仕様を含め検証できるC言語プログラム部品検証ツール CForge (CForge: Modular Verification Tool for C Programs Including Specifications of Data Structures)}, url = {http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf}, volume = {64}, year = {2009} }

TY - JOUR ID - citeulike:5793852 L3 - citeulike-article-id:5793852 N2 - 　東芝は，“仕様を基点としたソフトウェア高信頼化”というコンセプトで，ソフトウェアの信頼性向上に取り組んでいる。その一環として，仕様とプログラム部品を対応付けながらメンテナンスを行うことで，プログラムの改変・拡張時の信頼性を確保することを目指している。 　今回，仕様とC言語プログラムの整合性の静的検証を行うツールCForgeを開発した。これはデータ構造とポインタを扱うことができ，また，仕様に基づいて網羅的に検証できる。 Toshiba has been engaged in a software reliability project based on the concept of “specification-leveraged dependability enhancement.” The basic object of this concept is to preserve consistency between a program and its specifications in the course of further modification or extention of the software. We have developed CForge, a new modular verification tool that can verify consistency between C functions and their specifications In addition it is capable of comprehensive verification including data structures and pointers. IS - 8 JF - 東芝レビュー EP - 23 TI - データ構造に関する仕様を含め検証できるC言語プログラム部品検証ツール CForge (CForge: Modular Verification Tool for C Programs Including Specifications of Data Structures) VL - 64 SP - 20 KW - alloy KW - c KW - model-checking AU - Sakai, Masahiro AU - Imai, Takeo AU - Kataoka, Yoshio PY - 2009/08// UR - http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf ER -