形式的手法と企業 [終了]

Question

それで...

私はソフトウェアエンジニアリングの形式的手法を教えています。「アジャイル方法論」も教えています。ほとんどの人はこれは矛盾していると考えているようです。それはとても理にかなっていると思います...私は実際に物事を成し遂げる必要がある会社でも働いています:) 私は獲得したスキルポイントを日々の「仕様」に適用できますが、私の同僚は通常、「形式的」という言葉から逃げます。

私は以前、これはプログラムの学習方法の本質的な方法によるものだと考えていました。私たちは通常、問題を理解することではなく、有効な解決策を見つけることに駆り立てられます。それから私は、これは公式コミュニティのほとんどの人がエンジニアではなく、数学者またはコンピューター科学者であるという事実によるものだと考えました。最近では、形式メソッドのコミュニティが何らかの「難読化」法の背後に隠れて、利用可能なすべての UNICODE シンボルを使用し、無作法で見た目に悪いツールを積極的に開発し、標準を前にして嘲笑しているだけなのだろうか、と私は疑問に思っています。

はい、私は「彼らを責める」視点から「私たちを責める」視点に移行してきました ;-)

そこで、私の質問は次のとおりです。あなたの会社では何らかの正式な手法を使用していますか?それらを導入しましたか、それとも前提条件でしたか?数学の霧を人々の恐怖から取り除き、形式的な手法を使用するように仕向けるには、どのようなテクニックを使用しますか?より一般的な使用法において、現在のツールに欠けているものは何だと思いますか?

Answer 1

人々に任意の方法または方法論を購入させる鍵は、彼らが抱えている問題をどのように解決するかを示すことです。彼らがそれを見ることができれば、彼らの生活が良くなるので、あなたは彼らにテクニックを採用させる機会をはるかに改善します。

そして、それらをできないなら、おそらく実用性よりも哲学に基づいた方法を採用したかったでしょう。他の人があなたの哲学を共有しない限り、あなたはどこにも行かないでしょう。おそらくすべきではありません。

数十年にわたって、非常に多くの方法論がありました。新しいものは常に古いものの欠点に対処しますが、プロジェクトは依然としてトラブルに陥り失敗します。どうして？新しい方法論を思いついたロックスターはロックスターであり、根本的な問題とその適用方法を理解しているからこそ、新しい方法論を作ったからです。後に来る人は盲目的にレシピに従う傾向があり、うまく機能しません。

だからこそ、根本的な問題について教え、さまざまな方法がそれらの問題にどのように対処しようとするかを示すことが最善だと思います。企業、プロジェクト、およびチームの違いは非常に大きいため、すべての組み合わせに1つの方法論をうまく適用することはできません。適切なツールを選択して適切に適用することを学ぶことは非常に重要です。

Answer 2

すべての貢献に感謝します。彼らは非常に洞察力に優れています。少し話させてください (個人的なことだと思わないでください :-)

ほとんどの人は、形式的メソッドとは単にプログラムの検証に関するものだと考えているようです。または重要なシステム。究極の決まり文句を追求すると、これは真実かもしれません。プログラムが正しく実行されていることを証明するためです（v.s.寄稿者が言ったように、正しいプログラムを実行しているかどうかを尋ねる検証です)。

ただし、Alloy などのモデル検索/チェック ツールを検討してください。UML と OO に慣れている人にとって、このようなツールの使い方を学ぶのにかかる時間はごくわずかです。それでも、モデルに関する洞察を即座に得ることができます。使用しようとしているモデルの十分に小さなサブセットから反例を見つけるのに、通常は 10 分もかかりません (そして、最初に Alloy でモデルを記述することも含まれます)。

要件エンジニアリングを例に挙げます。通常、大量の UML を描画します。ただし、OCL を使用する人はほとんどおらず、多くのビジネス ルールには自然言語で非公式に注釈が付けられています。なぜ？時間の制約はありますか？

ここで、大多数がモデルが満足できるものであることを証明するために直感だけを利用しているという事実を考えてみましょう。繰り返しますが、なぜですか？そのモデルを Alloy で作成するのと同じ時間 (描画の美しさを気にする必要がないので、おそらくさらに短い時間) をかけて、満足度をチェックするだけで済みますか?そして、今私はどのような数学をする必要があるのでしょうか?「述語」？IF とブール値の派手な名前 ;-) 量指定子?ForEachs() の派手な名前...

