AbsInt

AbsInt
AbsInt Angewandte Informatik Gmb
유형게셀샤프트미트베슈렌크테르하프퉁
산업소프트웨어 검증 도구
설립.1998년; 24년 전(1998년)
본사
자르브뤼켄
,
독일.
주요 인물
설립자:크리스티안 페르디난트, 다니엘 케스트너, 마르크 랑겐바흐, 플로리안 마틴, 스테판 테싱, 라인하르트 빌헬름
상품들aiT, Stack Analyzer, Arstée, RuleChecker, CompCert, TimingProfiler, TimeWeaver
웹 사이트www.absint.com

AbsInt는 독일 자르브뤼켄에 본사를 둔 소프트웨어 개발 도구 벤더입니다.1998년 Programming Languages and Compiler Construction of Programming Languages and Compiler Construction of Programming Languages에서 테크놀로지를 분사하여 설립되었습니다. 자르랜드 대학의 라인하르트 빌헬름입니다.AbsInt는 추상적 [1]해석에 기초한 소프트웨어 검증 툴을 전문으로 합니다.이 툴은 Fortune 500대 기업, 교육기관, 정부기관 및 스타트업이 전 세계에서 사용하고 있습니다.

상품들

aiT WCET Analyzer는 실시간 시스템에서 최악의 경우 작업[2] 실행 시간에 대한 안전 상한을 정적으로 계산합니다.바이너리 실행 파일을 직접 분석하여 마이크로프로세서의 고유 캐시 및 파이프라인 동작을 [3]고려합니다.미국 고속도로교통안전국(NHTSA)과 NASA는 도요타 [4]차량의 전기 스로틀 제어 시스템의 급발진에 관한 연구(Study on Surnalent Acceleration)에서 이를 사용했다.

Stack Analyzer는 임베디드 응용 프로그램 태스크의 최대 스택 사용률을 결정하고 스택오버플로의 부재를 증명할 수 있습니다.분석 결과는 모든 입력 및 각 태스크 [5]실행에 대해 유효합니다.Stack Analyzer는 항공우주, 의료, 통신 및 운송 산업에서 사용됩니다.

Arstie는 [6]C에서 작성되거나 자동으로 생성되는 안전성에 중요한 임베디드 애플리케이션에서 런타임 오류가 없음을 증명하는 정적 프로그램 분석기입니다.방위/항공우주, 의료, 산업 제어, 전자, 통신/데이터콤 및 운송 산업에서 사용됩니다.아스트레는 CNRS/ENS의 Patrick Cousot 그룹에서 시작되었으며 AbsInt에 의해 CNRS/ENS의 라이센스에 따라 개발 및 배포됩니다.

RuleChecker는 MISRA C/C++, SEI CERT C, CWE, ISO/IEC TS 17961:2013 및 Adaptive Autosar C+ Coding Guidelines 등의 코딩 가이드라인을 준수하는지 자동으로 체크하는 정적 프로그램 분석기입니다.

TimeWeaver는 정적 경로 분석 및 정적 값 분석과 비침입적 실시간 명령 수준 추적을 결합하여 WCET(Worst-Case Execution Time)를 제한하는 하이브리드 WCET 분석 도구입니다.이 접근방식은 광범위한 최신 고성능(멀티코어) 프로세서에 적용됩니다.

CompCert는 공식적으로 검증된 최적화 C 컴파일러입니다.C로 작성된 안전 크리티컬 및 미션 크리티컬 소프트웨어를 컴파일하여 높은 수준의 보증을 충족시키는 것이 목적입니다.PowerPC(32비트), ARM 및 IA32(x86 32비트) 아키텍처의 머신 코드를 생성합니다.2015년 이후 복근Int는 상용 라이선스를 제공하고, 산업용 지원 및 유지보수를 제공하며, 도구의 발전에 기여합니다.

역사

AbsInt는 1998년 Saarland University Programming Languages and Compiler 학과의 분사로 설립자는 바이너리 수준의 정적 프로그램 분석기와 옵티마이저를 위한 범용 생성 프레임워크를 개발했습니다.이 프레임워크의 중요한 컴포넌트는 Program Analyzer Generator PAG로 추상 도메인 및 전송 함수의 [7]수학적 사양에서 정적 분석기를 자동으로 생성할 수 있습니다.PAG의 첫 번째 버전은 1995년에 출시되었습니다.PAG/WW를 사용하면 전 세계에서 다양한 교육 과정에 사용되고 있는 PAG의 무료 학술 버전을 이용할 수 있습니다.

