ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2013/04/10/6773298
ソフトウェア・テスト PRESS 総集編、Googleはどうやってテストしているか
に、もりたさんからコメントが。
--- ここから ---
こんにちは。
ずいぶんと遅くなってしまったのでもう見ていただけないかもしれませんが。

形式仕様記述言語については、「自動改札機の運賃計算プログラムはいかにデ
バッグされているのか？ 10の40乗という運賃パターンのテスト方法を開発者
が解説」という記事がとても参考になりました。

http://www.publickey1.jp/blog/12/_1040.html

私も、ご紹介いただいた荒木先生の「プログラム仕様記述論」で勉強を始めた
ところです。ただ私は脳出血による音声・言語機能障碍を持つ障碍者なので、
なかなか進みません（突如としてひらがなすら読めなくなるのです）。

それでも何とかへっぽこプログラマーとして生きています。
--- ここまで ---

　もりたさん、こんにちは。
>ずいぶんと遅くなってしまったのでもう見ていただけないかもしれませんが。
　とんでもない。全然、遅くないです。
　ご紹介いただいたリンク、めちゃくちゃ面白いですね。
　オムロンが自動改札機をどうやって開発・テストしているかという話。

http://www.publickey1.jp/blog/12/_1040.html
自動改札機の運賃計算プログラムはいかにデバッグされているのか？
10の40乗という運賃パターンのテスト方法を開発者が解説（前編）
2012年9月24日
http://www.publickey1.jp/blog/12/_1040_1.html
自動改札機の運賃計算プログラムはいかにデバッグされているのか？
10の40乗という運賃パターンのテスト方法を開発者が解説（中編）
2012年9月24日
http://www.publickey1.jp/blog/12/_1040_2.html
自動改札機の運賃計算プログラムはいかにデバッグされているのか？
10の40乗という運賃パターンのテスト方法を開発者が解説（後編）

　読むと、京王線の話がよく出ている。
　おっとろしい。オムロンも情報省のフロント企業や。＼(^O^)／

　九大(九州大学)の荒木先生、この事例、知ってるかな。
　とにかく、伝えておきます。

　有益な情報提供ありがとうございました。

http://www.amazon.co.jp/exec/obidos/ASIN/4274132633/showshotcorne-22/
プログラム仕様記述論 (IT Text) [単行本]
荒木 啓二郎 (著), 張 漢明 (著)

2013/05/08 追記：
　オムロンの事例、荒木先生に訊いたら、当たり前だけど、よくご存じだった。
　もっと教えてやるけん、中洲に来いだって。＼(^O^)／

関連：
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特別セミナー
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書
http://iiyu.asablo.jp/blog/2011/02/04/5662037
仕様記述言語Alloy, Software Abstractionsの翻訳がオーム社から出そう＼(^O^)／

　「Software Abstractions」の翻訳のこと、フォローしてなかった。
　2011年7月に、ちゃんと出てます。
http://www.amazon.co.jp/exec/obidos/ASIN/4274068587/showshotcorne-22/
抽象によるソフトウェア設計－Alloyではじめる形式手法－
[単行本（ソフトカバー）]
Daniel Jackson (著), 中島 震 (監訳), 今井 健男 (翻訳),
酒井 政裕 (翻訳),遠藤 侑介 (翻訳), 片岡 欣夫 (翻訳)

　オーム社にある紹介。
http://ssl.ohmsha.co.jp/cgi-bin/menu.cgi?ISBN=978-4-274-06858-4
抽象によるソフトウェア設計 ―Alloyではじめる形式手法

　もりたさんが障碍者ということで、その関連。
関連：
http://iiyu.asablo.jp/blog/2013/04/11/6774218
ITパラリンピック、スイッチHAL, ALS患者が太鼓の達人大会
http://iiyu.asablo.jp/blog/2013/01/21/6697651
バリバラ、障碍者の防災
http://iiyu.asablo.jp/blog/2013/03/10/6742517
バリバラ「東日本大震災から２年～被災地の障害者はいま」、「心をひとつに ～松田聖子＆ボブ・ジェームス～ 東北に歌う」
http://iiyu.asablo.jp/blog/2011/04/08/5782723
CBR 地域に根ざしたリハビリテーション、障害者の社会開発、ケアを問いなおす
http://iiyu.asablo.jp/blog/2012/12/29/6673818
人間のクズ。西播磨の県立高校生が障碍者に嫌がらせ、動画投稿
http://iiyu.asablo.jp/blog/2011/05/11/5856733
東日本大震災。聴覚障碍者はじめ、障碍者の苦境。
http://iiyu.asablo.jp/blog/2011/05/20/5871487
ETV特集：ネットワークでつくる放射能汚染地図、障害者、震災１か月の記録
http://iiyu.asablo.jp/blog/2011/09/14/6102829
東日本大震災６か月「取り残される障害者」
http://iiyu.asablo.jp/blog/2012/04/06/6402464
東日本大震災１年「この町で暮らしたい～障害者・地域福祉の復興へ～」、東日本大震災から一年 障害者が語る“この一年”