＜キッチリとは何か＞
現状はエンジニアリング以前
解釈ミスを減らす方法論へ
　「テストやレビューをしっかりやれ」「プロジェクト・マネジメントをキッチリ徹底しろ」 今のソフトウエア開発では，誰もが品質確保の確かさを「キッチリ」としか表現できない面がある。 エンジニアリングの実践に程遠いこうした現状から脱却しハードウエアと同じ地位を持つ工業製品として ソフトウエア開発を昇華させる必要がある。そのための道具として「形式的手法」を知り，見直すべき時が来た。

＜10分で分かる形式的手法＞

＜ケース・スタディー編＞
国内でも成功事例が出現
形式的手法の壁は高くない
　形式的手法の発祥の地，欧州では「同手法についてよくある誤解」とのテーマが学会などで語られる。 一方，日本ではその存在すらほとんど認知されておらずよくある誤解などが発生する以前の状態だ。 こうした中，国内でも先駆的に形式的手法を活用し成果を上げた企業がある。研究者の興味の対象でしかなかった形式的手法が，いよいよ日本でも現場に広がり始めた。仕様記述と形式検証（モデル検査）。 形式的手法を構成するぞれぞれの分野での最新事例を紹介する。

＜形式検証編＞
バグをしらみつぶしに探索
仕様精査やテストの手段に
　形式的手法の一種であるモデル検査（model checking）が流行の兆しを見せている。アルゴリズムの改良やコンピュータの高速化が後押ししLSI設計分野だけでなくソフトウエア分野においても実用段階に入りつつあるのだ。上流工程で仕様のバグを機械的に検出するモデル検査技術を人手に頼ることの多いテストやシミュレーションと組み合わせることでより多様な観点からバグをつぶせるようになる。現場のソフトウエア技術者が使いこなせる技術に成長してきた。

＜仕様記述編＞
実装者を迷わせない
詳細は形式記述言語で
　ソフトウエアの仕様は現在，多くが自然言語で書かれている。形式も人によってバラバラだ。自然言語の持つあいまいさや仕様記述の方法論の不在が仕様の解釈ミスを助長し，ソフトウエア開発の手戻りを招いてきた。 仕様を記述するには「形式的な仕様記述言語」という専用のツールがある。日本ではほとんど認知されていないが開発の上流工程の重要性が叫ばれる今は，形式的な仕様記述の使い時だ。