¿Por qué se utiliza Lustre para la programación de software de control crítico (centrales nucleares, etc.)?

7

Entonces, como se indica en wikipedia:

  

Lustre es un flujo de datos síncrono y formalmente definido, declarativo   Lenguaje de programación para la programación de sistemas reactivos. Comenzó como un   Proyecto de investigación a principios de los años ochenta. Una presentación formal de la   El lenguaje se puede encontrar en las Actas de 1991 del IEEE. En 1993   progresado a la práctica, uso industrial en un producto comercial como el   lenguaje central del entorno industrial SCADE, desarrollado por   Tecnologías de Esterel. Ahora se utiliza para el software de control crítico en   Aviones, helicópteros y plantas de energía nuclear.

Me pregunto por qué se usan lenguajes como este para el software de control crítico y por qué se han desarrollado. Por ejemplo, ¿se puede escribir en C?

¿Por qué es necesario diseñar este tipo de idiomas específicos? ¿Porque son "más rápidos" o porque están estrictamente diseñados para el sistema en el que están?

    
pregunta Josip Ivic 24.08.2016 - 10:31

1 respuesta

9
  

¿Por qué se usan lenguajes como este (Lustre) para el software de control crítico?

Debido a que algunas herramientas de software (o incluso la metodología) pueden ayudar a parcialmente a probar la corrección del código w.r.t. algunas especificaciones formalizadas, y debido a que otras herramientas de software (o las mismas, por ejemplo, SCADE) pueden generar algún código C (que sería "más seguro" y quizás más rápido de lo que el código escrito a mano puede realistamente lograr) de la fuente de Lustre.

Lea sobre análisis del programa de fuente estática .

Observe que existen algunas herramientas para ayudar a demostrar que algunos programas en C (con un estilo de codificación restringido) son de alguna manera "seguros" o "correctos" w.r.t. alguna especificación formalizada ; p.ej. consulte Frama-C .

También, recuerde que algunos subgrupos de lenguajes de programación (por ejemplo, la mayoría de Ocaml, gracias a él sistema de tipos , pero sin su el infame Obj.magic trick ) puede "garantizar" por diseño que su programa ganó No choques (escribe alguna hipótesis).

Pero recuerda: hay No Silver Bullet : debido a la indecidibilidad de Halting Problem , no puede esperar probar completamente ningún software (y no puede esperar formalizar completamente sus especificaciones y su entorno; debe aceptar que el software es abstracciones ...)

Lea también el blog de Lattner: Lo que todo programador de C debería saber sobre comportamiento indefinido

Por cierto, varias industrias (incluidas las nucleares, aeronaves e incluso dispositivos de salud, etc.) tienen sus especificaciones y regulaciones con respecto al software crítico para la seguridad. Por ejemplo, DO-178C para los aviones comerciales. En tales casos, el software cuesta mucho lot (por ejemplo, por línea de código) que su aplicación de teléfono habitual, y la metodología de desarrollo de software es muy diferente (y mucho más burocrática: documentará y necesitará han aceptado y probado formalmente cualquier cambio, incluso un parche de línea).

    
respondido por el Basile Starynkevitch 24.08.2016 - 10:37

Lea otras preguntas en las etiquetas