形式手法はなぜ流行っていないのか - Qiita
はじめに みなさん形式手法をご存知でしょうか？ 名前くらいは聞いたことあるけどいまいち何かわからないという方が多いのではないでしょうか。 その通りです。形式手法はアカデミアではそれなりに研究されているものの、 一般の（特にWeb系）ソフトウェア開発者が携わることはなかなかないのではないかと思います。 この記事ではソフトウェア開発に形式手法が導入されないのはなぜなのかを考察します。 この記事ではアジャイルソフトウェア開発において形式手法を導入する際のハードルについて考察します。 追記 本記事について、「形式手法は流行っていない」というのは正確ではないのではないかという指摘をいただきました。組み込み系や社会インフラ系等バグを絶対に出せないシステム開発では形式手法がよく使われているそうです。 ちょっと古いデータですが活用事例です。 誤解を招く紹介となっていたことをお詫びします。 さらに追記 ku
ディペンダブル・システムのための形式手法の実践ポータル
このサイトは、形式手法の普及促進を目的として、経済産業省「新世代情報セキュリティ研究開発事業」の成果やその後の関連動向等を掲載しています。
形式手法書籍・リンク集
形式手法書籍・リンク集 これまで，形式手法・ツールに関する情報ソースは，研究論文や英語のWebサイト等一般の開発者には敷居の高いものでした．しかし近年日本での形式手法への関心の高まりを受けて，一般の開発者向けの書籍や，日本語による解説記事等も増えてきました．以下では形式手法・ツールに関する書籍，論文，Webサイトの情報をまとめていきます． 書籍・リンク集（形式手法全般） このページでは形式手法全般について解説している書籍，論文，Webサイトに関する情報をまとめています． 他にも多数ありますのでぜひ検索してみてください．なお，コメントは運営者の一意見ですので，それを踏まえた上で参考にして下さい． 著名な英語記事（古典的なもの） ● Seven Myths of Formal Methods Anthony Hall, IEEE Software, vol. 7, no. 5, pp. 11-
Google Sites: Sign-in
Not your computer? Use a private browsing window to sign in. Learn more about using Guest mode
「形式手法適用調査」報告書 : 情報処理推進機構：ソフトウェアエンジニアリング
形式手法は高信頼性を担保するための有効な技術です。1990年代後半から欧州では、形式手法を適用したシステム構築が進められました。一方、国内では、「扱える技術者が少ない」等の理由から、形式手法の適用は進んでいません。このような背景から、国内の開発現場への適用促進に向けた基礎資料作成のため、本調査を実施しました。 本報告書は、欧州を中心に海外調査を行い、形式手法を適用した海外のプロジェクト104件の中から12件の事例、および形式手法ツールベンダの調査結果等について、とりまとめました。 調査した事例は、下記の通りです。 ・防潮可動堤開閉意志決定システム／オランダ ・航空管制システム（iFACT）／イギリス ・無人地下鉄車両の制御（パリ地下鉄14号線）／フランス ・パリ地下鉄プラットフォームドアの制御／フランス ・シャルルドゴール空港の無人シャトル制御／フランス ・北京地下鉄の自動列車停止システム
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書: ホットコーナー
ブログ(iiyu.asablo.jpの検索) ホットコーナー内の検索 でもASAHIネット(asahi-net.or.jp)全体の検索です。 検索したい言葉のあとに、空白で区切ってki4s-nkmrを入れるといいかも。 例 中村(show) ki4s-nkmr ウェブ全体の検索 ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。 --- http://iiyu.asablo.jp/blog/2010/07/29/5254538 高品質高信頼ソフトウェア開発の特別セミナー http://iiyu.asablo.jp/blog/2010/07/29/5254545 VDM++によるオブジェクト指向システムの高品質設計と検証 で書いた続き。 フ
VDM++によるオブジェクト指向システムの高品質設計と検証 仕様の品質を飛躍的に高める手法 | SEshop.com
品質問題で余計な修正コストがかかっている原因の8割は「仕様」が曖昧 一般にユーザからの要求に対して正確な仕様書が作成されて、はじめてエンジニアが要求に合ったソフトウェア開発（システム設計）を構築することができます。しかし、実際にはちゃんと「仕様」が書かれず、エンジニアたちが不毛な開発作業を強いられているのが現状です。本書は、VDM言語の大御所である著者がVDM++によるオブジェクト指向システムの正しい設計の助けとなる補完的なモデル化技法の適用法を詳細に解説したものです。 基本的な利用プロセスや記述方式からVDM++の近年の拡張である並列性のモデル化やVDM++ ToolboxのJavaコード生成機能についても触れています。アーキテクチャから保守管理者まで、仕様記述の仕組みが手に取るようにわかる1冊です。 原題：Validated Designs for Object-Oriented Sy
Alloy Analyzer で形式仕様記述
仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、 Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。 それらのツールと Alloy との比較も、機会があればご紹介したいと思います。 2. Alloy を使った形式仕様記述の特徴 数理論理学＋集合論をベースとした Alloy の言語で仕様を記述します。 書いた仕様を、簡単に検査することができます。 難しい論理式の証明などは必要ありません。 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。 仕様で書いた振る舞いをシミュレーションすることができます。 3. このページのスコープ ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。 抽象度
Isabelle
What is Isabelle? Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle ov
CafeOBJ 入門
このディレクトリで提供しているドキュメントは、CafeOBJ の初学者への手引きである。主に自然数の仕様を例題として用い、仕様記述から証明までの流れを体験してもらうことを主眼に置いている。 このドキュメントは、次のように構成されている: CafeOBJ 処理系の使い方 CafeOBJ 処理系の起動と終了方法 仕様の記述法 仕様を CafeOBJ 処理系に読み込ませる CafeOBJ の基本的な文法などの仕様の記述法 コメント モジュール ソート 輸入 オペレータ 等式 変数 定義済みモジュールの表示 項の構文解析 項の簡約 証明譜を用いた証明法 証明譜とは 組み込み述語 = 結合律の証明 交換律の証明 補足 トラブル発生時 内蔵モジュール 識別子で日本語を使う 練習問題 改訂履歴 2008-02-06 「識別子に日本語を使う」を追加した。 2007-09-25 「証明譜とは」の証明ログのダ
www.vdmtools.jp – このドメインはお名前.comで取得されています。
このドメインは お名前.com から取得されました。 お名前.com は GMOインターネットグループ(株) が運営する国内シェアNo.1のドメイン登録サービスです。 ※表示価格は、全て税込です。 ※サービス品質維持のため、一時的に対象となる料金へ一定割合の「サービス維持調整費」を加算させていただきます。 ※1 「国内シェア」は、ICANN(インターネットのドメイン名などの資源を管理する非営利団体)の公表数値をもとに集計。gTLDが集計の対象。 日本のドメイン登録業者(レジストラ)（「ICANNがレジストラとして認定した企業」一覧（InterNIC提供）内に「Japan」の記載があるもの）を対象。 レジストラ「GMO Internet Group, Inc. d/b/a Onamae.com」のシェア値を集計。 2023年10月時点の調査。
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
形式手法入門 －ロジックによるソフトウェア設計－ | Ohmsha
Amazon.co.jp: 抽象によるソフトウェア設計−Alloyではじめる形式手法−: Daniel Jackson (著), 今井健男 (翻訳), 酒井政裕 (翻訳), 遠藤侑介 (翻訳), 片岡欣夫 (翻訳), 中島震 (監訳): 本
連載記事「誰でも使える形式手法」 － ＠IT MONOist