👩🏿‍🤝‍👩🏻 👨🏿‍🤝‍👨🏾 💤 软件开发的工程方法 👩🏾 🗝️ ✖️

如何在不编写代码的情况下测试思想，体系结构和算法？如何制定和验证其性质？什么是模型检查器和模型查找器？要求和规格-过去的遗物？

你好我的名字叫Vasil Dyadov，现在我是Yandex的程序员，在加入英特尔之前，我曾经在Verilog / VHDL上为ASIC / FPGA开发RTL代码（寄存器传输级别）。我一直很喜欢软件和硬件可靠性，用于开发具有保证的预定义属性的软件和逻辑的数学，工具和方法的主题。

这是我在该系列中的第一篇文章，旨在吸引开发人员和管理人员注意软件开发的工程方法。最近，尽管他的方法和支持工具发生了革命性的变化，但他仍然理应受到忽视。

我不会反驳：这篇文章的主要任务是唤起人们的兴趣。因此，将有最少的冗长推理和最大的特异性。

本文分为两个部分。在第一篇中，我将描述工程方法的含义，在第二篇中，将显示在简单任务的框架中使用该方法的示例（接近微服务体系结构领域）。

我总是乐于讨论与软件开发相关的问题，并且很高兴与读者聊天（交流的坐标在我的个人资料中）。

第1部分。开发的工程方法

这是什么我将向您展示建造桥梁的示例：

第1阶段是对桥梁的要求的集合：桥梁的类型，负载能力等。
第2阶段-需求规范和结构计算（规范）。
第三阶段-基于工程计算（规格）的实际施工本身。

当然，这是一个简化的类比。没有人制造原型桥来阐明要求和规格。无法将参数化添加到网桥，以使其成为拱形或悬挂式。但是总的来说，我认为这个比喻很清楚。

在软件开发中，步骤1和步骤2通常不存在或表达得很弱。如果要求是固定的，则它是模糊，不完整和非正式的。仅需几个详细的要求并制定明确的规范。

许多人认为这是浪费时间，是过去的遗迹，尤其是如果选择了敏捷的开发方法（尤其是短迭代）。这是一个很大的错误。

怎么了

首先，我们将了解这样的要求和规范是什么，以及它们的显着区别是什么，这对于许多专业人员而言并不总是显而易见的。

有什么要求？

简而言之，要求是根据主题领域来制定产品属性。例如，如下所示：“程序的所有实例都应同样处理输入请求。”

这些要求不使用实施范围内的条款。一旦Raft，Paxos，“时间的对数复杂性”等术语“状态同步”渗入需求中，那么需求和规范就会开始混在一起。

重要的是要理解这一点，并清楚地将它们彼此分开。

怎么了

需求应该对软件的使用者是清楚的，因此，需求应该来自正在开发软件的主题领域（通常，距离开发远的专家必须参与制定需求和为软件开发设定任务）。
消费者看到的软件属性由主题区域指标评估。为了能够1）识别消费者用来评估我们的软件的主要产品指标，有必要分开要求和规范，2）清楚地了解哪些产品属性对用户很重要，哪些不重要。

否则，结果可能是这样的：开发人员未按时完成任务，将牺牲重要属性，并将大量时间和精力投入到不重要的属性上。此外，从软件开发的角度看似乎重要的东西从用户的角度看可能并不重要。

有关用户界面开发的各种文献和文章（例如：系统响应时间和用户满意度：基于浏览器的应用程序的实验研究，计算机延迟：1977–2017 ）中给出了这种差异的经典示例。开发人员通常会尝试优化操作的执行时间，例如，在数据库中搜索信息，而用户的响应时间很重要。而且，如果搜索速度很慢，但是用户开始尽快看到返回的结果，则在他看来，这种软件要比快速搜索但先累积结果并最终显示所有结果的软件更好。

这就是为什么OS资源计划员在服务器和桌面操作模式上有所不同的原因。对于服务器模式，系统的最大吞吐量很重要，即优化时间和内存以有效使用服务器。对于用户而言，系统响应的延迟很重要。系统对动作的响应速度越快，即使它运行得越慢，它看起来也会越快。

最后，最重要的原因：

如果要求和规格混杂在一起，则意味着我们不完全了解要开发软件的任务。 我们开始从软件开发领域的主题领域来制定和解决问题。 因此，域逻辑会泄漏并混淆代码逻辑。 结果是紧密耦合的代码难以维护。

