Desenvolvimento do software de segurança SIL4 dos automatismos fixos do Val de Roissy

Technical sheet

Esquema do Val de Roissy

Realização do software de segurança com o método B

Val de Roissy
Val de Roissy

A Siemens Transportation Systems (STS) subcontrata com a CLEARSY a realização dos softwares de segurança com B dos automatismos do futuro VAL de ROISSY : Unidade de Controle dos Alarmes (UCA) e Pilotos Automáticos De Seção (PADS), em nome da Siemens.

Esses softwares representam cerca de 150 000 linhas de ADA no final.

Esses softwares são classificados como SIL4 segundo a norma IEC61508 : EN50126, EN50128, EN50129.

O sistema simplificado

Val de Roissy
Val de Roissy

Alguns números…

Na linha L1 do VAL inaugurada em 4 de Abril de 2007, foram instalados 2 calculadores: o UCA e o PADS (tantos PADS quantos necessários – S por Seção).

Para o software pads :

  • 186 440 linhas para o código de segurança Ada do AS (AS – Aplicativo de Segurança)
  • 30 632 linhas para o código não seguro Ada do AS
  • número de Provas matemáticas: 62 056
  • número de linhas B : 256 653 linhas

Para o software uca :

  • 50 085 linhas para o código de segurança Ada do AS
  • 11 662 linhas para o código não seguro Ada do AS
  • número de Provas matemáticas : 12 811
  • número de linhas B : 65 722 linhas

O número de linhas B efetivas é menor do que o anunciado porque teve em consideração comentários, incluindo comentários que orientam os refinamentos.

Uma segunda linha para o aeroporto Charles de Gaulle deverá ser inaugurada em Junho de 2007.

Publicações e comentários

  • Documento de introdução : realização dos softwares de segurança SIL4 do Val de Roissy : descarregar
  • Conferência ZB2005 : Artigo « Using B as a High Level Programming Language in an Industrial » : descarregar
  • Conferência ZB2005 : Apresentação (transparências) « Using B as a High Level Programming Language in an Industrial Project »: descarregar
  • Météor : a Successful Application of B in a Large Project », FM’99, Toulouse, França, 1999 – Behm P., Benoît P., Faivre A., Meynadier J.-M. SpringerLink.com
  • Vital software: Formal method and coded processor – ERTS 2006 – 25-27 Janeiro 2006 – Toulouse – Dollé D. descarregar o artigo
  • Formal Methods in Industry: Achievements, Problems, Future – Jean Raymond Abrial Swiss Federal Institute of Technology Zurich : Portal.acm.org
  • MetroPole : um artigo sobre o Val de Roissy