ビジネスモデルイノベーションの形式的記述と検証

○吉田 和樹¹⁾

1) 国立情報学研究所

Abstract

ビジネスモデルイノベーションを形式的に記述し、その実現性を検証するための手法を提案する。

この手法では、モデル化の枠組みとしてビジネスモデルキャンバス(BMC)を、形式的な記述には形式的仕様記述言語の代数的仕様を、また、実現性の検証には等式論理の定理証明器CafeOBJを使用する。

BMCの中でリソースの流れを定型化して記述し、ビジネスモデルパターンを、その記述を組み合わせて、テンプレートとして用意する。

企画・立案段階で、パターンを組み合わせてイノベーションの構想を練る中で、テンプレートを利用して形式的な記述を完成させ、CafeOBJで実現性を検証する。

A method is proposed to specify business model innovation formally and validate its feasibility.

In this method, Business Model Canvas is adopted as an architecture for modeling the activities inside or between the companies. Algebraic Specification, which has been used for specifying software design originally, is used for the modeling together with a theorem prover on equational logic, CafeOBJ.

In BMC, a flow of resources i.e. human, capital, material and information, is specified, and typical business model patterns are made up as templates from the specifications.

In a business planning phase, while formulating an idea of innovation based on the combination of patterns, a formal specification of the innovation is completed using the templates, then its feasibility is validated in CafeOBJ.

Keywords

ビジネスモデルキャンバス，代数的仕様，CafeOBJ

Business Model Canvas，Algebraic Specification，CafeOBJ