Jump to content

AbsInt: Difference between revisions

Add links
From Wikipedia, the free encyclopedia
Browse history interactively
← Previous edit
Content deleted Content added
VisualWikitext
fix ref
AnomieBOT (talk | contribs)
Bots
6,543,291 edits
m Dating maintenance tags: {{Citation needed}}
 
(34 intermediate revisions by 19 users not shown)
Line 1: Line 1:
{{Undisclosed paid|date=March 2021}}
{{Infobox company
{{Infobox company
| company_name = AbsInt Angewandte Informatik GmbH
| name = AbsInt Angewandte Informatik GmbH
| logo = [[File:Logo AbsInt.png|200px|AbsInt GmbH]]
| logo = Logo AbsInt.png
| type = [[Gesellschaft mit beschränkter Haftung]]
| company_type = [[Private company|Private]]
⚫
| industry = Software Verification Tools
⚫
| key_people = Founders: Christian Ferdinand, Daniel Kästner, Marc Langenbach, Florian Martin, Stephan Thesing, and [[Reinhard Wilhelm]]
| location = Saarbrücken, Germany
| founded = {{Start date and age|1998}}
| hq_location_city = [[Saarbrücken]]
⚫
| industry = Software Verification Tools
| hq_location_country = [[Germany]]
⚫
| products = aiT, StackAnalyzer, Astrée
⚫
| key_people = Founders: Christian Ferdinand, Daniel Kästner, Marc Langenbach, Florian Martin, Stephan Thesing, and [[Reinhard Wilhelm]]
⚫
| homepage = http://www.absint.com
⚫
| products = aiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver
| num_employees =
| num_employees_year =
| revenue =
⚫
| homepage = {{URL|www.absint.com}}
}}
}}
⚫
'''AbsInt''' is a software-development tools vendor based in [[Saarbrücken]], [[Germany]]. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of [[Reinhard Wilhelm|Prof. Reinhard Wilhelm]] at [[Saarland University]]. AbsInt specializes in software-verification tools based on [[abstract interpretation]].<ref name=LasVegas>{{cite conference

⚫
'''AbsInt''' is a software-development tools vendor based in [[Saarbrücken]], [[Germany]]. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of [[Reinhard Wilhelm|Prof. Reinhard Wilhelm]] at [[Saarland University]]. AbsInt specializes in software-verification tools based on [[abstract interpretation]].<ref name=LasVegas>{{cite journal
| first1 = D.
| first1 = D.
| last1 = Kästner
| last1 = Kästner
| first2 = C.
| first2 = C.
| last2 = Ferdinand
| last2 = Ferdinand
| title = Efficient Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors
| title = Efficient Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors
| journal = Proceedings of the 29th International System Safety Conference ISSC2011 Las Vegas
| conference = Proceedings of the 29th International System Safety Conference ISSC2011 Las Vegas
| volume =
| issue =
| year = 2011
| year = 2011
⚫
}}</ref> Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.
⚫
| pages=
⚫
| doi = }}</ref> Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.


