タグ

形式手法に関するaoe-tkのブックマーク (6)

  • 自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(前編)

    自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(前編) ふだん何気なく使っている鉄道。改札を降りるときにICカードを自動改札にかざすと、「ピッ」という音と共に一瞬のうちに運賃を計算してくれます。けれど、複数の路線を乗り継いだり、途中で定期券区間が挟まっていたりと、想像しただけでもそこには膨大な組み合わせがあります。それでも運賃計算プログラムはわずか一瞬で正しい運賃計算が求められ、バグがあったら社会的な一大事にもつながりかねません。 爆発的な計算結果の組み合わせがあるはずの運賃計算プログラムは、どうやってデバッグされ、品質を維持しているのでしょうか? 9月12日から14日のあいだ、東洋大学 白山キャンパスで開催された日科学技術連盟主催の「ソフトウェア品質シンポジウム 2012」。オムロンソーシアルソリューションズ 幡

    自動改札機の運賃計算プログラムはいかにデバッグされているのか? 10の40乗という運賃パターンのテスト方法を開発者が解説(前編)
    aoe-tk
    aoe-tk 2012/09/24
    テストケースの絞り込み方法、別途計算ソフトウェアを作っての答えの突き合わせ、形式手法の試み...色々勉強になる。
  • ディペンダブル・システムのための形式手法の実践ポータル

    このサイトは、形式手法の普及促進を目的として、経済産業省「新世代情報セキュリティ研究開発事業」の成果やその後の関連動向等を掲載しています。

  • コマンドキューをもつシステムのAlloyモデル - masateruk’s blog

    とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。 問題 あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。 assign(v)   // オブジェクトの値をvに上書きします。 copy(obj)   // オブジェクトobjの値をコピーします。 getValue()  // オブジェクトの値を取得します。 このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。 assign(v)コマンドは、値の上書きする。 copy(obj)コマンドは、オブジェクトobjの値をコピー

    コマンドキューをもつシステムのAlloyモデル - masateruk’s blog
  • Alloy Community

    Welcome to the new Alloy community website! This site is intended as a way for Alloy users to connect and discuss the Alloy modeling language, as well as a place to post papers, software, events or courses related to Alloy. The Alloy Analyzer can be downloaded HERE! If you are a new user to Alloy, please browse the Tutorial and the main Alloy Analyzer web page. If you are a researcher or user of

  • 形式手法とモデリング - AlloyAnalyzerを中心に | Think IT(シンクイット)

    1. 初めに ソフトウエアの欠陥がもたらす影響がクリティカルになるにつれて、より間違いの少ない開発手法に注目が集まっています。 そんな中で注目されている技術の1つが、形式手法です。形式手法とは、数学をベースにしたシステム開発手法の総称です。 ですが、従来の形式手法は、数学の専門知識が必要だったほか、大がかりなシステム開発体制とあわせて語られることがほとんどでした。このため、一般の開発者にとっては、なじみのない技術でした。 こうした状況が、ここ数年で一変しました。PCの性能向上と、より使いやすいツールの提供により、誰でも簡単に試すことがのできる環境が整いつつあります。 記事では、形式手法ツールの1つ「Alloy Analyzer」を取り上げ、以下の2つのポイントを中心に解説します。 形式手法は、導入の難しさが解消されてきている 形式手法は、ほかの現行の開発手法を補うかたちで利用できる 1.

  • [Think IT] 【新・言語進化論】仕様記述言語を知っていますか?

    フェロー プリンシパルR&Dスペシャリスト 技術開発部 システム科学研究所 所長 1979年日電信電話公社入社、2002年NTTデータへ転籍、2007年4月NTTデータ 初代フェロー、技術開発部システム科学研究所所長に就任。ソフトウェア工学、要求工学、Webデータベース連携、ICカードプラットフォーム、ユビキタスコンピューティング等の研究開発に従事し、最近は知識創造デザイン技術やサービスイノベーションの研究にも取組んでいる。

  • 1