実践! ソフトウェアモデル検査 HOME | お問い合わせ | サイトマップ | リンク
研究会のご紹介 オンラインサービス 支援ソフトウェア 実用化の研究
過去のトピックス
2009/11/12
第6回ディペンダブルシステムシンポジウム(DSS2009)で発表を行います
2009/07/16
SWEST11でポスター・デモ発表を行います
2009/07/16
JaSST'09 in 関西に協賛します
2009/06/15
ETWest2009で研究発表(テクニカルセッション)開催
2009/06/15
モデル検査支援ソフトウェアのサンプル(踏切)を追加しました
2008/10/27
第五回 システム検証の科学技術シンポジウムで発表します。
2008/10/27
SWEST10での発表用スライドを公開しました。
2008/07/07
SWEST10で技術セミナー(モデル検査セッション)とポスター・デモ発表を行います。
2008/06/24
ETWest2008で技術セミナー(テクニカルセッション)開催。
2008/02/21
JaSST'08 in 東京で研究発表しました。
2008/01/09
JaSST'08 in 東京で研究発表します。
2007/11/22
第四回 システム検証の科学技術シンポジウムで研究発表しました。
2007/11/22
ESS2007で研究発表しました。
2007/09/28
Q&Aを追加しました。
2007/09/28
SWEST9で支援ソフトウェアを紹介。
2007/07/25
JaSST’07関西でチュートリアルを開催しました。
2007/07/25
<バグ修正>モデル検査支援ソフトウェアの変数設定画面で、変数値にマイナスの値が設定できない不具合を改修しました。
2007/06/18
モデル検査支援ソフトウェアの動作実績について。
2007/06/18
JaSST’07関西が開催されます。当研究会もチュートリアルを行います。
2007/06/18
ETWest2007で技術セミナー(テクニカルセッション)開催。
2007/04/03
ダウンロードページの公開。
2007/02/14
JaSST'07 in 東京で研究発表しました。
2007/01/24
モデル検査Webページのリニューアル。
2006/12/20
Q&Aページを追加。
2006/12/15
JaSST'07 in 東京で研究発表します。
2006/11/02
モデル検査支援ソフトウェア(試供版)の公開に向けて作業中。
2006/09/27
第三回 システム検証の科学技術シンポジウムで研究発表します。
2006/04/14
「情報システムの信頼性向上に関するガイドライン(案)」に形式手法の活用が載りました。
2006/04/06
JaSST'06 in 大阪 で講演を行います
2006/03/10
社内で教えてみました2。
上流工程(仕様作成)での活用を目指して、日頃、ソフトウェアを組まない人を対象にモデル検査の社内教育を3日間(3/1 - 3/3)行ないました。講師からは、「プログラマーの場合、モデル検査言語とC言語の文法が混乱して理解しにくい場合があるが、今回は、その問題がなくスムーズに進んだ」との感想が、受講者からは「面白い技術なので、最後は自分で使いこなして評価したい」との感想が得られました。
2006/01/26
雑誌に掲載されました。
我々のモデル検査での取り組み内容が日経エレクロトニクス誌に掲載(P103 - 105)されました。
2006/01/26
設計者との協力関係。
モデル検査専任者が対象システムのソフトウェア仕様の理解が浅いとモデルの作成や反例の解析などに時間が掛かります。また、仕様の読み違えから間違ったモデルを作成してしまうかもしれません。
ソフトウェアの開発者とモデル検査専任者が協力することによって上記の問題を解決することができます。短時間にモデル検査を実施することも可能になります。
2006/01/26
社内で教えてみました。
システム開発の実作業に従事する技術者を対象にして、モデル検査の社内教育をおこないました。
教育期間は2日間と短めでしたが、参加者からは「自分の仕事に取込んでいきたい」、「多くの社員に広めていきたい」、「もっと詳しい内容が知りたい」との感想を得ることができました。
2006/01/26
フロー図からモデルが作れる。
これまで、モデル検査用言語を使ってモデルをプログラム記述していましたが、モデルが大きくなると、そのプログラム記述に作業時間が取られます。また、複雑な場合ほど、モデル作成に先立って、フロー図を作成している場合が多くありました。そこで、フロー図からSMVコードを生成するモデル検査支援ソフトウェアを開発しました。
2006/01/26
デバッグで使える。
これまで、上流工程での設計検証手段として考えられていたモデル検査ですが、なんと、デバッグに適用して、大きな効果があることがわかってきました。 不具合事象がわかっているので、モデル化作業が短時間で済み、網羅的探索でバグを発見します。従来、長時間を要した再現性の低い不具合に対して最短時間で対策が打てます。
組込みシステム産業振興機構
関西産学官連携センター 組込みシステム技術連携研究体
先進的組込みソフト産学官連携プログラム 組込み適塾
サイエンスによる知的ものづくり教育プログラム トップエスイー
形式手法実践ポータル Formal Methods User Group
Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.