Abordagem de engenharia para desenvolvimento de software

Como testar idéias, arquitetura e algoritmos sem escrever código? Como formular e verificar suas propriedades? O que são verificadores de modelos e localizadores de modelos? Requisitos e especificações - uma relíquia do passado?

Oi Meu nome é Vasil Dyadov, agora trabalho como programador em Yandex, antes de trabalhar na Intel, mesmo antes desenvolvi código RTL (nível de transferência de registro) no Verilog / VHDL para ASIC / FPGA. Há muito tempo que gosto do tópico de confiabilidade de software e hardware, matemática, ferramentas e métodos usados ​​para desenvolver software e lógica com propriedades predefinidas garantidas.

Este é o meu primeiro artigo de uma série projetada para chamar a atenção de desenvolvedores e gerentes para a abordagem de engenharia do desenvolvimento de software. Recentemente, ele foi imerecidamente ignorado, apesar das mudanças revolucionárias em sua abordagem e ferramentas de suporte.

Não vou dissimular: a principal tarefa do artigo é despertar interesse. Portanto, haverá um mínimo de longo raciocínio e um máximo de especificidade.

O artigo tem duas partes. No primeiro, descreverei o que quero dizer com abordagem de engenharia; no segundo, mostrarei um exemplo de uso da abordagem no quadro de uma tarefa simples (próximo ao campo da arquitetura de microsserviços).

Estou sempre aberto para discutir questões relacionadas ao desenvolvimento de software e terei prazer em conversar com os leitores (as coordenadas de comunicação estão no meu perfil).

Parte 1. Abordagem de engenharia para o desenvolvimento

O que é isso Vou mostrar o exemplo da construção de uma ponte:

• O estágio 1 é a coleção de requisitos para a ponte: o tipo de ponte, capacidade de carga, etc.
• Etapa 2 - especificação de requisitos e cálculo de estruturas (especificação).
• Etapa 3 - a própria construção real com base em cálculos de engenharia (especificações).

Obviamente, essa é uma analogia simplificada. Ninguém faz pontes de protótipo para esclarecer requisitos e especificações. A parametrização não pode ser adicionada à ponte para que fique arqueada ou suspensa. Mas, no geral, acho que a analogia é clara.

No desenvolvimento de software, as etapas 1 e 2 geralmente estão ausentes ou são muito pouco expressas. Se os requisitos são fixos, é vago, incompleto e informal. Apenas alguns detalhes detalham e desenvolvem especificações claras.

Muitas pessoas pensam que isso é uma perda de tempo, uma relíquia do passado, especialmente se a abordagem ágil para o desenvolvimento for escolhida (especialmente com iterações curtas). E este é um grande erro.

Porque

Para começar, entenderemos quais são esses requisitos e especificações e qual é sua diferença significativa, o que nem sempre é óbvio para muitos profissionais.

Quais são os requisitos?

Em resumo, os requisitos são a formulação das propriedades do produto em termos de área de assunto. Por exemplo, assim: "Todas as instâncias do programa devem processar igualmente solicitações de entrada".

Os requisitos não usam os termos do escopo de implementação. Assim que os termos "sincronização de estado", Raft, Paxos, "complexidade logarítmica no tempo" vazam para os requisitos, então os requisitos e as especificações começam a se misturar.

É importante entender isso e separar claramente um do outro.

Porque

1. Os requisitos devem ser claros para os consumidores de software, portanto, devem ser da área de assunto para a qual o software está sendo desenvolvido (geralmente, os especialistas que estão longe do desenvolvimento precisam estar envolvidos na formulação de requisitos e na definição de uma tarefa para o desenvolvimento de software).

   
   

2. As propriedades de software que um consumidor vê são avaliadas por métricas da área de assunto. É necessário separar requisitos e especificações para poder 1) identificar as principais métricas do produto pelas quais o consumidor avaliará nosso software e 2) entender claramente quais propriedades do produto são importantes para o usuário e quais não são.

   
   

Caso contrário, isso pode acontecer da seguinte maneira: os desenvolvedores, que não cumprem os prazos, sacrificam propriedades importantes e dedicam muito tempo e atenção a outras sem importância. Além disso, o que parece importante do ponto de vista do desenvolvimento de software pode não ser importante do ponto de vista do usuário.

Um exemplo clássico de tal discrepância é dado em uma variedade de literatura sobre desenvolvimento da interface do usuário e em artigos (por exemplo: Tempo de resposta do sistema e satisfação do usuário: um estudo experimental de aplicativos baseados em navegador , latência do computador: 1977-2017 ). Os desenvolvedores geralmente tentam otimizar o tempo de execução de uma operação, por exemplo, procurando informações em um banco de dados, e o tempo de resposta do usuário é importante. E se a pesquisa for lenta, mas o usuário começa a ver os resultados retornados o mais rápido possível, parece-lhe que esse software funciona melhor do que o que pesquisa rapidamente, mas primeiro acumula os resultados e finalmente exibe todos eles.

É por isso que os planejadores de recursos do sistema operacional diferem nos modos operacionais do servidor e da área de trabalho. Para o modo de servidor, a taxa de transferência máxima do sistema é importante, ou seja, otimização de tempo e memória para usar com eficiência o servidor. E para o usuário, o atraso na resposta do sistema é importante. Quanto mais rápido o sistema responde às ações, mais rápido parece, mesmo que funcione mais devagar.

