ソフトウェア科学領域【青木研究室】
■正しいソフトウェア
私達が日常生活をしている今日の社会には，さまざまなところにソフトウェアが使われています。ソフトウェアはパソコンで動作させるものだけでなく，携帯電話，電化製品，自動車，飛行機などにも組み込まれていて，身の回りの製品，日々の生活に係わっているのです。そのため，ソフトウェアの誤りは日常生活や経済活動を混乱させ，莫大な時間的，金銭的損失を引き起こす可能性があり，実際，そのような事例が報告されてきています。そこで，誤りの無い，正しいソフトウェアを開発する方法を研究することが，今後の社会の発展，および，安心した生活をおくるためには重要です。正しいソフトウェアを実現する１つのアプローチは，ソフトウェア開発において形式的手法（Formal
Methods）を用いることです。
■形式的手法（Formal Methods）
形式的手法では，数学を基礎とした言語やツールを用いて，対象となるソフトウェアを記述し，検証します。これにより，なんとなくソフトウェアを開発するのではなく，数学に基づいた解析や正しさの保証を行うことができます。また，このような手法を用いて，ソフトウェア自身を科学することも重要です。ソフトウェアがこれからの社会や世界の構成要素であり続けるのであれば，他の自然科学の学問分野と同様，その本質や原理を明らかにして，事実を積み上げ，共有し，発展させる必要があります。そこで，私の研究室では，形式的手法を用いて正しいソフトウェアを開発する手法，および，ソフトウェアの原理に関する研究を行っています。
■ソフトウェアの検証
ソフトウェアの正しさを保証するために，厳密に記述して正しいことを証明する方法が考えられます。この方法のことを検証（Verification）と呼びます。現在，ソフトウェア検証のための有望な技法として，モデル検査技法と定理証明技法があります。そこで，これらの技法をソフトウェア開発にどのように応用するかについて研究を行っています。主に，オブジェクト指向分析・設計法，組み込みソフトウェアを対象としています。また，提案した手法を支援するソフトウェア開発環境も作成しています。
■ソフトウェアの原理
プログラム意味論やプロセス代数といったソフトウェアに関連する基礎理論が古くから研究され続けており，成熟しつつあると考えています。このような基礎理論を用いて，現在のソフトウェアの原理を明らかにすることは，今後のソフトウェアの健全な発展のために重要です。そこで，現在，なんとなくソフトウェア開発で用いている記法や概念を，プログラム意味論などの枠組を用いて形式化して，その原理を明らかする研究を行っています。
作成したソフトウェア開発環境
■代表的な著書・論文
- 定理証明技術のオブジェクト指向分析への適用，日本ソフトウェア科学会学会誌コンピュータソフトウェア，Vol.18No.4,
pp.18-47, 2001
- RTOSに基づいたソフトウェアのためのモデル検査ライブラリ，組込みソフトウェアシンポジウム, pp.56-63,
2005
- An Axiomatic Formalization of UML Models, Practical UML-Based Rigorous
Development Methods, pp.13-28, 2001
- Formalization and Analysis of Dataflow in Object-Oriented Design Models,
International Symposium on Object-Oriented Real-Time Distributed
Computing , pp.95-105, 2005