2001년에는 스태틱스택 사용률 분석을 위한 Stack Analyzer 제품군이 출시되었으며, 2002년에는 aiT WCET Analyzer 제품군이 출시되었습니다.2003년 aiT는 출범 반년 만에 '정보사회 기술에서 유럽 최고의 혁신을 대표하는 획기적인 제품'으로 유럽정보사회기술상을 수상했다.2004년, aiT는 세계에서 가장 큰 여객기인 에어버스 [8]A380의 비행 제어 소프트웨어를 분석하는 데 사용되었다.2006년, Analyzer는 Mélardalen 대학이 실시한 최초의 WCET Tool Challenge(인용)에 합격했습니다.2010년에 aiT와 Stack Analyzer는 Estel Technologies의 SCADE Suite에 통합되었습니다.이것에 의해, WCET와 스택 분석을 모델 [9]레벨로 채용한 세계 최초의 임베디드 소프트웨어 개발 환경이 되었습니다.

아스트레는 2001년 11월 교수에 의해 처음부터 개발되기 시작했다.에콜 노르말 수페리외르(LIENS)의 인포마티케 연구소의 패트릭 쿠소(Patrick Cousot)는 처음에는 ASTREE 프로젝트, 국립 레체 사이언티피크 센터, 에콜 노르말 수페리외르 센터, 2007년 9월부터는 인리아(Par-encourtis)의 지원을 받았다.Arstée는 Analyzur statique de logiciels temps-réel embaqués(실시간 임베디드 소프트웨어 정적 분석기)의 약자입니다.이는 에어버스 A340과 A380의 [10]비행 제어 소프트웨어에서 성공적으로 사용되어 부동소수점 숫자와 관련된 복잡한 계산에도 허위 경보를 발생시키지 않았다.2008년 4월,[11] 아스트레는 국제우주정거장으로의 페이로드 수송에 사용되는 Jules Verne Automated Transfer Vehicle(ATV)의 C버전에서 런타임 에러가 없음을 증명할 수 있었습니다.2009년 이후 AbsInt에서 ENS/CNRS의 라이선스로 상업적으로 이용할 수 있게 되었습니다.

AbsInt는 DAEDALUS, AL-TIMES, Interested, Verisoft, PREDOR, TIMMO2USE, MBAT 등 유럽위원회와 독일 교육연구부의 자금 지원을 받는 많은 연구 프로젝트에 참여해 왔습니다.

AbsInt라는 이름은 정적 프로그램 분석을 위한 의미 기반 방법론인 추상 해석에서 유래했습니다.

레퍼런스

  1. ^ Kästner, D.; Ferdinand, C. (2011). Efficient Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors. Proceedings of the 29th International System Safety Conference 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). "The Worst-Case Execution-Time Problem — Overview of Methods and Survey of Tools". ACM Transactions on Embedded Computing Systems. 7 (3): 1–53. CiteSeerX 10.1.1.458.3540. doi:10.1145/1347375.1347389.
  3. ^ Ferdinand, Christian; Wilhelm, Reinhard (1999). "Fast and Efficient Cache Behavior Prediction for Real-Time Systems". Real-Time Systems. 17 (2–3): 131–181. doi:10.1023/a:1008186323068.
  4. ^ NASA (January 18, 2011). Technical Support to the National Highway Traffic Safety Administration (NHTSA) on the Reported Toyota Motor Corporation (TMC) Unintended Acceleration (UA) Investigation (Technical report). p. 151.
  5. ^ Ferdinand, Christian; Heckmann, Reinhold (2007). "Static Memory and Execution Time Analysis of Embedded Code". SAE 2006 Transactions Journal of Passenger Cars — Electronic and Electrical Systems. SAE Technical Paper Series. 9. doi:10.4271/2006-01-1499.
  6. ^ Kästner, D.; Wilhelm, S.; et al. (2010). Astrée: Proving the Absence of Runtime Errors. Embedded Real Time Software and Systems Congress ERTS², Toulouse.
  7. ^ Alt, Martin; Martin, Florian (1995). "Generation of Efficient Interprocedural Analyzers with PAG". Proceedings of the 2nd International Symposium on Static Analysis (SAS '95). Lecture Notes in Computer Science (983): 33–50. CiteSeerX 10.1.1.37.9598. doi:10.1007/3-540-60360-3_31.
  8. ^ Souyris, Jean; Le Pavec, Ervan; Himbert, Guillaume; Jégu, Victor; Borios, Guillaume; Heckmann, Reinhold (2005). Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation. Proceedings of the 5th International Workshop on Worst-case Execution Time (WCET '05), Mallorca, Spain. pp. 21–24.
  9. ^ Ferdinand, C.; Heckmann, R.; Le Sergent, T.; Lopes, D.; Martin, B.; Fornari, X.; Martin, F. (2008). Combining a High-Level Design Tool for Safety-Critical Systems with a Tool for WCET Analysis on Executables. 4th European Congress ERTS — Embedded Real Time Software, Toulouse.
  10. ^ Delmas, D.; Souyris, J. (2007). "ASTRÉE: from research to industry". Proceedings of the 14th Intl. Static Analysis Symposium (SAS'07), Kongens Lyngby, Denmark. Lecture Notes for Computer Science 4634, Springer: 437–451.
  11. ^ Bouissou, O.; Conquet, E.; et al. (2009). Space software validation using Abstract Interpretation. Proceedings of 13th Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey.

외부 링크