==Products==
==Products==
⚫
aiT WCET Analyzer statically computes safe upper bounds for the [[worst-case execution time]]<ref name=ACM>{{cite journal

⚫
aiT WCET Analyzer statically computes safe upper bounds for the [[worst-case execution time]]<ref name=ACM>{{cite journal
| first1 = Reinhard
| first1 = Reinhard
| last1 = Wilhelm
| last1 = Wilhelm
Line 55: Line 56:
| last14 = Staschulat
| last14 = Staschulat
| first15 = Per
| first15 = Per
| last15 = Stenström
| last15 = Stenström
| title = The Worst-Case Execution-Time Problem — Overview of Methods and Survey of Tools
| title = The Worst-Case Execution-Time Problem — Overview of Methods and Survey of Tools
| journal = ACM Transactions on Embedded Computing Systems
| journal = ACM Transactions on Embedded Computing Systems
| volume = 7 (3)
| volume = 7
| issue =
| issue = 3
| year = 2008
| year = 2008
| pages= 1–53
| pages= 1–53
| doi = 10.1145/1347375.1347389| citeseerx = 10.1.1.458.3540
⚫
| doi = }}</ref> of tasks in [[real-time systems]]. It directly analyzes binary executables and takes the intrinsic cache and pipeline behavior of the microprocessor into account.<ref name=RTS>{{cite journal
| s2cid = 2139310
⚫
}}</ref> of tasks in [[real-time systems]]. It directly analyzes binary executables and takes the intrinsic cache and pipeline behavior of the [[microprocessor]] into account.<ref name=RTS>{{cite journal
| first1 = Christian
| first1 = Christian
| last1 = Ferdinand
| last1 = Ferdinand
Line 73: Line 76:
| year = 1999
| year = 1999
| pages=131–181
| pages=131–181
| doi = 10.1023/a:1008186323068| s2cid = 28282721
| doi = }}</ref> The U.S. [[National Highway Traffic Safety Administration]] (NHTSA) and [[NASA]] used it in its [[Unintended acceleration|Study on Sudden Unintended Acceleration]] in the electronic throttle control systems of Toyota vehicles.<ref name=Toyota>{{cite journal
}}</ref> The U.S. [[National Highway Traffic Safety Administration]] (NHTSA) and [[NASA]] used it in its [[Unintended acceleration|Study on Sudden Unintended Acceleration]] in the electronic throttle control systems of Toyota vehicles.<ref name=Toyota>{{cite tech report
| last = NASA
| first =
| last = NASA
⚫
| title = Technical Support to the National Highway Traffic Safety Administration (NHTSA) on the Reported Toyota Motor Corporation (TMC) Unintended Acceleration (UA) Investigation
| coauthors =
⚫
| title = Technical Support to the National Highway Traffic Safety Administration (NHTSA) on the Reported Toyota Motor Corporation (TMC) Unintended Acceleration (UA) Investigation
| journal =
| volume =
| issue =
| date = January 18, 2011
| date = January 18, 2011
| pages=151
| pages=151
| doi = }}</ref>
}}</ref>


StackAnalyzer determines the maximum stack usage of the tasks in embedded ap­pli­ca­tions and can prove the absence of [[stack overflow]]. The analysis re­sults are valid for all inputs and each task ex­e­cution.<ref name=SAE>{{cite journal
StackAnalyzer determines the maximum stack usage of the tasks in embedded applications and can prove the absence of [[stack overflow]]. The analysis results are valid for all inputs and each task execution.<ref name=SAE>{{cite journal
| first1 = Christian
| first1 = Christian
| last1 = Ferdinand
| last1 = Ferdinand
Line 93: Line 92:
| journal = SAE 2006 Transactions Journal of Passenger Cars — Electronic and Electrical Systems
| journal = SAE 2006 Transactions Journal of Passenger Cars — Electronic and Electrical Systems
| volume = 9
| volume = 9
| issue =
| year = 2007
| year = 2007
| doi = 10.4271/2006-01-1499| series = SAE Technical Paper Series
| pages=
| doi = }}</ref> StackAnalyzer is used in the Aerospace, Medical, Telecom and Transportation industries.
}}</ref> StackAnalyzer is used in the Aerospace, Medical, Telecom and Transportation industries.


[[Astrée (static analysis)|Astrée]] is a static pro­gram analyzer that proves the absence of run-time errors in safety-critical embedded ap­pli­cations written or automatically generated in [[C programming language|C]].<ref name=ERTS>{{cite journal
[[Astrée (static analysis)|Astrée]] is a static program analyzer that proves the absence of run-time errors in safety-critical embedded applications written or automatically generated in [[C programming language|C]].<ref name=ERTS2010>{{cite conference
| first1 = D.
| first1 = D.
| last1 = Kästner
| last1 = Kästner
Line 117: Line 115:
| first9 = X.
| first9 = X.
| last9 = Rival
| last9 = Rival
| displayauthors = 2
| display-authors = 2
| title = Astrée: Proving the Absence of Runtime Errors
| title = Astrée: Proving the Absence of Runtime Errors
| journal = Embedded Real Time Software and Systems Congress ERTS², Toulouse
| conference = Embedded Real Time Software and Systems Congress ERTS², Toulouse
| volume =
| issue =
| year = 2010
| year = 2010
⚫
}}</ref> It is used in the Defense/Aerospace, Medical, Industrial Control, Electronic, Telecom/Datacom and Transportation industries. Astrée originates from the group of [[Patrick Cousot]] at [[CNRS]]/[[École Normale Supérieure|ENS]] and is developed and distributed by AbsInt under license from the CNRS/ENS. In the 6th Static Analysis Tool Exposition (SATE VI) <ref>[https://samate.nist.gov/SATE6OckhamCriteria.html SATE VI Ockham Sound Analysis Criteria]</ref> of [[NIST]] (2020), Astrée was confirmed to satisfy the SATE VI Ockham Sound Analysis Criteria.<ref>{{cite report
| pages=
| first1 = Paul
⚫
| doi = }}</ref> It is used in the Defense/Aerospace, Medical, Industrial Control, Electronic, Telecom/Datacom and Transportation industries. Astrée originates from the group of [[Patrick Cousot]] at [[CNRS]]/[[École Normale Supérieure|ENS]] and is developed and distributed by AbsInt under license from the CNRS/ENS.
| last1 = Black
| first2 = Kanwardeep
| last2 = Walia
| title = NISTIR8304 -- SATE VI Ockham Sound Analysis Criteria
| publisher = US National Institute of Standards and Technology (NIST)
| year = 2020
| doi = 10.6028/NIST.IR.8304
| doi-access = free
⚫
}}</ref>