这是Michael Jackson在《问题框架：分析和构建软件开发问题》一书中写得很好的。我认为，这是对软件开发人员最有用的书之一。它首先教导分析用户的问题，好的软件应该解决这些问题。占用很少系统资源却无法解决用户任务的超快速程序是一个糟糕的程序。酷，但不好。

规格是多少？

规范是根据软件开发领域对软件属性的表述。这是复杂性，同步等概念的所在。

规范可以按层次进行组织：从抽象到特定，您可以在上面编写代码。这种方法通常是最有效的。抽象规范很容易反映体系结构-您可以看到基本属性，发现体系结构错误等。因此，我们可以在软件生命周期的早期阶段发现问题，并显着降低修复错误的成本。

特别值得一提的是，系统组件之间的协议和接口的规范的好处和重要性，这将有助于避免以下情况：

与通常的开发方法有何不同？

在工程方法中，我们根据规格预先设计了具有所需特性的软件。我们检查规格中是否有来自要求的必要属性。

我以平板电脑的形式进行了比较（非常主观）：

物业资料	工程方法	工艺方法
要求说明	详细，常用的ReqIF格式和相关工具（例如Eclipse RMF）	细节通常很小，措辞不准确，非正式
技术指标	通常使用形式，B方法，Z，VDM，TLA +，Alloy等。	你是什么什么规格？我们在文件中写了我们需要做的事情以及它应该如何工作，这就足够了
调试和建模规范	Pro-B，工作室B，TLA + / TLC，合金，PRISM，VECS等	哦，那会是什么样？
突出指标	详细，基于规格和型号	好吧，我们将提出一些指标，写在Wiki页面上
代码开发	根据规格和型号	好吧，像往常一样：拍手-在生产中
测试中	针对模型上确定的边缘案例的基于模型的目标测试；方向随机化由模型生成。根据接口和交互协议的规范集成边缘案例。基于模型的LTL属性的监督机；定向模糊边界模型检查（例如Divine）	好吧，像往常一样：进行一些单元测试，然后我们将考虑典型案例并添加集成和系统案例；模糊检测某些关键功能（模糊检测以发现多线程软件中的同步错误？）；我们在消毒剂下进行一些测试
验证码	例如，使用GNATprove或Frama-C，从规范中获取属性，注释代码，并正式证明该代码符合正式规范；否则我们将使用Atelier B在最后阶段通过代码生成从规范逐步迭代到实现；或选择其他方法	不，它令人恐惧，漫长且昂贵，而且我们没有制定用于正式验证的属性：要检查哪些合规性？

这不是瀑布开发模型的搅动模型吗？

软件工程，甚至包括正式的规范和仿真，都可以采用敏捷方法。

可以相信，开发的工程方法与快速迭代的软件开发不兼容（如许多文章所述，这里是一个示例）。

但是事实并非如此。工程方法已成功应用于许多项目，包括迭代次数短的项目。

以前，由于开发手段和支持工具不完善，工程方法确实与瀑布模型紧密相关。

但是现在一切都发生了巨大变化。

由于在建模，SAT / SMT求解器等领域取得了突破性的成功，现在可以快速检查系统状态的巨大空间，以了解我们需要的属性是否存在以及是否存在不必要的属性，以验证代码的工业规模等。

出现了一流的工业工具，例如Alloy，TLA ++ / TLC，Atelier B，PRISM，将规范和检查规范的任务从需要高资历和巨大努力的学术/数学领域转移到了大多数程序员都可以使用的一键式任务中。

现在可以迭代和逐步开发规格。从抽象到具体，模型都是经过精心设计的。大型系统的仿真时间以分钟和小时为单位。

可以轻松地反复指定需求，尤其是使用现代方法和工具时。
需求，规范，模型重构，代码编写及其重构的优化可以轻松地并行进行-一次迭代即可。

通常，工程方法现在根本不等于瀑布模型，这是两个独立的事物。

工程方法很容易与任何开发组织方法结合。

Hillel Wayne的博客显示了使用正式规范和模型是多么容易。他有一个很好的例子，说明了如何在10分钟内正式指定程序用户界面的逻辑并检查其某些属性。

我不会详细介绍和翻译整篇文章，而只是在Alloy中显示规范本身：

UI规范

open util/ordering[Time]
sig Time {
    state: one State
}
abstract sig State {}
abstract sig Login extends State {}
abstract sig Reports extends Login {}

one sig Logout extends State {}
one sig Students, Summary, Standards extends Reports {}
one sig Answers extends Login {}

pred transition[t: Time, start: State, end: State] {
  t.state in start
  t.next.state in end
}

