モデルチェッキングコンテスト（MoCCon）
トップエスイーでは、ソフトウェアエンジニアリングの技術・理論・ツールを使いこなすIT技術者を育成しており、さらに、エンジニアの自己研鑽を支援する活動を行っています。その一環として2017年3月に、国内の社会人・学生を対象とした、先端的なソフトウェアエンジニアリング技術を競う「トップエスイーコンテスト」を開催しました。以下の2つのコンテストをまとめてトップエスイーコンテストと呼んでいます。
- MoCCon：モデルチェッキングコンテスト（Model Checking Contest）
- BiPCon：ビッグデータプログラミングコンテスト（Big Data Programming Contest）
2つのコンテストはどちらもオンラインコンテストとなっており、コンテスト参加者はWebサイトを通じて課題の入手と解答の提出を行うことができました。
それぞれのコンテストで優勝と学生奨励賞の2つの賞を設け、2017年3月24日に国立情報学研究所で開催されたトップエスイーシンポジウムで、入賞者の表彰式が行われました（図3）。表彰式では文部科学省 研究振興局の榎本参事官（情報担当）より表彰状と副賞の贈呈が行われ、記念すべき第1回の副賞としてApple Watch Series 2が受賞者に贈られました。コンテストの結果は、トップエスイーコンテストのサイトに掲載されています。
モデルチェッキングコンテスト（MoCCon）は、企業の開発現場や研究所などの産業界における形式手法の普及と、モデル検査技術者の育成を目的としています。定められた期間内で、モデル検査を用いた検査業務を依頼してきた相手の要求を満たす成果を出し、得られた結果を簡潔にまとめて報告する能力を競うコンテストです。モデル検査を業務として行うことに重点を置いているため、表4のような具体的な状況を想定しています。課題はもちろん、想定した状況を加味したものを提示しました。
| 現場 | 企業や研究所などの組織で、 |
|---|---|
| 担当者 | 当該組織でのモデル検査担当者（競技者）が、 |
| 状況 | 検査業務として自社で開発中のシステムの検査の依頼を受けて、 |
| 作業 | モデル検査を用いてシステムの不具合の原因究明を行う。 |
| 成果物 | モデル検査報告書 |
コンテストの審査は、コンテスト参加者によって執筆された「モデル検査報告書」によって行われました。モデル検査報告書はモデル検査の依頼者に対して、検査の前提やモデル、検査式、検査結果などを報告するドキュメントです。モデル検査報告書には「検査の目的・方針・前提」「モデル・検査式の説明」「抽象化と絞り込み」「検査結果」を内容を盛り込みますが、作成したモデルと検査式、モデル検査ツールから出力された反例は付録として報告書に添付する形式としました。
コンテストで求められる能力と技術
モデルチェッキングコンテストでは、以下の能力と技術が求められます。
- システムの理解力
- モデリング技術
- 抽象化と絞り込みの技術
- 検査式の作成技術
- 反例の解析技術
- 報告能力
- ドキュメントの作成能力
最初に求められるのはシステムの理解力です。モデル検査は業務で用いられるため、第三者が製作したシステムの仕組みや振る舞いを理解する能力が必要です。システムを理解できたら、モデルチェッキングの名の通り、それをモデル化するモデリング技術が求められます。抽象化と絞り込みはモデル検査特有の技術です。状態爆発が発生しないように、時には大胆な手法を用いてモデルを極力小さくする必要があります。検査式の作成はモデル検査でとても重要な技術です。一般的に時相論理式をマスターするには少なからず学習が必要です。反例はシステムの振る舞いを理解できていれば、比較的容易に解析することができます。報告能力とドキュメントの作成能力については言うまでもないですが、モデル検査に限らずビジネスマンとして備えておくべき能力です。特にモデルチェッキングコンテストでは、審査対象がモデル検査報告書のみとなっているため、難しい報告内容を簡潔にまとめて、読みやすいドキュメントを作成することが入賞への近道となります。
トップエスイーでは「モデル検査事例演習」という講義で、最初にモデルを作成するところから、最後にモデル検査報告書を作成するところまでを、図4に示すモデル検査の適用プロセスにしたがって教えています。
審査のポイント
コンテスト参加者から提出していただいたモデル検査報告書は表5の観点から総合的に審査しました。
| 報告書本体 |
|---|
| モデル検査の知識がなくても理解できる内容か？ |
| 第三者に的確に説明できているか？ |
| 付録 |
| 全般：視認性／可読性の向上が図られているか？ |
| モデル：状態爆発を回避する工夫はされているか？ |
| 検査式：不具合の原因を解析するための式となっているか？ |
| 反例：不具合の原因が明確に示されているか？ |
審査では、不具合の原因究明に成功したことを前提条件として、モデル検査の知識がない依頼者に、検査の経緯と結果をどれだけ的確に報告書できているかを重点的に査読しました。
コンテスト参加者のうち約60%の方が、不具合の原因究明に成功されました。