RuleChecker is a static program analyzer that automatically checks C/[[C++]] code for compliance with coding guidelines including [[MISRA C]]/C++, [[SEI CERT C]], [[Common Weakness Enumeration|CWE]], [[List_of_ISO_standards_16000–17999|ISO/IEC TS 17961:2013]], and Adaptive Autosar C++ Coding Guidelines.
⚫
==History==


TimeWeaver is a hybrid [[worst-case execution time|WCET]] analysis tool that combines static path analysis and static value analysis with non-intrusive real-time instruction-level tracing to bound the worst-case execution time ([[worst-case execution time|WCET]]). This approach works for a wide range of modern high-performance ([[multi-core]]) processors.
⚫
AbsInt is a 1998 spin-off from the Department for Programming Languages and Compilers at the [[Saarland University]], where its founders had developed a generic and generative framework for binary-level static program analyzers and optimizers. An important component of this framework is the Program Analyzer Generator PAG, which allows to automatically generate static analyzers from a mathematical specification of the abstract domains and transfer functions.<ref name=PAG>{{cite journal

[[CompCert]] is a formally verified optimizing C [[compiler]]. Its intended use is the compilation of safety-critical and mission-critical software written in C and meeting high levels of assurance. It produces machine code for the [[PowerPC]], [[ARM architecture family|ARM]] and [[AArch64]], [[IA32]] ([[x86]] [[32-bit]]), [[AMD64]], and [[RISC-V]] (32- and [[64-bit]]) architectures. Since 2015 AbsInt offers commercial licenses, provides industrial-strength support and maintenance, and contributes to the advancement of the tool. For the development of CompCert, [[Xavier Leroy]] and the development team of CompCert received the 2021 [[ACM Software System Award]].

⚫
==History==
⚫
AbsInt is a 1998 spin-off from the Department for Programming Languages and Compilers at the [[Saarland University]], where its founders had developed a generic and generative framework for binary-level static program analyzers and optimizers. An important component of this framework is the Program Analyzer Generator PAG, which allows to automatically generate static analyzers from a mathematical specification of the abstract domains and transfer functions.<ref name=PAG>{{cite journal
| first1 = Martin
| first1 = Martin
| last1 = Alt
| last1 = Alt
Line 139: Line 149:
| year = 1995
| year = 1995
| pages=33–50
| pages=33–50
| doi = 10.1007/3-540-60360-3_31| citeseerx = 10.1.1.37.9598
| doi = }}</ref> The first version of PAG was released in 1995. With PAG/WWW, a free academic version of PAG is available which has been used worldwide in numerous teaching courses.
}}</ref> The first version of PAG was released in 1995. With PAG/WWW, a free academic version of PAG is available which has been used worldwide in numerous teaching courses.


