AbsInt：嵌入式系统静态分析与安全验证工具

"Absint是一家专注于提供高级开发工具和安全相关软件验证服务的公司，主要服务于航空航天、汽车、能源、轨道交通和医疗设备等行业。该公司提供的关键产品包括静态分析解决方案，如aiTWCETAnalyzer用于确定最差情况运行时间上限，Timeweaver结合动态数采进行最差情况运行时间分析，TimingProfiler进行静态执行时间估计，StackAnalyzer分析最大栈用量以防溢出，以及CompCert和Astrée等工具分别用于C语言优化编译和错误检测。此外，RuleChecker则用于检查C语言代码是否符合MISRA和CERT等标准。随着行业对功能安全性和代码质量的要求日益提高，Absint的产品和服务对于降低开发成本和减少软件瑕疵导致的问题具有重要意义。" Absint是一家德国公司，成立于1998年，其主要业务是为嵌入式系统提供高级开发工具，特别关注于安全相关的软件验证、确认和认证。Absint的产品线涵盖多个方面，旨在帮助客户确保软件的安全性和可靠性。例如，aiTWCETAnalyzer是一个关键工具，它能够分析并确定程序在最坏情况下的运行时间上限，这对于满足安全关键系统的时间约束至关重要。Timeweaver结合了动态数据采集技术，进一步增强了这种时间分析能力。 另一款名为TimingProfiler的工具提供了静态最差情况执行时间估计，并且可以持续反馈这些估计如何受到代码更改的影响。StackAnalyzer则是用来防止栈溢出，通过分析确定最大的栈使用量上限。在编译器领域，CompCert是一个经过形式验证的C语言优化编译器，保证了编译过程的正确性。而Astrée则是一个强大的C语言代码检查工具，能够检测到各种运行时错误，如数据竞争和死锁。 为了确保代码遵循行业标准，RuleChecker提供了对C语言代码的规则检查，支持MISRA和CERT等编码规范。这些工具的应用对于应对当前汽车、航空航天等行业的挑战至关重要，如功能复杂性的增加、代码量的爆炸式增长以及电子/电气系统在成本中的占比增大。 软件瑕疵带来的成本是巨大的，不仅包括开发延误和项目取消，还有可能引发事故赔偿、产品召回甚至法律诉讼。据统计，80%的软件问题集中于代码的20%部分，因此，通过Absint提供的早期静态分析工具，可以在设计阶段就发现和解决问题，显著降低修复成本。这凸显了Absint产品和服务在现代软件开发流程中的价值和重要性。