形式検証SPIN講習会に参加
兼ねてから興味があったSPINの講習会に参加した。WEBや書籍などで情報が存在するがやはり直接講習という形で理解できる方がいろいろとメリットがある。
これまでもシンポジウムやカンファレンスなので国内の講習やセミナーに参加するチャンスはあったが、うまくスケジュールが合わせられなかった。
今回の開催場所は横浜の開講記念館という場所で大変歴史的な趣を感じる。
講習およびその後の懇親会で参加者や講師の方といろいろ話をすることができ、価値ある講習会であった。
SPINは並行性などを形式検証できるので、組込み・リアルタイムシステムの開発者にはうってつけである。もっともSPINを効果的に用いて検証するにしても、オブジェクト指向開発やリアルタイムシステムの開発手法・プロセスの理解は欠かせない。
現在ソフトウエア業界もグローバル化の波でターニングポイントに来ているが、生産性・品質向上の抜本的な対策や戦略を考えないと「じり貧」である。
多くの開発現場が従来のやり方と変化が無いので、今のままでは大変なことになる。
SPINのような線形実相理論やスケジューリング理論のRMAおよびテストのATGに代表される理論的な開発・検証アプローチと自動化がキーであるが、それにはしっかりとしたソフトウエア工学の知識と実践が不可欠である。
=HSCI Takanari Hashimoto(URL:http://hsc-i.com/)=
| 固定リンク
「パソコン・インターネット」カテゴリの記事
- 6つのテーマを同時並行作業(2019.07.05)
- すっかりご無沙汰してしましました(2018.05.27)
- CCCC(C AND C++CODE COUNTER)GUIランチャーの公開(2017.04.13)
- 作成したYicesのGUIからオプションを変えSMTを行う(2017.01.19)
- 『Yices』によるSMTソルバ(2017.01.18)
この記事へのコメントは終了しました。
コメント
参加しましたSPIN講習会は半日でしたので、実質3時間です。Promelaのシンタックスや検証モデルについての概要でした。
検証する対象を抽象化したモデルや論理式およびPromelaでの記述の習得はハンズオントレーニングが向いていますので、事情が許せば不定期ですが北陸先端大学の青木先生が講師をしているセミナーが良いと思います(都内で実施)。3日コースですが価格も低価格で実施されています。
ブログでは、今後SPINを含めて有益なセミナーやカンファレンスなどを紹介していきたいと思います。
投稿: | 2008年12月24日 (水) 18時08分
SPINの本を自習しました。
簡単な模型は作れるようになりました。
LTL式をどう書くとよいかが、うまく思いつきません。
受講されたセミナでは、LTL式の作り方はどのような内容だったのでしょうか。
投稿: kaizen | 2008年12月22日 (月) 10時47分