Vol.3 No.1 2010

41/100

研究論文:臨床情報学のための野外科学的方法(木下ほか)−38−Synthesiology Vol.3 No.1(2010)る数学的対象を与える「解釈」を考える。命題ψが、解釈Mにおいて成立する、ということをMψと書いて、ψはMにおいて真である、という。形式理論の公理をすべて真にするような解釈を特に「モデル」という。どんなモデルに対してもψが成り立つときには ψと書き、ψは「恒真」(valid)である、という。形式理論が与えられた場合、多くの場合には、命題の恒真性に興味があるが、特定のモデルにおける真偽を調べることに興味がある場合もある。与えられたモデルの下での命題の真偽を調べることを「モデル検査」と呼ぶ。形式理論の中でも時相論理と呼ばれる論理に基づく理論におけるモデル検査は、制御プログラムの動的な性質の検査を調べるのに都合が良く、最近ではプログラムの検証での必須の技法の一つになっている。モデル検査を効率よく自動的に実行する「モデル検査器」と呼ばれるソフトウエアツールがいくつも開発されている。モデル検査器は、情報システムの遷移系注3)としての表現と、期待される性質の二つを入力として受け取り、前者が後者を満足するかどうかをYESまたはNOの答えとして返すものである。遷移系が与えられた性質をもたない場合には、反例をも返すのが普通である。反例は、動作に関するシステムの状態系列の形で与えられる。モデル検査器を用いて、システムの欠陥を次のようにして検出する。まず、システムを表現する遷移系を作る。システムは数学的世界とは独立に存在するものだが、それをもとに当面議論したい性質は保ちつつ、システムのその他の面は差し支えない程度に捨象(抽象化)して、数学的な対象である遷移系を作るのである。ここで、抽象化に失敗して元のシステムの性質をうまく保っていない遷移系を作ってしまっている可能性もあるが、これについては後述する。以後はシステムそのものについてではなく、専ら遷移系について議論することになる。さて、遷移系が期待する性質をもつかどうかを、モデル検査器を用いて検査する。モデル検査器がNOと答え反例を返す場合には、その反例に関して期待される性質が成り立っていないので、この反例を欠陥の候補とするのが妥当である。この場合には、反例を解析して遷移系の動きを実際のシステムに対応させることにより、(遷移系ではなく)システムの欠陥が生じているのかどうかを判断する。しかし、モデル検査器がYES(満足する)と答える場合には、それだけではシステムの欠陥が存在しない(つまり期待どおりに動く)とは言えない。モデル検査器に与える遷移系が現実のシステムの妥当な表現になっているかどうかは、必ずしも明らかではないからである。このように、モデル検査器は数学的モデルを対象とした検査を行うものである。実際の情報システムの検査にモデル検査器を用いるためには、システムと数学的モデルのずれを埋めるための工夫が必要である。例えば、モデル検査器がNOを返した場合でもすぐにシステムに欠陥があると結論することはできず、反例を解析すべきであるが、その解析には誰が当たるのか、という問題がある。検証 (欠陥検出)に携わるものばかりでなく、開発チームの者も参加して最終的に欠陥か否かを決めるのは開発チームの者にすべきである、というのがわれわれの一般的結論であるが、いずれにしろこの種の考察を加えるのがモデル検査のシステム検証への実用にかかる研究であり、フィールドワークを通じて行おうとしたのはこのような研究である。3 技術移転の野外科学的方法論本章では、川喜田二郎氏によるW型問題解決モデルと、産業技術総合研究所設立以来我々が議論してきた本格研究のモデルとを比較対照しながら、技術移転活動の体系化を試みる。3.1 川喜田氏によるW型問題解決モデル川喜田二郎氏は科学研究の活動を、書斎科学、実験科学、野外科学の三つに分けて考えた[1]。書斎科学は、先人により体系づけられた情報を机上での考察や推論などの演繹により発展させる活動であり、数学などを典型とする。実験科学は、再現可能な現象を実験室内で引き起こして観察する帰納の活動で、実験物理学が典型である。両者が所与の理論に基づいた活動なのに対し、野外科学はそれらとは別の活動で、再現不可能な現象を現場に出かけて観察して理論をたてる、発想(abduction)を主眼とする。地震の直後に社会的に生じる現象は、このような観察の対象の好例である。野外科学における観察の現場をフィールド(野外)と呼ぶ。フィールドは必ずしも屋外に存在する必要はなく、例えば、ソフトウエアの開発現場は情報学にとってのフィールドと考えられる。三つの活動の関係は図1図1 川喜田氏によるW型問題解決モデル(参考文献[2]より再構成)知識の収納庫野外観察実験観察経験レベル思考レベル探検検証実験準備発想と統合問題提起推論情勢判断HGEDCBAF

※このページを正しく表示するにはFlashPlayer9以上が必要です