Serviço · Oferta âncora
Apoio à Qualificação de Ferramentas e
Certificação
As saídas do ESBMC só contam como evidência de certificação se a própria ferramenta for qualificada para o seu nível de garantia. Construímos os artefatos de qualificação que sustentam esse argumento; kits DO-330, evidência de Tool Confidence Level da ISO 26262, pacotes alinhados à IEC 61508 e apoio a Common Criteria; para revisão pelo seu DER ou avaliador de segurança funcional.
O problema
Uma prova formal não é, por si só, evidência de certificação
Reguladores aeroespaciais, automotivos, ferroviários, de segurança industrial e médicos exigem todos que qualquer ferramenta cuja saída seja usada como evidência de verificação seja ela própria qualificada a um nível compatível com a integridade de segurança do software sendo verificado. O ESBMC não é diferente.
Sem um pacote de qualificação, um contraexemplo ou prova do ESBMC é um insight de engenharia, útil, mas improvável de ser aceito na avaliação de segurança. Nosso papel é fornecer a evidência de qualificação que seu DER ou avaliador precisa considerar.
Nossa abordagem
Um kit de qualificação que você pode entregar ao seu DER ou avaliador
Trabalhamos lado a lado com seus engenheiros de segurança, gerentes de certificação e DERs (ou seu gerente de segurança funcional da ISO 26262) para produzir os artefatos que seu caso de garantia precisa, escritos na linguagem e na estrutura que o regulador espera.
O pacote acompanha seu projeto. À medida que as versões do ESBMC evoluem, mantemos a baseline de configuração e reverificamos a evidência de qualificação para que seu safety case permaneça vivo.
Padrões que abordamos
Escopo de qualificação
DO-178C / DO-330
Software Considerations in Airborne Systems (DO-178C) e o padrão complementar de qualificação de ferramentas de software (DO-330). Ajudamos a construir os artefatos de qualificação que sustentam as saídas do ESBMC como evidência de ferramenta qualificada do DAL A ao DAL E, sujeito à aceitação pelo seu DER ou avaliador.
ISO 26262
Veículos rodoviários, segurança funcional. Fornecemos evidência de Tool Confidence Level (TCL) conforme ISO 26262-8 §11, adequada para qualificação de ferramentas de desenvolvimento de software do ASIL A ao ASIL D.
IEC 61508
Segurança funcional de sistemas elétricos / eletrônicos / eletrônicos programáveis relacionados à segurança. Pacotes de qualificação de ferramentas alinhados ao SIL para controle industrial, energia e segurança de processos.
EN 50128 / EN 50657
Aplicações ferroviárias, software para controle ferroviário / software embarcado. Evidência de qualificação de ferramentas alinhada ao regime de classificação de ferramentas dos padrões.
ISO/IEC 15408 (Common Criteria)
A verificação formal sustenta os Evaluation Assurance Levels mais altos (EAL5+) tipicamente exigidos para a certificação de firmware de secure-element, TEE e raiz de confiança.
IEC 62304
Ciclo de vida de software de dispositivos médicos. Argumentos de qualificação de ferramentas adaptados à classificação de segurança de software da IEC 62304 (Classe A–C).
O que você recebe
Entregáveis
Tool Qualification Plan (TQP)
Um plano formal cobrindo o uso pretendido do ESBMC, o contexto operacional e a evidência de qualificação, estruturado para encaixar-se em seus planos DO-178C (PSAC / SDP / SVP / SCMP / SQAP) ou no seu safety case da ISO 26262.
Tool Operational Requirements (TOR)
Uma especificação precisa e testável do que o ESBMC faz em seu projeto, do que suas saídas significam e de como essas saídas são usadas como evidência de verificação.
Casos de Validação e Verificação de Ferramenta
Evidência de validação de que o ESBMC se comporta conforme especificado em seu ambiente operacional, incluindo gerenciamento de configuração, evidência de build determinístico e rastreamento de problemas conhecidos.
Racional de classificação TCL (ISO 26262)
Uma análise documentada de Tool Impact / Tool Error Detection que leva a um Tool Confidence Level defensável, com a evidência de suporte exigida para aplicabilidade ASIL D.
Matriz de rastreabilidade
Rastreabilidade bidirecional dos seus requisitos de segurança às propriedades formais verificadas pelo ESBMC e às provas ou contraexemplos resultantes.
Apoio de ligação com DER / avaliador
Podemos participar de revisões de Stage of Involvement (SOI) com seu Designated Engineering Representative ou avaliador independente, e responder a questões esclarecedoras sobre a evidência de qualificação da ferramenta ESBMC.
Por que nós
Uma base de evidência crível para avaliadores
- O ESBMC vem sendo continuamente desenvolvido e validado em competições desde 2008, com mais de 50 prêmios nas competições internacionais SV-COMP e Test-Comp (TACAS/FASE 2012–2026).
- A mesma equipe produziu as publicações canônicas do ESBMC (IEEE Transactions on Software Engineering 2011, ICSE'11 Distinguished Paper, ASE'24 Distinguished Paper, ASE'23 Most Influential Paper), uma base de evidência incomumente forte para um argumento de qualificação de ferramenta.
- Lucas Cordeiro é Diretor do Arm Centre of Excellence na University of Manchester e membro do EPSRC Peer Review Full College, com experiência direta no apoio à verificação industrial em esforços de código aberto patrocinados por Intel, Arm e AWS.
Nota. Esta é uma oferta de serviço. A Cyber-Reasoning Consultancy (CRC) produz pacotes de evidência de qualificação de ferramentas para revisão pelo seu Designated Engineering Representative, representante da EASA / FAA / UK CAA, ISO 26262 Functional Safety Assessor, avaliador da IEC 61508 ou organismo notificado. As decisões de admissibilidade permanecem com o avaliador; não atuamos como autoridade certificadora e não garantimos a aceitação regulatória de qualquer pacote em particular. A CRC não é um FAA Designated Engineering Representative, uma agência listada pela EASA nem um organismo de certificação acreditado. Onde necessário, trabalhamos lado a lado, e deferimos, aos seus avaliadores nomeados.
Buscando a aprovação DO-178C, ISO 26262 ou IEC 61508?
Conte-nos seu nível de garantia alvo e a parte do ciclo de vida que o ESBMC apoiará. Escoparemos o pacote de qualificação e o preço de acordo.