logo标签列表

形式化方法与企业

formal-methods
11

所以...

我教授软件工程中的形式化方法。我还教授“敏捷方法”。大多数人似乎认为这是矛盾的。我认为这很有道理...我还在一家公司工作，在那里我们需要实际完成任务 :) 虽然我可以在日常工作中应用我的“规范”技能，但我的同事们通常会逃避“正式”这个词。

我曾经认为这是因为我们学习编程的内在方式：我们通常被驱使着寻找一个可行的解决方案，而不是去理解问题的本质。然后我认为这是因为形式化社区的大多数人不是工程师，而是数学家或计算机科学家。现在，我想知道是否仅仅因为形式方法社区隐藏在某种“混淆”法则背后来使用所有可用的 UNICODE 符号，积极开发粗鲁、不美观的工具，并嘲笑标准。

是的，我已经从“指责他们”转向了“指责我们”的观点 ;-)

那么，我的问题是：你的公司是否使用任何形式化方法？您是否引入它们，或者它们是先决条件？您用什么技术消除数学的迷雾，激励人们使用形式化方法？您认为当前工具缺乏更广泛使用的什么？

6个回答
6
让人们接受任何方法或方法论的关键是向他们展示它如何解决他们所遇到的问题。如果他们能看到这会让他们的生活变得更好，那么你就有更大的机会让他们采用这些技术。
如果你无法向他们展示这一点，也许你想要采用这些方法是基于哲学而不是实用性。除非其他人分享你的哲学观点，否则你不会走得很远。也许你不应该这样做。
几十年来出现了许多方法论。新的方法总是解决旧方法的缺陷，但项目仍然会陷入麻烦和失败。为什么？因为制定新方法论的人是明星，他们之所以制定新方法论，恰恰是因为他们理解潜在的问题及如何应用它们。后来者往往盲目地跟随配方，结果效果不佳。
因此，我认为最好的方法是教授相关的基础问题，然后展示各种方法如何尝试解决这些问题。公司、项目和团队之间的差异如此之大，以至于没有一种方法论可以成功地适用于所有组合。学习选择适当的工具并善加运用是至关重要的。
3
感谢您的所有贡献，它们非常有见地。请允许我稍微批评一下（不要把它当个人攻击，虽然:-)）
大多数人似乎认为形式化方法只是关于程序验证或关键系统的。如果我们追求终极陈词滥调：证明我们正在正确地编写程序（与验证相反，验证询问我们是否正在编写正确的程序），那么这可能是正确的。
但是考虑模型查找/检查工具，例如Alloy。学习使用这样的工具对于习惯于UML和OO的任何人来说都需要极少量的时间。尽管如此，它可以立即为您的模型提供洞察力。通常，仅需不到10分钟即可在模型的足够小的子集上找到反例（这包括首先在Alloy中描述模型）。
以需求工程为例。人们通常会画很多UML。尽管如此，很少有人使用OCL，并且许多业务规则以自然语言进行非正式注释。为什么？时间限制？
现在考虑到大多数人只是凭直觉证明模型是可满足的。再次问：为什么？我可以花同样的时间（可能甚至更少，因为我不需要关心绘画美学）在Alloy中编写该模型，并且只需检查可满足性？现在我需要什么样的数学知识？“谓词”？IF和布尔运算的花哨名称;-)量词？ForEach（）的花哨名称...
大型信息系统呢？它们不需要是关键的...只需尝试在头脑中分析具有超过600个类的概念（而不是实现！）图。我看到很多人因为错过了某些约束条件或模型允许发生愚蠢的事情而犯易错的模型错误。
事实是，人们不需要从头到尾使用形式化方法。诚然，我可以在Coq中证明整个应用程序，并证明它与某些规范完全一致。这可能是计算机科学家/数学家的方法。
尽管如此，按照GTD的理念，为什么我不能将某些任务委托给计算机并允许它帮助改进我的开发？这真的是一个“时间”的问题，还是纯粹缺乏技术能力和学习/创新的意愿？
2
在企业中与业务IT开发一起工作意味着需要将实际业务人员的知识传递给开发人员。虽然我自己认为抽象数学是最伟大的消遣之一，但它是一个糟糕的沟通工具。而且沟通才是关键。虽然我可能会成功地说服IT人员接受更抽象的符号，但我基本上没有机会说服业务人员。
虽然我可以看到在企业中某些领域形式化方法的作用（数学和逻辑重的专业软件，像安全关键软件那样需要可证明属性），但它们对于正确地满足客户订单需求等方面提供的帮助很小。
我认为基于模型的方法和领域特定语言仍有待验证。我认为它们的成功或失败取决于它们是否能够提供更快的反馈，以满足业务需求，以及它们是否假定业务人员必须进行任何重要的学习。
技术很容易，沟通很难。形式化方法可能帮助我们做好事情，但我见过的这些方法都没有帮助我们做正确的事情。（是的，这些都是陈词滥调，但这是因为它们不可避免地且痛苦地是真的。）
1

我正在学习“规范和验证”课程。作为课程结构的一部分，我们正在进行以下工作- 1. 学习像PVS（原型验证系统）http://pvs.csl.sri.com/和SMV（软件建模和验证）http://www.cs.cmu.edu/~modelcheck/smv.html这样的工具 2. 除此之外，我们还会剖析由于软件故障而发生的事故。例如- 阿丽亚娜5号的失误

我认为正式方法更适用于故障成本高于设计成本的情况。它似乎适用于在关键系统中使用的软件，如航空电子、芯片设计等。目前的汽车行业也正在将其纳入实践。

大多数工具缺乏的是：
  1. 它们不是非常直观。缺乏易于使用的集成开发环境会加剧这种情况。
  2. 需要一些函数式编程知识。我在使用 PVS 时感到如此，因为它基于 LISP，一旦我开始学习 Scheme，它就开始有些意义了。
 - Arnkrishn
1

我曾经几次尝试让人们接受正式的规范方法（Z和Alloy），并且有着与你相同的经历：大多数人虽然觉得它们有用，但在实际工作中使用起来却非常不舒服。

有趣的是，同样的人却很愿意制作毫无用处的海量UML图表。

我认为这主要有两个原因：

a.) 很多开发人员对正式方法所需的抽象层次感到不适。事实上，大多数入门级的数学教育都是关于微积分和非离散数学，这可能与此有关。

b.) 正式方法需要一种自下而上的设计方法，你需要从底层开始设计核心模型并使其无懈可击，然后通过提供一个接口来将其连接到实际用户需求上。由于我们往往是根据需求推动开发工作，因此自上而下的方法感觉更加自然，尽管它经常会导致不一致的模型。这就像在房子建成后在地下室后面进行翻修。

开发人员每天必须处理数百万个不良设计的抽象概念，为什么他们在需要处理必要程度的抽象时会感到不舒适？ - user9903
1
在成本低的系统中，形式化方法毫无意义。
在一个生产的网络应用中，你有多个前端盒子，多个后端盒子，多个数据库盒子 - 如果其中任何一个程序失败了，那都不是什么大事。硬件如此便宜，以至于你可以用远远低于正式指定所有软件成本的方式来构建这些系统。
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接