抄録
部品再利用によるソフトウェア合成は開発コスト低減や信頼性向上に有効であるが，高信頼な部品の整備が容易でなく，また，適用可能な問題領域が限定される点が問題となる．本稿ではこの問題に対してモデル充足ソフトウェア合成（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.