In 2001 the StackAnalyzer product line for static [[Stack (abstract data type)|stack usage]] analysis was launched, followed by the aiT WCET Analyzer product line in 2002. In 2003, only half a year after its launch, aiT was awarded a European Information Society Technology Prize for "groundbreaking products that represent the best of European innovation in information society technologies". In 2004, aiT was used to analyze the flight-control software of the Airbus A380, the world's largest passenger aircraft.<ref name=A380>{{cite journal
In 2001, the StackAnalyzer product line for static [[Stack (abstract data type)|stack usage]] analysis was launched, followed by the aiT WCET Analyzer product line in 2002. In 2004, only half a year after its launch, aiT was awarded a European Information Society Technology Prize <ref>[https://web.archive.org/web/20071116120620/http://www.ict-prize.org/winners/list.html?year=2004 ict-prize.org in web.archive.org], retrieved on 29.09.2023</ref> for "groundbreaking products that represent the best of European innovation in information society technologies". In 2004, aiT was used to analyze the flight-control software of the [[Airbus A380]], the world's largest passenger aircraft.<ref name=A380>{{cite conference
| first1 = Jean
| first1 = Jean
| last1 = Souyris
| last1 = Souyris
Line 155: Line 166:
| last6 = Heckmann
| last6 = Heckmann
| title = Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation
| title = Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation
| journal = Proceedings of the 5th International Workshop on Worst-case Execution Time (WCET '05), Mallorca, Spain
| conference = Proceedings of the 5th International Workshop on Worst-case Execution Time (WCET '05), Mallorca, Spain
| volume =
| issue =
| year = 2005
| year = 2005
| pages=21–24
| pages=21–24
| doi = }}</ref> In 2006, the Analyzers successfully passed the first [[Worst-case_execution_time#WCET_Tool_Challenge|WCET Tool Challenge]] carried out by the University of Mälardalen (citation). In 2010, aiT and StackAnalyzer were integrated into SCADE Suite from [[Esterel Technologies]], making it the first embedded-software development environment worldwide to feature WCET and stack analysis at the model level.<ref name=ERTS>{{cite journal
}}</ref> In 2006, the Analyzers successfully passed the first [[Worst-case execution time#WCET Tool Challenge|WCET Tool Challenge]] carried out by [[Mälardalen University]] {{citation needed|date=September 2024}}. In 2010, aiT and StackAnalyzer were integrated into SCADE Suite from [[Esterel Technologies]], making it the first embedded-software development environment worldwide to feature WCET and stack analysis at the model level.<ref name=ERTS08>{{cite conference
| first1 = C.
| first1 = C.
| last1 = Ferdinand
| last1 = Ferdinand
Line 176: Line 185:
| last7 = Martin
| last7 = Martin
| title = Combining a High-Level Design Tool for Safety-Critical Systems with a Tool for WCET Analysis on Executables
| title = Combining a High-Level Design Tool for Safety-Critical Systems with a Tool for WCET Analysis on Executables
| journal = 4th European Congress ERTS — Embedded Real Time Software, Toulouse
| conference = 4th European Congress ERTS — Embedded Real Time Software, Toulouse
| volume =
| issue =
| year = 2008
| year = 2008
}}</ref>
| pages=
⚫
| doi = }}</ref>


