Hispanopedia Wiki
Articulo de referencia

AbsInt

AbsInt es un proveedor de herramientas de desarrollo de software con sede en Saarbrücken , Alemania . La empresa se fundó en 1998 como una escisión tecnológica del Departamento ...

Hispanopedia WikiContenido en espanolLectura gratuita

AbsInt es un proveedor de herramientas de desarrollo de software con sede en Saarbrücken , Alemania . La empresa se fundó en 1998 como una escisión tecnológica del Departamento de Lenguajes de Programación y Construcción de Compiladores del Prof. Reinhard Wilhelm en la Universidad de Saarland . AbsInt se especializa en herramientas de verificación de software basadas en interpretación abstracta . [ 1 ] Sus herramientas son utilizadas en todo el mundo por empresas de la lista Fortune 500, instituciones educativas, agencias gubernamentales y startups.

Productos

El analizador aiT WCET calcula estáticamente límites superiores seguros para el tiempo de ejecución en el peor de los casos [ 2 ] de tareas en sistemas en tiempo real . Analiza directamente ejecutables binarios y tiene en cuenta el comportamiento intrínseco de la caché y la tubería del microprocesador . [ 3 ] La Administración Nacional de Seguridad del Tráfico en Carreteras de EE. UU. (NHTSA) y la NASA lo utilizaron en su Estudio sobre la aceleración repentina no intencionada en los sistemas de control electrónico del acelerador de vehículos Toyota. [ 4 ]

StackAnalyzer determina el uso máximo de pila de las tareas en aplicaciones embebidas y puede demostrar la ausencia de desbordamiento de pila . Los resultados del análisis son válidos para todas las entradas y cada ejecución de tarea. [ 5 ] StackAnalyzer se utiliza en las industrias aeroespacial, médica, de telecomunicaciones y de transporte.

Astrée es un analizador de programas estático que demuestra la ausencia de errores en tiempo de ejecución en aplicaciones embebidas críticas para la seguridad escritas o generadas automáticamente en C. [ 6 ] Se utiliza en las industrias de Defensa/Aeroespacial, Médica, Control Industrial, Electrónica, Telecomunicaciones/Transmisión de Datos y Transporte. Astrée es originario del grupo de Patrick Cousot en el CNRS / ENS y es desarrollado y distribuido por AbsInt bajo licencia del CNRS/ENS. En la 6.ª Exposición de Herramientas de Análisis Estático (SATE VI) [ 7 ] del NIST (2020), se confirmó que Astrée cumple con los Criterios de Análisis de Sonido de Ockham de SATE VI. [ 8 ]

RuleChecker es un analizador de programas estático que comprueba automáticamente el código C/ C++ para verificar su conformidad con las directrices de codificación, incluidas MISRA C /C++, SEI CERT C , CWE , ISO/IEC TS 17961:2013 y las Directrices de Codificación Adaptive Autosar C++.

TimeWeaver es una herramienta híbrida de análisis WCET que combina el análisis estático de rutas y el análisis estático de valores con el rastreo no intrusivo a nivel de instrucción en tiempo real para acotar el tiempo de ejecución en el peor de los casos ( WCET ). Este enfoque funciona con una amplia gama de procesadores modernos de alto rendimiento ( multinúcleo ).

CompCert es un compilador C optimizador formalmente verificado . Su uso previsto es la compilación de software crítico para la seguridad y la misión, escrito en C y que cumpla con altos niveles de garantía. Genera código máquina para las arquitecturas PowerPC , ARM y AArch64 , IA32 ( x86 de 32 bits ), AMD64 y RISC-V (de 32 y 64 bits ). Desde 2015, AbsInt ofrece licencias comerciales, proporciona soporte y mantenimiento de nivel industrial y contribuye al avance de la herramienta. Por el desarrollo de CompCert, Xavier Leroy y el equipo de desarrollo de CompCert recibieron el premio ACM Software System Award 2021 .

Historia

AbsInt es un proyecto derivado del Departamento de Lenguajes de Programación y Compiladores de la Universidad de Saarland , fundado en 1998 , donde sus creadores desarrollaron un marco genérico y generativo para analizadores y optimizadores de programas estáticos a nivel binario. Un componente importante de este marco es el Generador de Analizadores de Programas (PAG), que permite generar automáticamente analizadores estáticos a partir de una especificación matemática de los dominios abstractos y las funciones de transferencia. [ 9 ] La primera versión de PAG se publicó en 1995. Con PAG/WWW, está disponible una versión académica gratuita que se ha utilizado en numerosos cursos de enseñanza en todo el mundo.