巨大情報システムはどうなるでしょうか？彼らは批判的である必要はありません...600 を超えるクラスを含む概念図 (実装ではありません!) を頭の中で分析してみてください。何らかの制約を見逃したり、モデルが愚かな出来事を許してしまったりするため、モデルで犯しやすい間違いで壁に頭をぶつけている人を多く見かけます。

実際のところ、頭から尻尾まで正式なアプローチを使用する必要はありません。確かに、アプリケーション全体を Coq で証明し、それが何らかの仕様に 100% 準拠していることを証明することはできます。これはコンピュータ科学者/数学者のアプローチかもしれません。

それでも、GTD の哲学があるのに、コンピューターにいくつかのタスクを委任して、開発の改善に役立てることができないのはなぜでしょうか?それは本当に「時間」の問題なのでしょうか、それとも単純に技術的能力や学習/革新する意欲の欠如なのでしょうか?

Answer 3

企業の基幹業務IT開発と連携するということは、ビジネスに関する知識を実際のビジネスマンから開発者の頭に移さなければならないことを意味します。私自身、抽象的な数学は最も楽しいものの1つであると感じていますが、それはひどいコミュニケーションツールです。そして、コミュニケーションがそれのすべてです。 IT担当者がより抽象的な表記法を採用するように説得するのに成功したかもしれませんが、基本的にはビジネス担当者にはチャンスがありません。

企業での正式な方法の役割を見ることができる領域がいくつかありますが（数学およびロジックが重い専門ソフトウェア、安全性が重要なソフトウェアのような証明可能なプロパティの重要な必要性）、それらは正しい要件を得るのにほとんど役立ちません例えば可能性のある外部または内部プロバイダーのセットに1つ以上の供給注文を発行することにより、顧客の注文を履行する方法。

ju審員はまだモデルベースのアプローチとドメイン固有の言語に取り組んでいると思います。 ITからビジネス側の要望やニーズに対してより迅速なフィードバックを提供するかどうか、ビジネスマンが重要な学習を行う必要があると推測するかどうかによって、成功または失敗すると思います。

テクノロジーは簡単です。コミュニケーションは大変です。正式な方法は正しいことをするのに役立つかもしれませんが、私が見たものは正しいことをするのに何もしません。 （はい、これらは決まり文句ですが、それは避けられないほど痛いほど真実だからです。）

Answer 4

「仕様と検証」のコースを受講しています。コース構造の一部として、次のことを行っています。 1. PVS（プロトタイプ検証システム） http://pvs.csl.sri.com/およびSMV（ソフトウェアモデリングおよび検証） http：//www.cs.cmu .edu /〜modelcheck / smv.html 2.それとは別に、ソフトウェア障害のために発生した事故を分析します。たとえば-アリアンVの失敗

フォーマルな方法は、故障コストが設計コストよりも大きいシナリオにより適していると感じています。そして、重要なシステムで使用されているソフトウェアにそれらを使用する傾向があります。航空電子工学、チップ設計などで使用されていると思いますし、現在の自動車産業でもそれを実践しています。

Answer 5

私は人々に正式な仕様方法を数回（ZおよびAlloy）受け入れさせようとしましたが、あなたが持っているのと同じ経験をしました：ほとんどの人々は、彼らが有用な目的を果たすと感じながら、それらを使用することは非常に不快です実際の作業。

おもしろいことに、同じ人々は、まったく役に立たないUMLダイアグラムを大量に大量に作成することに満足しています。

これには主に2つの理由があると思います：

a。）多くの開発者は、正式なアプローチで必要とされる抽象化のレベルに不快を感じています。ほとんどの入門レベルの数学教育はすべて微積分であり、非離散数学はこれで何かをする必要があるかもしれません。

b。）フォーマルな方法では、コアモデルをゼロから設計して気密性を確保し、その上にインターフェイスを提供して実際のユーザー要件に接続する、非常にボトムアップな設計アプローチが必要です。要件が開発努力を後押しする傾向があるため、トップダウンのアプローチはより自然に感じますが、それはしばしば一貫性のないモデルにつながります。すでに建てられた後、あなたの家の下に地下室を改装するようなものです。

Answer 6

正式な方法は、障害のコストが低いシステムでは意味がありません。

実稼働Webアプリケーションには、複数のフロントエンドボックス、複数のバックエンドボックス、複数のデータベースボックスがあります。いずれかのプログラムが失敗した場合、それはイベントではありません。ハードウェアは非常に安価であるため、すべてのソフトウェアを正式に指定するよりもはるかに少ないコストでこれらのシステムを構築できます。