The development of Astrée started from scratch in November 2001 by Prof. [[Patrick Cousot]] at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by [[INRIA]] (Paris-Rocquencourt). Astrée stands for ''Analyseur statique de logiciels temps-réel embarqués'' ("real-time embedded software static analyzer"). It has been used successfully on the flight control software of the AIRBUS A340 and A380,<ref name=ASTREE>{{cite journal
The development of Astrée started from scratch in November 2001 by Prof. [[Patrick Cousot]] at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by [[INRIA]] (Paris-Rocquencourt). Astrée stands for ''Analyseur statique de logiciels temps-réel embarqués'' ("real-time embedded software static analyzer"). It has been used successfully on the flight control software of the AIRBUS A340 and A380,<ref name=ASTREE>{{cite journal
| first1 = D.
| first1 = D.
| last1 = Delmas
| last1 = Delmas
Line 191: Line 197:
| journal = Proceedings of the 14th Intl. Static Analysis Symposium (SAS'07), Kongens Lyngby, Denmark
| journal = Proceedings of the 14th Intl. Static Analysis Symposium (SAS'07), Kongens Lyngby, Denmark
| volume = Lecture Notes for Computer Science 4634, Springer
| volume = Lecture Notes for Computer Science 4634, Springer
| issue =
| year = 2007
| year = 2007
| pages=437–451
| pages=437–451
| doi = }}</ref> where it raised no false alarms, even for complex computations involving floating-point numbers. In April 2008, Astrée was able to prove the absence of any runtime error in a C version of the automatic docking software of the [[Jules Verne Automated Transfer Vehicle]] (ATV) used for transporting payloads to the [[International Space Station]].<ref name=SPACESOFT>{{cite journal
}}</ref> where it raised no false alarms, even for complex computations involving floating-point numbers. In April 2008, Astrée was able to prove the absence of any runtime error in a C version of the automatic docking software of the [[Jules Verne Automated Transfer Vehicle]] (ATV) used for transporting payloads to the [[International Space Station]].<ref name=SPACESOFT>{{cite conference
| first1 = O.
| first1 = O.
| last1 = Bouissou
| last1 = Bouissou
Line 221: Line 226:
| first13 = M.
| first13 = M.
| last13 = Turin
| last13 = Turin
| displayauthors = 2
| display-authors = 2
| title = Space software validation using Abstract Interpretation
| title = Space software validation using Abstract Interpretation
| journal = Proceedings of 13th Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey
| conference = Proceedings of 13th Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey
| volume =
| issue =
| year = 2009
| year = 2009
⚫
}}</ref> Since 2009 Astrée is commercially available from AbsInt under license from ENS/CNRS.
| pages=
⚫
| doi = }}</ref> Since 2009 Astrée is commercially available from AbsInt under license from ENS/CNRS.


AbsInt has participated in many research projects funded by the [[European Commission]] and the [[BMBF|German Ministry of Education and Research]], such as DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, and others.
AbsInt has participated in many research projects funded by the [[European Commission]] and the [[BMBF|German Ministry of Education and Research]], such as DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, and others.


The name AbsInt is derived from [[abstract interpretation]], a semantics-based methodology for [[static program analysis]].
The name AbsInt is derived from [[abstract interpretation]], a semantics-based methodology for [[static program analysis]].<ref name=CousotCoust77>{{cite conference
| first1 = Patrick
| last1 = Cousot
| first2 = Radhia
| last2 = Cousot
| title = Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
| conference = Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
| year = 1977
⚫
| pages=238–252
}}</ref>


==References==
==References==
{{reflist}}
{{Reflist|30em}}


==External links==
==External links==
*{{Official website|www.absint.com}}
{{Portal|Software Testing}}
*[http://www.absint.com/ AbsInt website]


{{DEFAULTSORT:Absint}}
{{DEFAULTSORT:Absint}}
[[Category:Static program analysis tools]]
[[Category:Static program analysis tools]]
[[Category:Software companies based in Saarbrücken]]
[[Category:Software companies of Germany]]
[[Category:Companies based in Saarbrücken]]
[[Category:Companies based in Saarland]]
[[Category:Software companies established in 1998]]

Latest revision as of 18:28, 23 September 2024

AbsInt Angewandte Informatik GmbH
Company typeGesellschaft mit beschränkter Haftung
IndustrySoftware Verification Tools
Founded1998; 26 years ago (1998)
Headquarters
Saarbrücken
,
Germany
Key people
Founders: Christian Ferdinand, Daniel Kästner, Marc Langenbach, Florian Martin, Stephan Thesing, and Reinhard Wilhelm
ProductsaiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver
Websitewww.absint.com

AbsInt is a software-development tools vendor based in Saarbrücken, Germany. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of Prof. Reinhard Wilhelm at Saarland University. AbsInt specializes in software-verification tools based on abstract interpretation.[1] Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.

Products

[edit]

aiT WCET Analyzer statically computes safe upper bounds for the worst-case execution time[2] of tasks in real-time systems. It directly analyzes binary executables and takes the intrinsic cache and pipeline behavior of the microprocessor into account.[3] The U.S. National Highway Traffic Safety Administration (NHTSA) and NASA used it in its Study on Sudden Unintended Acceleration in the electronic throttle control systems of Toyota vehicles.[4]

StackAnalyzer determines the maximum stack usage of the tasks in embedded applications and can prove the absence of stack overflow. The analysis results are valid for all inputs and each task execution.[5] StackAnalyzer is used in the Aerospace, Medical, Telecom and Transportation industries.

Astrée is a static program analyzer that proves the absence of run-time errors in safety-critical embedded applications written or automatically generated in C.[6] It is used in the Defense/Aerospace, Medical, Industrial Control, Electronic, Telecom/Datacom and Transportation industries. Astrée originates from the group of Patrick Cousot at CNRS/ENS and is developed and distributed by AbsInt under license from the CNRS/ENS. In the 6th Static Analysis Tool Exposition (SATE VI) [7] of NIST (2020), Astrée was confirmed to satisfy the SATE VI Ockham Sound Analysis Criteria.[8]

RuleChecker is a static program analyzer that automatically checks C/C++ code for compliance with coding guidelines including MISRA C/C++, SEI CERT C, CWE, ISO/IEC TS 17961:2013, and Adaptive Autosar C++ Coding Guidelines.

TimeWeaver is a hybrid WCET analysis tool that combines static path analysis and static value analysis with non-intrusive real-time instruction-level tracing to bound the worst-case execution time (WCET). This approach works for a wide range of modern high-performance (multi-core) processors.

CompCert is a formally verified optimizing C compiler. Its intended use is the compilation of safety-critical and mission-critical software written in C and meeting high levels of assurance. It produces machine code for the PowerPC, ARM and AArch64, IA32 (x86 32-bit), AMD64, and RISC-V (32- and 64-bit) architectures. Since 2015 AbsInt offers commercial licenses, provides industrial-strength support and maintenance, and contributes to the advancement of the tool. For the development of CompCert, Xavier Leroy and the development team of CompCert received the 2021 ACM Software System Award.

History

[edit]

AbsInt is a 1998 spin-off from the Department for Programming Languages and Compilers at the Saarland University, where its founders had developed a generic and generative framework for binary-level static program analyzers and optimizers. An important component of this framework is the Program Analyzer Generator PAG, which allows to automatically generate static analyzers from a mathematical specification of the abstract domains and transfer functions.[9] The first version of PAG was released in 1995. With PAG/WWW, a free academic version of PAG is available which has been used worldwide in numerous teaching courses.

In 2001, the StackAnalyzer product line for static stack usage analysis was launched, followed by the aiT WCET Analyzer product line in 2002. In 2004, only half a year after its launch, aiT was awarded a European Information Society Technology Prize [10] for "groundbreaking products that represent the best of European innovation in information society technologies". In 2004, aiT was used to analyze the flight-control software of the Airbus A380, the world's largest passenger aircraft.[11] In 2006, the Analyzers successfully passed the first WCET Tool Challenge carried out by Mälardalen University [citation needed]. In 2010, aiT and StackAnalyzer were integrated into SCADE Suite from Esterel Technologies, making it the first embedded-software development environment worldwide to feature WCET and stack analysis at the model level.[12]

The development of Astrée started from scratch in November 2001 by Prof. Patrick Cousot at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by INRIA (Paris-Rocquencourt). Astrée stands for Analyseur statique de logiciels temps-réel embarqués ("real-time embedded software static analyzer"). It has been used successfully on the flight control software of the AIRBUS A340 and A380,[13] where it raised no false alarms, even for complex computations involving floating-point numbers. In April 2008, Astrée was able to prove the absence of any runtime error in a C version of the automatic docking software of the Jules Verne Automated Transfer Vehicle (ATV) used for transporting payloads to the International Space Station.[14] Since 2009 Astrée is commercially available from AbsInt under license from ENS/CNRS.

AbsInt has participated in many research projects funded by the European Commission and the German Ministry of Education and Research, such as DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT, and others.

The name AbsInt is derived from abstract interpretation, a semantics-based methodology for static program analysis.[15]

References

[edit]
  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. S2CID 2139310.
  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. S2CID 28282721.
  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. ^ SATE VI Ockham Sound Analysis Criteria
  8. ^ Black, Paul; Walia, Kanwardeep (2020). NISTIR8304 -- SATE VI Ockham Sound Analysis Criteria (Report). US National Institute of Standards and Technology (NIST). doi:10.6028/NIST.IR.8304.
  9. ^ 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.
  10. ^ ict-prize.org in web.archive.org, retrieved on 29.09.2023
  11. ^ 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.
  12. ^ 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.
  13. ^ 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.
  14. ^ Bouissou, O.; Conquet, E.; et al. (2009). Space software validation using Abstract Interpretation. Proceedings of 13th Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey.
  15. ^ Cousot, Patrick; Cousot, Radhia (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 238–252.
[edit]
Retrieved from "https://en.wikipedia.org/enwiki/w/index.php?title=AbsInt&oldid=1247301673"