言語設計学講座観測に基づく振舞のモデル化と検証客員研究員：緒方和博何のため？コンピュータが生活のあらゆる局面にはいり込んでくる２１世紀の高度情報化社会においては，高い信頼性を持って適切な品質のサービスを提供するシステム（ソフトウェアやハードウェア）を，高いコストをかけてでも開発および維持しなければならない情況がますます増えてくると思われる．このような高品質のシステムを開発するには，開発の上流工程においてなるべく多くの不具合を取り除く必要がある．どのように？ 1.開発したいシステム（ソフトウェアやハードウェア）がどのように振る舞うのかを思考実験(観測)する．言い換えると，実行にともないシステムを特徴づける値がどのように変化するのかを考える． 2. 観測により得られる情報をもとにシステムの振舞の模型（モデル）を作る．この研究では OTS（観測遷移機械）という数学モデルを使ってシステムのモデルを作る． 3. モデルを計算機言語で記述する．この研究では CafeOBJ という計算機言語を使う；等式を用いてモデルを記述する． 4. コンピュータを使って記述したモデルの実験（検証）を行う．この研究では CafeOBJ 処理系を用いて実験を行う．何ができるの？ A. 電子商取引プロトコル iKP の不具合の発見と修正：IBM で設計された iKP プロトコルが重要と思われる性質を有していないことを発見，修正案を提案，そして修正案がその性質を有することを確認した．重要と思われる性質とは，「銀行が支払いを許可した場合，その支払いにかかわる買い手と売り手はともにその支払いに同意している」というものである． B. セキュリティプロトコル TLS（SSL）の正しさの確認：ウェブブラウザ（Netscape や Internet Explorer など）で標準的に使われている TLS (SSL) プロトコルが望ましい性質を有していることを確認した． C. Suzuki-Kasami 分散相互排除アルゴリズムを正しく使うための条件の発見：アルゴリズムを提案している論文では明記されていない条件を発見した． D. 実時間（realtime）および複合（hybrid）システムのモデル化と検証：Fischer プロトコル（実時間相互排除プロトコル），鉄道の踏み切り問題（実時間システム），温度安定器（複合システム）が望ましい性質を有していることを確認した．