En 2001, se lanzó la línea de productos StackAnalyzer para el análisis estático del uso de la pila , seguida de la línea de productos aiT WCET Analyzer en 2002. En 2004, tan solo seis meses después de su lanzamiento, aiT recibió el Premio Europeo de Tecnologías de la Sociedad de la Información [ 10 ] por "productos innovadores que representan lo mejor de la innovación europea en tecnologías de la sociedad de la información". En 2004, aiT se utilizó para analizar el software de control de vuelo del Airbus A380 , el avión de pasajeros más grande del mundo. [ 11 ] En 2006, los analizadores superaron con éxito el primer WCET Tool Challenge realizado por la Universidad de Mälardalen . En 2010, aiT y StackAnalyzer se integraron en SCADE Suite de Esterel Technologies , convirtiéndose así en el primer entorno de desarrollo de software embebido del mundo en incorporar análisis de pila y WCET a nivel de modelo. [ 12 ]

El desarrollo de Astrée comenzó desde cero en noviembre de 2001 por el Prof. Patrick Cousot en el Laboratoire d'Informatique de la École Normale Supérieure (LIENS), inicialmente apoyado por el proyecto ASTRÉE, el Centre National de la Recherche Scientifique, la École Normale Supérieure y, desde septiembre de 2007, por INRIA (París-Rocquencourt). Astrée significa Analyseur statique de logiciels temps-réel embarqués ("analizador estático de software integrado en tiempo real"). Se ha utilizado con éxito en el software de control de vuelo del AIRBUS A340 y A380, [ 13 ] donde no generó falsas alarmas, incluso para cálculos complejos que involucran números de punto flotante. En abril de 2008, Astrée pudo demostrar la ausencia de cualquier error de ejecución en una versión en C del software de acoplamiento automático del Vehículo de Transferencia Automatizado (ATV) Jules Verne, utilizado para transportar cargas útiles a la Estación Espacial Internacional . [ 14 ] Desde 2009, Astrée está disponible comercialmente a través de AbsInt bajo licencia de ENS/CNRS.

AbsInt ha participado en numerosos proyectos de investigación financiados por la Comisión Europea y el Ministerio Federal de Educación e Investigación de Alemania , como DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, entre otros.

El nombre AbsInt deriva de la interpretación abstracta , una metodología basada en la semántica para el análisis estático de programas . [ 15 ]

