VDMを用いた仕様記述・検証 ～ モデリング編 ～
今回は「LEGO Mindstorms NXT」を題材に、要求の分析からVDMを前提としたモデリング、UMLの記述までの流れを詳しく解説する。 前回「VDMはソフトウェア開発でこう使う！ ～導入と運用のツボ～」では、VDM（Vienna Development Method）を開発現場に『導入』し、『運用』するためのさまざまな施策を紹介しました。 今回からは、それらの施策を使いながら、実際どのように要求をモデリングし、仕様を記述し、仕様を検証するのかをレゴ社のLEGO Mindstorms NXT（以下、Mindstorms）を題材にして見ていきます。まず、本稿では要求を分析したうえで、VDMを前提としてモデリングをし、そのモデルをUMLで記述するところまでを紹介します。 なお、ここからはUMLの状態遷移図やクラス図などが出てきます。これらの記法は基本的にUMLに準拠した形で記述しますが、
VDMはソフトウェア開発でこう使う！
“VDMを開発プロセスの中でどのように活用すべきか”について、「導入」と「運用」に分けて、具体的な施策を示しながら解説する。 前回、「VDM（Vienna Development Method）」は仕様記述において強力な道具であり、現場への導入がしやすい手法だと紹介しました。 では、この手法さえ導入すれば開発におけるすべての問題が解決するでしょうか？ 残念ながらその答えは「ノー」です。VDMは、何でも解決してしまうドラえもんのひみつ道具でもなければ、夢をかなえる魔法のランプでもありません。また、仕様の品質向上に効果があり、なおかつ現場への導入がしやすいとはいえ、実際に現場に取り入れるとなると抵抗や不安を感じるものです。前回の解説を読んだ方もきっとそのように感じているのではないでしょうか？ というわけで今回は「VDMをどのようにソフトウェア開発の現場で使ったらよいのか？」について紹介し、導入
ライトウェイトな形式手法で高品質な仕様をこの手に！
ライトウェイトな形式手法で高品質な仕様をこの手に！：誰でも使える形式手法（1）（1/3 ページ） 近年、組み込みソフトウェアは高機能・多機能化により複雑さを増し、開発規模が著しく増大しています。 こうした厳しい状況の中、ソフトウェア開発の現場では、以下のような問題に直面するケースが多く見られます。 出荷前に仕様の不具合が発見され、対応に追われた 修正をしたら思わぬ個所に不具合が発生した 外部に依頼したソフトウェアの品質がなかなか上がらない ソースコードしかなく、仕様書が残っていないため、どこを修正すればよいのか分からない 仕様をレビューすることの限界を感じる では、なぜこのような問題が起こるのでしょうか？ その原因の1つは“仕様の不確かさ”にあります。読者の皆さんの中にも、『仕様（の不確かさ）が原因で痛い目を見た』という経験をお持ちの方がたくさんいらっしゃるのではないでしょうか？ そこで本
dfltweb1.onamae.com – このドメインはお名前.comで取得されています。
このドメインは お名前.com から取得されました。 お名前.com は GMOインターネットグループ(株) が運営する国内シェアNo.1のドメイン登録サービスです。 ※表示価格は、全て税込です。 ※サービス品質維持のため、一時的に対象となる料金へ一定割合の「サービス維持調整費」を加算させていただきます。 ※1 「国内シェア」は、ICANN(インターネットのドメイン名などの資源を管理する非営利団体)の公表数値をもとに集計。gTLDが集計の対象。 日本のドメイン登録業者(レジストラ)（「ICANNがレジストラとして認定した企業」一覧（InterNIC提供）内に「Japan」の記載があるもの）を対象。 レジストラ「GMO Internet Group, Inc. d/b/a Onamae.com」のシェア値を集計。 2023年10月時点の調査。
「バグ無し」は可能、ソフトの先頭走る
ソフトウエア開発の先端技術を現場に広める伝道師。酒匂寛氏はこの呼び名にふさわしい。オブジェクト指向技術を日本にいち早く紹介し、多数の導入プロジェクトに参加。現在は「形式手法」の定着を目指す。オープン系の最初期から30年、あくまで現場にこだわり、「バグ無し」開発への理想を追い続ける。 オブジェクト指向、形式手法とソフト開発技術の最前線にいち早く取り組んできました。 自分の中では問題意識は一貫しています。ソフトを開発する上で、ソフトの論理的な振る舞いを表現した「仕様（スペック）」がいかに大切か、ということです。 仕様は、要求を出す人と物（プログラム）を作る人が合意する接点となります。ここがいい加減だと、どうにもならないわけですよ。オブジェクト指向も形式手法も、仕様を正しく作り、信頼性の高いソフトを実現する手段として注目しました。 ソフト開発では仕様書を書くのは当たり前ですが、それでは不十分であ
形式仕様記述Alloyを試してみる - きしだのHatena
試してみるよ。 とりあえず商品をまとめたセット商品についての仕様を書いてみる。 まず商品の定義 module exec/shohin sig Shohin{} pred show{ } run show sigはJavaとかのclassだと思えばだいたいOK。 なんか商品がみっつ出た。 じゃあ、セット商品を定義してみる。 sig SetShohin{ bundle: set Shohin } おー、同じ商品が３つのセットに含まれてしまった。Alloyさんイヤらしいとこついてくる。 ということで、ひとつの商品は多くてもひとつのセットにしか含まれない、っていう制約を加えます。 fact { all s: Shohin | lone bundle.s } 書き下ろすと「すべての商品について、商品をbundleとして持つのはたかだか１つ」になるんですけど、この、フィールドを左に書く書き方は通常のプ
『抽象によるソフトウェア設計』とAlloy、第一印象報告 - 檜山正幸のキマイラ飼育記 (はてなBlog)
『抽象によるソフトウェア設計 -- Alloyではじめる形式手法』の献本をいただきました*1。書店に並ぶ前、7月9日に届きました。訳者のみなさん、ありがとうございます。 抽象によるソフトウェア設計−Alloyではじめる形式手法− 作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫出版社/メーカー: オーム社発売日: 2011/07/15メディア: 単行本（ソフトカバー）購入: 8人 クリック: 274回この商品を含むブログ (35件) を見る 「序文」、「監訳者序文」、「訳者あとがき」、そして第1章「はじめに」あたりを読んで感心しておりました。第1章はわずか4ページですが、素晴らしい、実にいいことが書いてあります。それで僕はスッカリ満足して（残りは読まないままで ^^;）いました。 金曜日（7月15日）にid:bonotakさんに、「アンタ、いくらなんでも
「抽象によるソフトウェア設計」発売 - Yet Another Ranha
https://sites.google.com/site/softwareabstractionsja/ https://sites.google.com/site/softwareabstractionsja/about/toc ← 目次 本日7月15日金曜日、洋書「Software Abstractions」(http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928)の訳本である「抽象によるソフトウェア設計 Alloyではじめる形式手法」が発売されます。 実はレビュワーだったりしたので、発売当日になってしまいましたが、勝手に紹介するつもりです。 さて、本書はサブタイトルの通りでAlloyを使って何か色々しましょうという感じになっています。 いや、そもそも"Alloy"って何やねんという話なのですが、Alloy
形式手法 - PukiWiki
2011-04-01 日々のメモ2011 2011-03-31 RecentDeleted 2011-03-26 vtk 2011-03-24 StarLogo 2011-03-23 PAT 2011-01-10 vtk for Java 2011-01-05 FrontPage 日々のメモ 2010-12-17 日々のメモ2010 2010-12-10 ParaView 2010-12-08 Go言語 2010-12-06 vtk for Tcl 2010-11-25 AlloyAnalyzer Japanese 2010-11-23 doxygen 2010-11-22 GoQuickSort GoTurtleParallel GoTurtle 形式手法 fgram Coq 分類 † 形式手法、ってその言葉だけをとると、あまり情報がない。なぜって 通常、科学・工学の分野で研究をする、と
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
