DO-332, o Princípio de Substituição de Liskov e a consistência do tipo local aumentam a certificação DO-178
O DO-332, suplemento do padrão DO-178C sobre tecnologia orientada a objetos (OOT) e técnicas relacionadas, analisa as questões levantadas pela orientação de objetos em software crítico à segurança e fornece novas orientações para lidar com as vulnerabilidades da OOT. Um novo objetivo importante do DO-332 é a “Verificação da Consistência do Tipo Local”, que explora um resultado de teoria do tipo conhecido como “Princípio de Substituição de Liskov” e ajuda a enfrentar alguns dos principais desafios de certificação levantados pela flexibilidade dinâmica da OOT.
A Tecnologia Orientada a Objetos (OOT) é amplamente utilizada e é suportada por uma série de linguagens de programação, incluindo C++, Java e Ada, mas por várias razões sua popularidade não se espalhou para o ar e outros softwares críticos à segurança. O problema subjacente é a complexidade da verificação de software que faz uso de três dos elementos básicos da OOT: herança, polimorfismo e ligação dinâmica. (A Figura 1 explica o básico de orientação do objeto.) Um exemplo simples ilustra as questões:
Figura 1: Noções básicas de orientação de objetos
Suponha que a classe Sensor seja a raiz de uma hierarquia de herança, ref é uma referência polimórfica a um objeto de qualquer classe nesta hierarquia, e Reset é uma operação definida de forma diferente para diferentes classes de sensor. A declaração do árbitro. Reset(…) se liga dinamicamente à versão apropriada, com base na classe do objeto denotado pelo árbitro. Como se verifica se essa invocação atende aos requisitos da operação Reset?
Um problema surge se a herança for usada para definir uma subclasse que não seja uma especialização do Sensor. O Reset desta subclasse pode ter algum efeito não relacionado à redefinição de um sensor, ou pode gerar uma exceção. Seria um erro o árbitro referenciar um objeto de tal subclasse, e seria necessário analisar que o erro não poderia ocorrer. Isso complica o processo de verificação.
Outra questão diz respeito à análise da cobertura estrutural. Para sistemas em qualquer um dos três níveis mais altos (A, B ou C) dos padrões DO-178, a cobertura completa da declaração deve ser demonstrada usando testes baseados em requisitos. Mas existem várias estratégias de implementação que um compilador pode escolher para lidar com a vinculação dinâmica, com diferentes implicações sobre o que significa “cobertura de declaração”. O escopo da cobertura estrutural não deve depender da estratégia de implementação que o compilador utiliza.
O DO-332[1], o suplemento OOT para DO-178C[2], abordou essas questões através do novo conceito de consistência do tipo local, que explora o princípio de que a herança só deve ser usada para especialização de classe.
Herança e o Princípio de Substituição de Liskov
Em um design orientado a objetos, a arquitetura do sistema reflete as classes e suas relações. Uma relação particularmente importante é a especialização (“é a”), mas há muitas outras. A implementação do projeto envolve a escolha de mecanismos linguísticos para capturar as relações.
Em uma linguagem orientada a objetos, a herança pode ser usada para implementar uma variedade de relações entre duas classes. No entanto, anomalias podem surgir quando a herança é usada para qualquer coisa além da especialização, uma vez que as operações definidas para a superclasse podem não fazer sentido para a subclasse. A restrição da herança às relações de especialização tem sido estudada no contexto da teoria do tipo, onde é conhecido como Princípio de Substituição de Liskov (LSP)[3]. Informalmente, o PSL significa que, sempre que uma instância de uma superclasse pode ser usada, substituir uma instância de qualquer subclasse deve ser permitida.
O uso da herança para especialização tem uma importante interação com as pré-condições e pós-condições de uma operação (seu “contrato”). Uma pré-condição é um pressuposto que a operação está fazendo em relação ao estado do programa quando a operação é invocada. Uma pós-condição é uma garantia que a operação está fazendo no estado do programa quando a operação é concluída. As pré e pós-condições podem ser especificadas explicitamente – seja no texto-fonte, como na Ada 2012[4] ou no SPARK[5], ou separadamente – ou podem estar implícitas na lógica da operação.
Se a herança for em conformidade com o LSP, a versão de uma subclasse de uma operação não deve impor uma pré-condição mais forte (mais restritiva) do que a versão da superclasse. Caso contrário, uma invocação pode ter sucesso em alguns casos (em uma instância de superclasse), mas falhar em outros (em uma instância de subclasse). Análogamente, a versão de uma subclasse de uma operação não deve especificar uma condição post mais fraca (mais geral) do que a versão da superclasse.
Cumprir com o LSP significa, portanto, satisfazer duas propriedades:
- Consistência do contrato: Nenhuma operação de subclasse fortalece uma pré-condição ou enfraquece uma condição pós-operatório da operação de superclasse que está substituindo.
- Consistência comportamental: Cada operação de subclasse atende aos requisitos de suas superclasses.
O DO-332 captura esses conceitos em um novo objetivo, verificação de consistência do tipo local. Esse objetivo não requer demonstrar que a hierarquia de classes está em conformidade com o PSL, o que seria excessivamente restritivo. Em vez disso, reflete que o esforço de verificação é mais simples para arquiteturas de classe que cumprem, e que a análise só precisa considerar o contexto local.
Consistência do tipo local
A Figura 2 mostra a atividade associada à verificação da consistência do tipo local, que o DO-332 requer para software nos níveis A, B ou C. A redação “para cada subtipo onde a substituição é usada” refere-se a contextos onde ocorre ligação dinâmica, como ref. Reset(…), e o “subtipo” em questão é a classe de um objeto que o árbitro poderia referenciar naquele momento. As classes potenciais não serão necessariamente a hierarquia completa, e diferentes conjuntos de classes podem ser aplicáveis em diferentes invocações da mesma operação.
Figura 2: A atividade associada à verificação da consistência do tipo local, que o DO-332 requer para software nos níveis A, B ou C
Considere uma ocorrência particular de árbitro. Reset(…), e deixe o HeatSensor ser uma das possíveis subclasses para os objetos que o árbitro poderia referenciar lá. Consistência local do árbitro. Reset(…) para HeatSensor pode ser demonstrado “otimistamente” ou “pessimista”. A abordagem otimista funciona se o HeatSensor satisfaz o LSP, e pode ser realizado de duas maneiras:
- Através de métodos formais, demonstrando que a versão do HeatSensor de Reset atende aos requisitos para a versão do Sensor e não fortalece as pré-condições ou enfraquece as pós-condições do Reset do Sensor.
- Através de testes, executando os testes baseados em requisitos para a versão do Sensor de Reset, usando uma instância do HeatSensor.
Métodos formais podem ser facilitados pelo suporte adequado da linguagem de programação e seu ponto de ferramentas, por exemplo, Ada 2012 ou SPARK.
A abordagem otimista demonstrará a consistência contratual e comportamental entre as versões da superclasse e da subclasse da operação. A verificação adicional é obtida através de testes baseados em requisitos para a subclasse e possivelmente também através de métodos formais.
Se as classes não cumprirem o LSP, ou se houver poucas chamadas dinamicamente vinculadas ou a hierarquia for rasa e/ou estreita, então pode ser mais simples apenas testar cada caso possível que possa surgir. Este é o teste pessimista especificado no terceiro item da bala na Figura 2. Testes baseados em requisitos são necessários para exercer a operação para cada subclasse que possa surgir.
DO-332, consistência do tipo local e certificação do guia LSP
A verificação da consistência do tipo local é apenas um aspecto do uso do OOT com segurança; O DO-332 contém orientações sobre outros elementos OOT, bem como técnicas relacionadas, como modelos genéricos. DO-332 é “agnóstico de linguagem”; mais detalhes estão disponíveis sobre como aplicar OOT em sistemas de segurança crítica ou de alta segurança, usando a Ada 2012 como a linguagem de programação[6].
A orientação de consistência local do DO-332 é consistente com a abordagem geral do DO-178C para verificação, garantindo que todos os testes sejam baseados em requisitos. Adapta as atividades de verificação de forma inédita para refletir a semântica da orientação de objetos e o grau de conformidade da estrutura de classe com o LSP. A nova orientação deve ajudar a promover o uso seguro da Programação Orientada a Objetos (OOP) em aviônicos e outros domínios críticos.
Referências
- [1] RTCA/EUROCAE DO-178C/ED-12C. Considerações de Software em Sistemas Aéreos e Certificação de Equipamentos, dezembro de 2011.
- [2] RTCA/EUROCAE DO-332/ED-217. Suplemento de tecnologia orientada a objetos e técnicas relacionadas ao DO-178C e DO-278A, dezembro de 2011.
- [3] B. Liskov e J. Wing. “Uma noção comportamental de subtipagem”, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, Edição 6 (novembro de 1994), pg. 1811-1841.
- [4] Manual de Referência de Idiomas Ada 2012 (dezembro de 2012), www.ada-auth.org/standards/ada12.html
- [5] J. Barnes com Altran Praxis. SPARK – A abordagem comprovada do software de alta integridade. Altran Praxis, 2012.
- [6] AdaCore, Programação Orientada a Objetos de Alta Integridade em Ada, julho de 2011. extranet.eu.adacore.com/articles/HighIntegrityAda.pdf