pred logout[t: Time] { transition[t, Login, Logout] }
pred login[t: Time] { transition[t, Logout, Summary] }
pred students[t: Time] { transition[t, Reports, Students] }
pred summary[t: Time] { transition[t, Reports, Summary] }
pred standards[t: Time] { transition[t, Reports, Standards] }
pred answers[t: Time] { transition[t, Students, Answers] }
pred close_answers[t: Time] { transition[t, Answers, Students] }

fact Trace {
  first.state = Summary
  all t: Time - last |
    logout[t] or
    login[t] or
    students[t] or
    summary[t] or
    standards[t] or
    answers[t] or
    close_answers[t]
}

, . , UI .

check {all t: Time | t.state = Answers implies 
        t.prev.state = Students} for 7

, , .

agile.

— .

, , — Alloy, .

, , ( ) .

( ) , .

, .

2. Alloy

Alloy, : , , .

, — , , - .

, , .

$\big\{x,y\big\}$ , $x \in X$ $y \in Y$ .

Alloy : X->Y.

( util/relation):

relation.als

module relation

-- :
-- set A -    A,   
-- one A -       A
-- lone A -    A   
-- some A -      A

-- :
-- univ -       ,
--            
-- iden -   {A0, A0},     
--               univ
--        iden = {a : univ, b: univ |  a=b}
--            
-- none -  

-- :
-- : and, or, => (), != ( ), not
--  :
-- & - 
-- A->B -      .
--        
-- X<:Y -     Y ,   
--           X
-- A in B -  A   B
-- ~A -     A
-- A + B - 
-- no A - A ,  A = none
-- ^A -     A,
--         B , :
--      A in B,
--      {E0, E1}, {E1, E2} in B => {E0, E2} in B
-- A.B -  JOIN,  . :
--       {A0, B0} in A, {B0, C0, D0} in B, 
--       {A0, C0, D0} in A.B 

-- :
-- all X : Y | .... - 
-- some X : Y | .... - 

--  :
-- pred[a: A, b:B] {...}    
-- : pred[a, b]  a.pred[b]
--       
-- -,    
-- method(self : Object, args ...)

pred valid [rel : univ->univ, dom : set univ, cod : set univ] {
  rel.univ in dom and rel.univ in cod
}
fun domain [rel : univ->univ] : set (rel.univ) { rel.univ }
fun codomain [rel : univ->univ] : set (univ.rel) { univ.rel }
pred total  [rel: univ->univ, dom: set univ] {
  all x: dom | some x.rel
}
pred partial [rel: univ->univ, dom: set univ] {
  all x: dom | lone x.rel
}
pred functional [rel: univ->univ, dom: set univ] {
  all x: dom | one x.rel
}
pred surjective [rel: univ->univ, cod: set univ] {
  all x: cod | some rel.x
}
pred injective [rel: univ->univ, cod: set univ] {
  all x: cod | lone rel.x
}
pred bijective [rel: univ->univ, cod: set univ] {
  all x: cod | one rel.x
}
pred bijection [rel: univ->univ, dom, cod: set univ] {
  rel.functional[dom] and rel.bijective[cod]
}
pred reflexive [rel: univ->univ, s: set univ] {
  s<:iden in rel
}
pred irreflexive [rel: univ->univ] {no iden & rel}
pred symmetric [rel: univ->univ] {~rel in rel}
pred antisymmetric [rel: univ->univ] {~rel & rel in iden}
pred transitive [rel: univ->univ] {rel.rel in rel}
pred acyclic [rel: univ->univ, s: set univ] {
  all x: s | x not in x.^rel
}
pred complete[rel: univ->univ, s: univ] {
  all x,y:s | (x!=y => x->y in (rel + ~rel))
}
pred preorder [rel: univ->univ, s: set univ] {
  rel.reflexive[s] and rel.transitive
}
pred equality [rel: univ->univ, s: set univ] {
  rel.preorder[s] and rel.symmetric
}
pred partial_order [rel: univ->univ, s: set univ] {
  rel.preorder[s] and rel.antisymmetric
}
pred total_order [rel: univ->univ, s: set univ] {
  rel.partial_order[s] and rel.complete[s]
}

, , Alloy.

utils/graph, , , :

graph.als

module graph[node]
open relation

--     
fun nodes[r: node->node]: set node {
  r.domain+ r.codomain
}

--  ,     
--       
--   
pred connected[r: node->node] {
  all n1,n2 : r.nodes | n1 in n2.*(r + ~r)
}

--    
pred dag [r: node->node] {
  r.acyclic[r.nodes]
}

