南山大学 理工学部・理工学研究科・理工学研究センター

機械システム工学科 教員・研究室:張漢明

chang.png

張 漢明 准教授

〔専門分野〕

ソフトウェア工学

〔研究テーマ〕

形式手法に基づくソフトウェア開発技術支援

〔研究室web〕

理論に基づいた系統的なソフトウェア開発手法を研究する

ソフトウェアの「仕様」

chang_lab_01.png

ソフトウェア開発は「目に見えない人間の思考を目に見える形で実現すること」と捉えることができ、顧客も含めた開発に関わる人達で、最終成果物(製品)に対する「認識を共有する」ことが最も大切です。そのために、ソフトウェアで実現する製品を文書で表現した、作る内容をまとめた「仕様」が必要となります。

仕様を決める打ち合わせで顧客に「あーして欲しい」「こーして欲しい」など曖昧な表現をされては、顧客と開発者の間で製品に対する認識に誤解が生じます。例えば、ラーメンをつくることを依頼されたとしましょう。豚骨、醤油といった「スープの種類」、縮れ麺、細麺などの「麺の種類」、チャーシュー、メンマといった「具材」などが「仕様」になります。もし,お客さんが「なんか美味しいやつ」と言われては何を作って良いか分かりませんし、「麺は太麺」などと「想定外」の要望が来る場合もあります。仕様を表現するためには、曖昧さのない適切な言語が求められます。

「形式仕様言語」によるソフトウェア開発技術

chang_lab_02.png

まず思いつくのは「数学言語」です。現実世界を表現・思考するために人間が創作した英智の結集であり、全てのエンジニアリング技術の基盤となっています。この数学に基づいて意味づけされた人工言語が「形式言語」と呼ばれるもので、実は「プログラミング言語は形式言語」とみなすことができます。

この形式言語(プログラミング言語)で作成されたソフトウェアが「仕様」通りに正しく動作するか調べることが重要なのですが、調査項目(誤入力、入力ミス、...)は膨大で、人の手でチェックすることには限界があります。そこで「ソフトウェアの仕様を記述する」ことに特化した言語が必要とされるようになって来ました。これを「形式仕様言語」と呼び、形式仕様言語に基づいて表現された仕様は「形式仕様」は呼ばれます。

ソフトウェア開発技術は、エンジニアリングとしてまだ未成熟の分野です。個人ベースで有する優れた技術を理論として昇華して、形式仕様を中心とした様々なソフトウェア開発技術を開発することが私の研究テーマです。

「組み込みソフトウェア開発」における理論の実践

chang_lab_03.png

家電や自動車といった機器はコンピュータによって制御されていますが、このコンピュータを「組込みシステム」と呼びます。この組込みシステムに入っているソフトウェアは特に「組み込みソフトウェア」と呼ばれており、「組み込みソフトウェア開発の実践」を通して、形式仕様の理論に基づいたソフトウェア開発技術の統合を目指しています。

組み込みソフトウェアは「複数」の装置を制御するので、「並行の概念」が必要となります。並行システムは、単一プロセスのシステムに比べて複雑であり、「デッドロック」などの並行システム特有の概念を考慮する必要があります。2つのプロセス(プログラム)のデッドロックの例えとして、A君とB君がおもちゃを交換することを考えます。互いに「相手がおもちゃを手放したら」その後に自分のおもちゃを手放すことを考えている(プログラムされている)場合、どちらも相手が手放すことをいつまでの待つ状態(ロック)になることが分かります。

他にも、並行システムは考慮すべき状態や実行パスが膨大なので、様々な問題を上手く統治するために、機能と抽象具象により分割することが重要です。このような関係を解明して、これらの間の整合性を保つための理論を構築し、計算機を用いた整合性を検証するための支援技術に関する研究を行っています。

主な研究業績

  • 荒木啓二郎、張漢明:『プログラム仕様記述論(IT Text シリーズ)』(情報処理学会編、オーム社、2002)

ページトップへ