AbsInt
 | |
| Typ | Gesellschaft mit beschränkter Haftung |
|---|---|
| Przemysł | Narzędzia do weryfikacji oprogramowania |
| Założony | 1998 |
| Siedziba | , |
Kluczowi ludzie |
Założyciele: Christian Ferdinand, Daniel Kästner, Marc Langenbach, Florian Martin, Stephan Thesing i Reinhard Wilhelm |
| Produkty | aiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver |
| Strona internetowa | |
AbsInt to dostawca narzędzi do tworzenia oprogramowania z siedzibą w Saarbrücken w Niemczech . Firma powstała w 1998 roku jako technologiczna spółka spin-off Katedry Języków Programowania i Budowy Kompilatorów prof. Reinharda Wilhelma na Saarland University . AbsInt specjalizuje się w narzędziach do weryfikacji oprogramowania opartych na abstrakcyjnej interpretacji . Jej narzędzia są używane na całym świecie przez firmy z listy Fortune 500, instytucje edukacyjne, agencje rządowe i startupy.
Produkty
aiT WCET Analyzer statycznie oblicza bezpieczne górne granice dla najgorszego czasu wykonania zadań w systemach czasu rzeczywistego . Bezpośrednio analizuje binarne pliki wykonywalne i bierze pod uwagę wewnętrzną pamięć podręczną i zachowanie potoków mikroprocesora. Amerykańska Narodowa Administracja Bezpieczeństwa Ruchu Drogowego (NHTSA) i NASA wykorzystały go w swoim badaniu dotyczącym nagłego niezamierzonego przyspieszenia w elektronicznych systemach sterowania przepustnicą w pojazdach Toyoty.
StackAnalyzer określa maksymalne wykorzystanie stosu zadań w aplikacjach osadzonych i może udowodnić brak przepełnienia stosu . Wyniki analizy są ważne dla wszystkich danych wejściowych i każdego wykonania zadania. StackAnalyzer jest używany w przemyśle lotniczym, medycznym, telekomunikacyjnym i transportowym.
Astrée to statyczny analizator programów, który udowadnia brak błędów w czasie wykonywania w aplikacjach wbudowanych o krytycznym znaczeniu dla bezpieczeństwa, napisanych lub generowanych automatycznie w C . Jest używany w przemyśle obronnym/lotniczym, medycznym, kontroli przemysłowej, elektronicznym, telekomunikacyjnym/datacom i transportowym. Astrée wywodzi się z grupy Patricka Cousota z CNRS / ENS i jest rozwijany i dystrybuowany przez AbsInt na licencji CNRS/ENS.
RuleChecker to statyczny analizator programów, który automatycznie sprawdza kod C/C++ pod kątem zgodności z wytycznymi kodowania, w tym MISRA C /C++, SEI CERT C , CWE , ISO/IEC TS 17961:2013 i Adaptive Autosar C++ Coding Guidelines.
TimeWeaver to hybrydowe narzędzie do analizy WCET , które łączy statyczną analizę ścieżki i statyczną analizę wartości z nieinwazyjnym śledzeniem na poziomie instrukcji w czasie rzeczywistym w celu ograniczenia czasu wykonania w najgorszym przypadku (WCET ) . Takie podejście sprawdza się w przypadku wielu nowoczesnych, wysokowydajnych ( wielordzeniowych ) procesorów.
CompCert to formalnie zweryfikowany optymalizujący kompilator C. Jego przeznaczeniem jest kompilacja oprogramowania o krytycznym znaczeniu dla bezpieczeństwa i misji, napisanego w C i spełniającego wysokie poziomy pewności. Tworzy kod maszynowy dla architektur PowerPC (32-bitowy), ARM i IA32 (x86 32-bitowy). Od 2015 roku AbsInt oferuje licencje komercyjne, zapewnia wsparcie i konserwację na poziomie przemysłowym oraz przyczynia się do rozwoju narzędzia.
Historia
AbsInt to spin-off z 1998 roku z Wydziału Języków Programowania i Kompilatorów na Uniwersytecie Saary , gdzie jego założyciele opracowali ogólne i generatywne ramy dla statycznych analizatorów i optymalizatorów programów na poziomie binarnym. Ważnym elementem tego frameworka jest Program Analyzer Generator PAG, który pozwala na automatyczne generowanie analizatorów statycznych na podstawie matematycznej specyfikacji dziedzin abstrakcyjnych i funkcji przenoszenia. Pierwsza wersja PAG została wydana w 1995 roku. Wraz z PAG/WWW dostępna jest bezpłatna akademicka wersja PAG, która była używana na całym świecie w licznych kursach dydaktycznych.
W 2001 r. wprowadzono na rynek linię produktów StackAnalyzer do statycznej analizy wykorzystania stosu, a następnie linię produktów aiT WCET Analyzer w 2002 r. W 2003 r., zaledwie pół roku po wprowadzeniu na rynek, aiT otrzymał Europejską Nagrodę Technologiczną Społeczeństwa Informacyjnego za „przełomowe produkty , które reprezentują najlepsze europejskie innowacje w technologiach społeczeństwa informacyjnego”. W 2004 r. aiT wykorzystano do analizy oprogramowania sterującego lotem Airbusa A380, największego na świecie samolotu pasażerskiego. W 2006 roku Analizatory pomyślnie przeszły pierwszy konkurs WCET Tool Challenge przeprowadzone przez Uniwersytet w Mälardalen (cytat). W 2010 roku aiT i StackAnalyzer zostały zintegrowane z SCADE Suite firmy Esterel Technologies , dzięki czemu stało się to pierwszym na świecie środowiskiem programistycznym wbudowanym, które zawiera WCET i analizę stosu na poziomie modelu.
Rozwój Astrée rozpoczął się od podstaw w listopadzie 2001 r. przez prof . , od września 2007 r., przez INRIA (Paryż-Rocquencourt). Astrée oznacza Analyseur statique de logiciels temps-réel embarqués („analizator statyczny wbudowanego oprogramowania w czasie rzeczywistym”). Z powodzeniem zastosowano go w oprogramowaniu do sterowania lotem samolotów AIRBUS A340 i A380, gdzie nie wywołał fałszywych alarmów, nawet w przypadku złożonych obliczeń obejmujących liczby zmiennoprzecinkowe. W kwietniu 2008 roku firma Astrée była w stanie udowodnić brak jakichkolwiek błędów czasu działania w wersji C oprogramowania do automatycznego dokowania pojazdu Jules Verne Automated Transfer Vehicle (ATV) używanego do transportu ładunków na Międzynarodową Stację Kosmiczną . Od 2009 roku Astrée jest dostępny na rynku z AbsInt na licencji ENS/CNRS.
AbsInt brał udział w wielu projektach badawczych finansowanych przez Komisję Europejską i niemieckie Ministerstwo Edukacji i Badań Naukowych , takich jak DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT i innych.
Nazwa AbsInt pochodzi od abstrakcyjnej interpretacji , opartej na semantyce metodologii statycznej analizy programu .