--    
--   ,   
--   
fun roots [r: node->node] : set node {
  let ns = r.nodes | -- ns -   
    ns - ns.^r --     ,
               --    -
               --  
}

--   
--  -  ,  
--   
fun leaves [r: node->node] : set node {
  let ns = r.nodes | -- ns -   
    ns - ns.^~r --     ,
                --    -
                --  
}

— , .

(1) — , , ;
(2) — , , ;
(3) — , ;
(4) , — ;
(5) . . , , , ;
(6) , — , .

, , Alloy:

compgraph.als

module compgraph[node]

open graph[node]
open relation

pred valid [edges: node->node,
            source : one node, --  1
            drain : one node --  2
] {
  edges.antisymmetric and edges.irreflexive --  6
  graph/roots[edges] = source --  1  4
  graph/leaves[edges] = drain --  2  4
}

open compgraph[node] as cg -- cg -  

enum node {n0, n1, n2, n3, n4}
--    ,    

run cg/valid --     cg,  
  --  valid    : relation  compgraph

, ( ).

, .

. . , .

, . :

— , . . ;
— ;
— , . . , .

, , . . ( , ).

, :

(7) ( ). , , ;
(8) , . . .

, .

, , , .

(9) , .

(, , ) :

(10) .

compgraph.als

module compgraph[node]

open graph[node]

pred active[edges : node->node,
            source: node,
            n : node
] {
  -- n    ,
  --   
  n in source.^edges
}

pred safe[edges : node->node,
          drain : node,
          n : node
] {
  --    ,  drain,
  --      n
  --      
  --  n     
  --  
  no n.*edges & (leaves[edges] - drain)
  --     , 
  --       
  --     ,
  --  ,     drain
  drain in n.*edges
}

pred valid [edges: node->node,
            source : one node, --  1
            drain : one  node --  2
] {
  edges.connected --     
                  --     ( 
                  --        ),
                  --      , 
                  -- ,   
                  --  connected
  edges.dag --  6  8
  source in edges.roots --  1, 4  9
  drain in edges.leaves --  2, 4  8
  all n : edges.roots - source |
    not active[edges, source, n] --  9
  all n : edges.nodes | -- 10 
    active[edges, source, n] => safe[edges, drain, n]
}

, .

;
;
;
;
;
.

. . : .

, ? ?

, , .

, .

, :

( , );
;
;
.

, .

-> ;
-> ;
-> ;
-> .

, .

, : , . - , — , / .

, : -> .

, :

;
.

, .

, Alloy , . , Alloy .

pred connect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node, 
  to : one node
] {
  --    
  from->to not in old_edges

  -- from   to,
  --    
  from not in to.*old_edges

  -- to    ,
  --    
  -- 
  to in (old_edges.nodes - source)

  --   to  
  -- ,   
  --   to  
  safe[old_edges, drain, to]

  --    ,
  --      
  --  
  new_edges = old_edges + from->to
}

connect .

, connect :

open compgraph[node] as cg

sig node {}

check {
  --      r1, r2
  all r1, r2 : node->node |
  --     source, drain, from, to
  all source, drain, from, to : node  {
    -- r1     
    -- source/drain /
    --  r2   r1   
    -- connect  from->to
    (cg/valid[r1, source, drain] and
     connect[r1, r2, source, drain, from, to])
    --   ,  r2 + source/drain
    --    
    -- 
    implies cg/valid[r2, source, drain]
    --    connect  
    --  
  }
} for 8

Executing "Check check$1 for 8"
   Sig this/node scope <= 8
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6], [node$7]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   8374 vars. 168 primary vars. 22725 clauses. 108ms.
   No counterexample found. Assertion may be valid. 26904ms

Alloy . , "168 primary vars" , $2^{168}$ . 30 !

, connect .

, :

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  --     
  from->to in old_edges

  --    from
  --   
  safe[new_edges, drain, from]

  --    
  new_edges.connected

  --  
  new_edges = old_edges - from->to
}

open compgraph[node] as cg
sig node {}
check {
  all r1, r2 : node->node |
  all source, drain, from, to : node  {
    (cg/valid[r1, source, drain] and
     disconnect[r1, r2, source, drain, from, to])
    implies cg/valid[r2, source, drain]
  }
} for 8

! ! :

disconnect

, r1, — disconnect, r2 — . , r1, r2, r2 .

, — from->to, source ( from) .

disconnect:

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  from->to in old_edges
  ( safe[new_edges, drain, from] or
   (from not in new_edges.nodes and
    from != source))
  new_edges.connected
  new_edges = old_edges - from >to
}