Referencias

  1. ↑ Kästner, D.; Ferdinand, C. (2011). Verificación eficiente de propiedades de seguridad no funcionales mediante interpretación abstracta: tiempos, consumo de pila y ausencia de errores de ejecución . Actas de la 29.ª Conferencia Internacional sobre Seguridad de Sistemas ISSC2011, Las Vegas.
  2. ↑ Wilhelm, Reinhard; Engblom, Jakob; Ermedahl, Andreas; Holsti, Niklas; Thesing, Stephan; Whalley, David; Bernat, Guillem; Ferdinand, Christian; Heckmann, Reinhold; Mitra, Tulika; Mueller, Frank; Puaut, Isabelle; Puschner, Peter; Staschulat, Jan; Stenström, Per (2008). "El problema del tiempo de ejecución en el peor de los casos: descripción general de los métodos y análisis de las herramientas". ACM Transactions on Embedded Computing Systems . 7 (3): 1– 53. CiteSeerX 10.1.1.458.3540 . doi : 10.1145/1347375.1347389 . S2CID 2139310 .  
  3. ↑ Ferdinand, Christian; Wilhelm, Reinhard (1999). "Predicción rápida y eficiente del comportamiento de la caché para sistemas en tiempo real". Sistemas en tiempo real . 17 ( 2– 3): 131– 181. doi : 10.1023/a:1008186323068 . S2CID 28282721 . 
  4. ↑ NASA (18 de enero de 2011). Asistencia técnica a la Administración Nacional de Seguridad del Tráfico en Carreteras (NHTSA) sobre la investigación de aceleración involuntaria (UA) de Toyota Motor Corporation (TMC) (Informe técnico). pág. 151. 
  5. ↑ Ferdinand, Christian; Heckmann, Reinhold (2007). "Análisis de memoria estática y tiempo de ejecución de código embebido". SAE 2006 Transactions Journal of Passenger Cars — Electronic and Electrical Systems . SAE Technical Paper Series. 9 2006-01-1499. doi : 10.4271/2006-01-1499 .
  6. ↑ Kästner, D.; Wilhelm, S.; et al. (2010). Astrée: Demostrando la ausencia de errores en tiempo de ejecución . Embedded Real Time Software and Systems Congress ERTS², Toulouse. 
  7. ↑ SATE VI Criterios de análisis de sonido de Ockham
  8. ↑ Black, Paul; Walia, Kanwardeep (2020). NISTIR8304 -- SATE VI Criterios de análisis de sonido de Ockham (Informe). Instituto Nacional de Estándares y Tecnología de EE. UU. (NIST). doi : 10.6028/NIST.IR.8304 .
  9. ↑ Alt, Martin; Martin, Florian (1995). "Generación de analizadores interprocedimentales eficientes con PAG". Actas del 2.º Simposio Internacional sobre Análisis Estático (SAS '95) . Lecture Notes in Computer Science (983): 33–50 . CiteSeerX 10.1.1.37.9598 . doi : 10.1007/3-540-60360-3_31 . 
  10. ↑ ict-prize.org en web.archive.org , consultado el 29.09.2023
  11. ↑ Souyris, Jean; Le Pavec, Ervan; Himbert, Guillaume; Jégu, Victor; Borios, Guillaume; Heckmann, Reinhold (2005). Cálculo del tiempo de ejecución en el peor de los casos de un programa de aviónica mediante interpretación abstracta . Actas del 5.º Taller Internacional sobre Tiempo de Ejecución en el Peor de los Casos (WCET '05), Mallorca, España. pp. 21–24 . 
  12. ↑ Ferdinand, C.; Heckmann, R.; Le Sergent, T.; Lopes, D.; Martin, B.; Fornari, X.; Martin, F. (2008). Combinación de una herramienta de diseño de alto nivel para sistemas críticos de seguridad con una herramienta para el análisis del tiempo de ejecución en el peor de los casos (WCET) en ejecutables . 4.º Congreso Europeo ERTS — Software en tiempo real integrado, Toulouse.
  13. ↑ Delmas, D.; Souyris, J. (2007). "ASTRÉE: de la investigación a la industria". Actas del 14.º Simposio Internacional de Análisis Estático (SAS'07), Kongens Lyngby, Dinamarca . Lecture Notes for Computer Science 4634, Springer: 437–451 .
  14. ↑ Bouissou, O.; Conquet, E.; et al. (2009). Validación de software espacial mediante interpretación abstracta . Actas de la 13.ª Conferencia sobre Sistemas de Datos en el Espacio, DASIA 2009, Estambul, Turquía. 
  15. ↑ Cousot, Patrick; Cousot, Radhia (1977). Interpretación abstracta: un modelo reticular unificado para el análisis estático de programas mediante la construcción o aproximación de puntos fijos . Cuarto Simposio Anual ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación. págs. 238–252 . 
  • Sitio web oficial
Lecturas relacionadas
6 articulos
SaarbrückenSaarbrückenSaarbrücken [ a ] es la capital y ciudad más grande del estado de Sarre , Alemania. La ciudad tiene 181.959 habitantes y es el centro administrativ...AlemaniaAlemaniaAlemania , oficialmente República Federal de Alemania , es un país de Europa Central . Se encuentra entre el mar Báltico y el mar del Norte al nort...Universidad de SaarlandUniversidad de SaarlandLa Universidad de Saarland ( en alemán: Universität des Saarlandes , pronunciado [ univɛʁziˈtɛːt dɛs ˈzaːɐ̯landəs ] ) es una universidad pública de...{\displaystyle n}Interpretación abstractaEn informática , la interpretación abstracta es una teoría de aproximación sólida de la semántica de los programas informáticos , basada en funcion...Tiempo de ejecución en el peor de los casosTiempo de ejecución en el peor de los casosEl tiempo de ejecución en el peor de los casos ( WCET ) de una tarea computacional es el tiempo máximo que podría tardar la tarea en ejecutarse en ...MicroprocesadorMicroprocesadorInstrumentos de Texas TMS1000 Intel 4004 Motorola 6800 (MC6800) Un procesador x86-64 moderno de 64 bits (AMD Ryzen Threadripper 7970X, basado en Ze...