E, finalmente, o motivo mais importante:

Se requisitos e especificações são misturados, significa que não entendemos completamente as tarefas para as quais estamos desenvolvendo software. Começamos a formular e resolver problemas da área de assunto no campo do desenvolvimento de software. Portanto, a lógica do domínio vaza e confunde a lógica do código. O resultado é um código fortemente acoplado, difícil de manter.

Isso foi bem escrito por Michael Jackson no livro Problem Frames: Analyzing & Structuring Problems Software Development . Na minha opinião, este é um dos livros mais úteis para desenvolvedores de software. Ele ensina, antes de tudo, a analisar os problemas dos usuários, que um bom software deve resolver. Um programa super rápido que consome poucos recursos do sistema, mas não resolve as tarefas do usuário, é um programa ruim. Legal, mas ruim.

Qual é a especificação?

Uma especificação é uma formulação de propriedades de software em termos de um campo de desenvolvimento de software. É aqui que os conceitos de complexidade, sincronização etc.

As especificações podem ser organizadas hierarquicamente: do abstrato ao específico, no qual você pode escrever o código. Essa abordagem geralmente é a mais eficaz. As especificações abstratas refletem facilmente a arquitetura - você pode ver as propriedades básicas, encontrar erros de arquitetura etc. Portanto, podemos encontrar problemas nos estágios iniciais do ciclo de vida do software e reduzir significativamente o custo de correção de erros.

É especialmente importante notar o benefício e a importância das especificações para protocolos e interfaces entre os componentes do sistema, o que ajudará a evitar essas situações:

Qual é a diferença da abordagem usual de desenvolvimento?

Na abordagem de engenharia, pré-projetamos software com as características necessárias de acordo com as especificações. Verificamos as especificações para as propriedades necessárias que vêm dos requisitos.

Fiz uma comparação na forma de um tablet (muito subjetivo):

E não é o modelo de agitação para um modelo de desenvolvimento em cascata aqui?

A engenharia de software, incluindo especificações e simulações formais, combina bem com a abordagem ágil.

Acredita-se que a abordagem de engenharia para o desenvolvimento seja incompatível com o rápido desenvolvimento de software iterativo (conforme declarado em muitos artigos, aqui está um exemplo ).

Mas isso não é verdade. A abordagem de engenharia foi aplicada com sucesso em muitos projetos, incluindo projetos com iterações curtas.

Anteriormente, devido a meios e ferramentas de suporte pouco desenvolvidos, a abordagem de engenharia estava realmente intimamente ligada ao modelo em cascata.

Mas agora tudo mudou drasticamente.

Graças aos sucessos inovadores no campo da modelagem, resolvedores SAT / SMT, etc., agora é possível verificar rapidamente grandes espaços de estados do sistema quanto à presença das propriedades de que precisamos e à ausência de desnecessárias, para verificar os volumes industriais do código etc.

Apareceram ferramentas industriais de primeira classe, como Alloy, TLA + / TLC, Atelier B, PRISM, que transferiram a tarefa de formalizar e verificar as especificações acadêmicas / matemáticas, exigindo altas qualificações e grandes esforços, para a tarefa de botões, acessível à maioria dos programadores.

Agora, as especificações podem ser desenvolvidas de forma iterativa e incremental. Os modelos são bem projetados iterativamente, do abstrato ao concreto. O tempo de simulação de sistemas grandes é calculado em minutos e horas.

É fácil especificar requisitos de forma iterativa, especialmente com abordagens e ferramentas modernas.
E o refinamento de requisitos, especificações, refatoração de modelos, código de gravação e sua refatoração podem facilmente ser paralelos - dentro de uma iteração.

Em geral, a abordagem de engenharia agora não é absolutamente igual ao modelo em cascata, essas são duas coisas independentes.

A abordagem de engenharia é facilmente combinada com qualquer metodologia da organização de desenvolvimento.

O blog de Hillel Wayne mostra como é fácil trabalhar com especificações e modelos formais. Ele tem um ótimo exemplo de como especificar formalmente a lógica da interface do usuário de um programa em 10 minutos e verificar algumas de suas propriedades.

Não vou entrar em detalhes e traduzir o artigo inteiro, apenas mostrarei a especificação em Alloy :

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, : , , .

, — , , - .

.

, , .

$$, $$ $$.

Alloy : X->Y.

( util/relation):

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, , , :

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:

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) .

:

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]
}

.

.

, .

:

1. ;
2. ;
3. ;
4. ;
5. ;
6. .

. . : .

, ? ?

.

, , .

, .

, :

• ( , );
• ;
• ;
• .

.

, .

:

1. -> ;
2. -> ;
3. -> ;
4. -> .

, .

, : , . - , — , / .

, : -> .

, :

• ;
• .

, .

, 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" , $$ . 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:

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

, :

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.

!

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. , :

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). .

, , , . .

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

Alloy

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

1. Hillel Wayne
   . , . , .

1. . . , . . , . . .
   , , .

Alloy

1. Alloy Analyzer + Higher-Order Alloy
   Alloy.
2. Online Tutorial
   , .
3. Tutorial Materials
   .