Executing "Check check$2 for 8"
   Sig this/node scope <= 8
   Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6], [node$7]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   8505 vars. 168 primary vars. 24808 clauses. 207ms.
   No counterexample found. Assertion may be valid. 18369ms.

, .

, ?

, ? ?

--     
--     ,
-- ,       
--       
check {
  all r1,r2: node->node | all source,drain: node |
  some intermediate : seq node->node {
     cg/valid[r1, source, drain] and cg/valid[r2, source, drain]
     =>
     intermediate.first = r1 and
     intermediate.last = r2 and
     all i : intermediate.inds - intermediate.lastIdx {
       let from = intermediate[i] |
       let to = intermediate[i+1] |
       some n1, n2 : node |
         connect[from,to, source, drain, n1, n2]
         or
         disconnect[from, to, source, drain, n1, n2]
     }
  }
} for 3

Executing "Check check$3"
   Sig this/node scope <= 3
   Sig this/node in [[node$0], [node$1], [node$2]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
A type error has occured: (see the stacktrace)
Analysis cannot be performed since it requires higher-order
quantification that could not be skolemized.

Alloy: .

«some intermediate…», — .

( , ) , .

higher-order Alloy, , . , CEGIS — counter-example guided inductive synthesis.

, .

, , , :

check {
  all edges, edges1 : node->node |
  all source,drain, from, to : node {
    (cg/valid[edges, source, drain] and
    cg/valid[edges1, source, drain] and
    edges1 = edges + from->to and
    edges1 != edges)
    =>
    some n1, n2: node | connect[edges, edges1, source, drain, n1, n2]
  }
} for 7

, :

connect

Executing "Check check$3 for 7"
   Sig this/node scope <= 7
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   6471 vars. 133 primary vars. 16634 clauses. 200ms.
   Counterexample found. Assertion is invalid. 116ms.

— , — . from->to.

, connect (, , ).

connect:

connect

pred connect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node, 
  to : one node
] {
  from->to not in old_edges
  from not in to.*old_edges
  to in (old_edges.nodes - source)
  --   
  active[old_edges, source, from] => safe[old_edges, drain, to]
  --   to    from,
  -- ,   to     ,
  --   from,    
  --   
  new_edges.connected
  --   ,    
  --    :)
  new_edges = old_edges + from -> to
}

Executing "Check check$3 for 7"
   Sig this/node scope <= 7
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   6513 vars. 133 primary vars. 16837 clauses. 125ms.
   No counterexample found. Assertion may be valid. 291ms.

disconnect. , :

diconnect

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  from->to in old_edges
  --       ,
  --     
  active[old_edges, source, from] => safe[new_edges, drain, from]
  -- ,      
  -- ,     :
  -- (from not in new_edges.nodes and
  --  from != source)

  new_edges.connected
  new_edges = old_edges - from->to
}

, , / , .

, , (, source->drain), connect/disconnect .

( , , ).

?

, .

, , , . .

: , ( safe/active .).

, .

, — , . .

, .

, , ( ) .

?

Alloy .

, , , Python.

, ( ) .

?

Alloy Analyzer, GitHub — .

Alloy?

, , - ;
, , , assert’ , . .;
( );
, , , . , , .

. Facebook, Google, Microsoft, Amazon .

Amazon Web Services, , (Use of Formal Methods at Amazon Web Services, Formal reasoning about the security of Amazon Web Services, Amazon Relies on Formal Methods for the Security of AWS)
Facebook ().
Google ().
Microsoft , (Spec#, Formal Methods at Scale in Microsoft, Formal Methods and Toolsfor Distributed Systems).

, , .

agile- , .

, : .

, , , , (TLA+/TLC, B-method/Atelier B, Promela/SPIN). .

, , , . .

Michael Jackson Problem Frames: Analysing & Structuring Software Development Problems
( !), . , .
Daniel Jackson Software Abstractions: Logic, Language, and Analysis
model finder Alloy . , . ( join, ). , .
. MODEL CHECKING.
. , , . , .

Alloy

Pamela Zave. How to Make Chord Correct
Alloy DHT Chord, ( , ), . , .
1. Alloy, .

Hillel Wayne
. , . , .

. . , . . , . . .
, , .

Alloy

Alloy Analyzer + Higher-Order Alloy
Alloy.
Online Tutorial
, .
Tutorial Materials
.

软件开发的工程方法

第1部分。开发的工程方法

有什么要求？

规格是多少？

与通常的开发方法有何不同？

这不是瀑布开发模型的搅动模型吗？

2. Alloy

?

?

?

Alloy?

Alloy

Alloy

More articles: