Oda TAKESHI (織田 健)

部品再利用によるソフトウェア合成は開発コスト低減や信頼性向上に有効であるが，高信頼な部品の整備が容易でなく，また，適用可能な問題領域が限定される点が問題となる．本稿ではこの問題に対してモデル充足ソフトウェア合成（MSSS）を提案する．MSSSは形式手法B Methodの信頼性保証を応用したモデル充足細粒度部品に数学的判定による健全性の高い再利用を適用してソフトウェアを合成する．これにより部品の信頼性を静的に保証でき，また変数名や部品名の解釈に起因する誤りを排除できる．一方で変数名や部品名に意味を持たせないため，部品名での機能の呼び出しによる合成ができず，変数名の書き換えや結合が必要になる．よって，本稿ではMSSSの信頼性を'モデル充足'として数学的に定義し，そこからMSSSの手順を定めることで，互いに矛盾しない部品群を再利用したソフトウェアがB Methodの信頼性を満たすことを保証する．また，MSSSでは要求仕様を一意の粒度に細分化して部品の仕様に対する検索キーとするため，検索キーを不足部品の仕様として提示でき，さらに，部品自動生成により部品を容易に整備できる．これにより，合成手法を適用可能な問題領域の拡大と，それによる高信頼ソフトウェア開発の低コスト化と迅速化が期待できる．Software synthesis by reusing software components is effective to reduce development cost and to increase dependency. Nevertheless, it is not easy to prepare components, so domains to apply synthesis are limited. we must prepare components for each software domain to apply synthesis, and it's difficult to prepare dependable components. In this paper, we propose 'Model Satisfiable Software Synthesis (MSSS)' to resolve these problems. MSSS synthesises software by reusing 'Model Satisfiable Fine-grained Component (MSFC)' mathematically. We can ensure static dependability of MSFC by B Method. And mathematical reuse prevents bugs caused by misunderstanding of function name. However, MSSS needs intricate rewriting and combination to interlock MSFCs, because we can't reuse them by name of function. So we define mathematical dependency of MSSS as 'model satisfiable' to define procedure of it. MSSS slices requirement uniquely to search components by sliced requirement. So we can make lacked components easily by using search-keys as specification of them. And also we can generate MSFCs from existing software. MSSS will enable us to apply synthesis to more software domains, and to develop dependable software quickly in lower cost.

ソフトウェア部品への形式仕様の付加は部品の再利用性向上に有効である．しかし，再利用によりソフトウェアを開発するためには大量の部品を用意する必要があり，それらに形式仕様を与えることは大きなコストを生じる．これに対して既存ソフトウェアから部品を生成する手法があるが，仕様と部品の整合性保証が不十分である．そこで，本稿では仕様との整合性を保証できる高信頼ソフトウェア部品を提案する．また，この高信頼ソフトウェア部品をB Methodで構築されたソフトウェアから自動生成する手法を提案する．提案する高信頼ソフトウェア部品は実装依存モデルと細分化実装で構成され，仕様として細分化モデルを持つ．細分化モデル，実装依存モデル，細分化実装はそれぞれB Methodのモデルと実装に対応した記述であり，B Methodの信頼性の定義に基づいて信頼性が定義される．この部品の信頼性の定義に基づいて部品自動生成手法を構築することで自動生成された細分化モデルが無矛盾であるための条件を明らかにし，また，実装依存モデルと細分化実装が常に整合性を満たすことを保証する．この自動生成により高信頼部品リポジトリを容易に構築することが可能になる．さらに，高信頼部品リポジトリを応用することでB Methodで記述された要求仕様に対してそれを満たす実装を出力する高信頼自動コード生成が期待できる．Formal specifications help us to reuse software components. But it cost to write formal specifications for all of software components. Automated component generation by slicing existent software is proposed to reduce this cost. But it's not enough in component reliability. In this paper we propose dependable software components (DSC), which can be ensured to satisfy specifications, and propose automated dependable software component generation (DSCG). A DSC is constructed with an implementation dependent model (IDM) and a sliced implementation, and a DSC has sliced model as its specification. These are similar to model and implementation in the B Method, and we can generate proof obligation from them. So we can ensure the consistency of a DSC and its specification applying the B Method. In this paper, we ensure the dependability in two angle by constructing that based on definitions of the DSC's consistency. First, we prove that sliced models generated by the DSCG has no contradiction conditionally. Second, we express the sliced model generated by the DSCG is sure to satisfy the IDM. We'll able to synthesis dependable software by composite DSCs to satisfy requirement models in the B Method.

In software development, if we regard a program as a function, then specifications of this program can be seen as definitions of the relationships between the input and the output data of the program. If the input and output data structures of the program and the relationships between them are stepwise refined and defined, then it is possible to start sortware design even if the details of the requirement and of the data structures have not yet been fully determined. Furthermore, output-oriented analysis and design on stepwise refinement can reduce the need for the intermediate files that are produced during clash handling. In this paper, we will offer a specification methodology, SDR, which approach is based on the stepwise data structure refinement strategy.