AbsInt

📅 آخر تحديث: ١٨ يوليو ٢٠٢٦
✍️ نُشر في: ١٨ يوليو ٢٠٢٦
الموسوعة الحرة

شركة AbsInt هي شركة متخصصة في أدوات تطوير البرمجيات، مقرها في ساربروكن ، ألمانيا . تأسست الشركة عام 1998 كشركة تقنية منبثقة عن قسم لغات البرمجة وبناء المترجمات التابع للبروفيسور راينهارد فيلهلم في جامعة سارلاند . تتخصص AbsInt في أدوات التحقق من البرمجيات القائمة على التفسير المجرد . [ 1 ] تُستخدم أدواتها عالميًا من قبل شركات مدرجة ضمن قائمة Fortune 500، ومؤسسات تعليمية، وهيئات حكومية، وشركات ناشئة.

منتجات

يحسب محلل aiT WCET بشكل ثابت الحدود العليا الآمنة لوقت التنفيذ في أسوأ الحالات [ 2 ] للمهام في الأنظمة الآنية . ويحلل مباشرةً الملفات التنفيذية الثنائية، ويأخذ في الحسبان سلوك الذاكرة المؤقتة وخطوط الأنابيب الخاصة بالمعالج الدقيق . [ 3 ] وقد استخدمته الإدارة الوطنية الأمريكية لسلامة المرور على الطرق السريعة (NHTSA) ووكالة ناسا في دراستهما حول التسارع المفاجئ غير المقصود في أنظمة التحكم الإلكتروني في دواسة الوقود لسيارات تويوتا. [ 4 ]

يُحدد برنامج StackAnalyzer الحد الأقصى لاستخدام الذاكرة المخصصة للمهام في التطبيقات المدمجة، ويمكنه إثبات عدم وجود تجاوز في سعة الذاكرة المخصصة . وتكون نتائج التحليل صالحة لجميع المدخلات ولكل عملية تنفيذ. [ 5 ] يُستخدم برنامج StackAnalyzer في قطاعات الطيران والفضاء، والطب، والاتصالات، والنقل.

أستري هو محلل برامج ثابت يثبت خلو التطبيقات المدمجة الحساسة للسلامة، سواءً كانت مكتوبة بلغة C أو مُولّدة تلقائيًا، من أخطاء وقت التشغيل . [ 6 ] يُستخدم في قطاعات الدفاع/الفضاء، والطب، والتحكم الصناعي، والإلكترونيات، والاتصالات/نقل البيانات، والنقل. نشأ أستري من مجموعة باتريك كوسو في المركز الوطني الفرنسي للبحث العلمي / المدرسة العليا للأساتذة ، ويتم تطويره وتوزيعه بواسطة شركة AbsInt بموجب ترخيص من المركز الوطني الفرنسي للبحث العلمي/المدرسة العليا للأساتذة. في معرض أدوات التحليل الثابت السادس (SATE VI) [ 7 ] الذي نظمه المعهد الوطني للمعايير والتكنولوجيا (NIST ) عام 2020، تم تأكيد استيفاء أستري لمعايير أوكام لتحليل الصوت. [ 8 ]

RuleChecker هو محلل برامج ثابت يقوم تلقائيًا بفحص كود C/ C++ للتأكد من امتثاله لإرشادات البرمجة بما في ذلك MISRA C /C++ و SEI CERT C و CWE و ISO/IEC TS 17961:2013 وإرشادات البرمجة التكيفية Autosar C++.

TimeWeaver هي أداة تحليل هجينة لوقت التنفيذ في أسوأ الحالات (WCET) ، تجمع بين تحليل المسار الثابت وتحليل القيمة الثابتة مع تتبع غير تدخلي على مستوى التعليمات في الوقت الحقيقي لتحديد الحد الأقصى لوقت التنفيذ في أسوأ الحالات ( WCET ). هذا النهج فعال مع مجموعة واسعة من المعالجات الحديثة عالية الأداء ( متعددة النوى ).

CompCert هو مُجمِّع C مُحسَّن ومُدقَّق رسميًا . يُستخدم لتجميع البرامج بالغة الأهمية للسلامة والمهام المكتوبة بلغة C والتي تستوفي معايير ضمان عالية. يُنتج CompCert شفرة الآلة لبنى PowerPC و ARM و AArch64 و IA32 ( x86 32 بت ) و AMD64 و RISC-V (32 و 64 بت ). منذ عام 2015، تُقدِّم AbsInt تراخيص تجارية، وتُوفِّر دعمًا وصيانةً على مستوى عالٍ، وتُساهم في تطوير الأداة. وقد حصل كزافييه ليروي وفريق تطوير CompCert على جائزة ACM لأنظمة البرمجيات لعام 2021 تقديرًا لتطويرهم CompCert .

تاريخ

AbsInt هي شركة منبثقة عن قسم لغات البرمجة والمترجمات في جامعة سارلاند عام 1998 ، حيث طور مؤسسوها إطار عمل عامًا وتوليديًا لمحللات ومحسّنات البرامج الثابتة على مستوى الملفات الثنائية. يُعد مولد محللات البرامج (PAG) مكونًا أساسيًا في هذا الإطار، إذ يسمح بتوليد محللات ثابتة تلقائيًا من مواصفات رياضية للمجالات المجردة ووظائف النقل. [ 9 ] صدرت النسخة الأولى من PAG عام 1995. يتوفر الآن إصدار أكاديمي مجاني من PAG، وهو PAG/WWW، والذي يُستخدم عالميًا في العديد من الدورات التعليمية.

في عام 2001، أُطلقت سلسلة منتجات StackAnalyzer لتحليل استخدام الذاكرة الثابتة ، تلتها سلسلة منتجات aiT WCET Analyzer في عام 2002. وفي عام 2004، وبعد ستة أشهر فقط من إطلاقها، حازت aiT على جائزة تكنولوجيا مجتمع المعلومات الأوروبية [ 10 ] لمنتجاتها الرائدة التي تُمثل أفضل ما توصلت إليه الابتكارات الأوروبية في تقنيات مجتمع المعلومات. وفي عام 2004، استُخدمت aiT لتحليل برمجيات التحكم في الطيران لطائرة إيرباص A380 ، أكبر طائرة ركاب في العالم. [ 11 ] وفي عام 2006، اجتازت أدوات التحليل بنجاح أول تحدٍّ لأدوات WCET أجرته جامعة مالاردالن . وفي عام 2010، دُمجت aiT وStackAnalyzer في SCADE Suite من Esterel Technologies ، مما جعلها أول بيئة تطوير برمجيات مضمنة في العالم تُتيح تحليل WCET وتحليل الذاكرة على مستوى النموذج. [ 12 ]

بدأ تطوير Astrée من الصفر في نوفمبر 2001 على يد البروفيسور باتريك كوزوت في مختبر المعلوماتية التابع للمدرسة العليا للأساتذة (LIENS)، بدعم مبدئي من مشروع ASTRÉE، والمركز الوطني للبحث العلمي، والمدرسة العليا للأساتذة، ومنذ سبتمبر 2007، من INRIA (باريس روكينكور). Astrée هو اختصار لـ Analyseur statique de logiciels temps-réel embarqués ("محلل ثابت للبرامج المضمنة في الوقت الحقيقي"). وقد تم استخدامه بنجاح في برنامج التحكم في الطيران لطائرات إيرباص A340 وA380، [ 13 ] حيث لم يصدر أي إنذارات كاذبة، حتى بالنسبة للحسابات المعقدة التي تتضمن أرقام الفاصلة العائمة. في أبريل 2008، تمكن أستري من إثبات عدم وجود أي خطأ أثناء التشغيل في نسخة C من برنامج الالتحام التلقائي لمركبة النقل الآلية جول فيرن (ATV) المستخدمة لنقل الحمولات إلى محطة الفضاء الدولية . [ 14 ] منذ عام 2009، أصبح أستري متاحًا تجاريًا من شركة AbsInt بموجب ترخيص من ENS/CNRS.

شاركت شركة AbsInt في العديد من المشاريع البحثية الممولة من قبل المفوضية الأوروبية ووزارة التعليم والبحث الألمانية ، مثل DAEDALUS وARTIST وSuReal وASTEC وALL-TIMES وInterested وVerisoft وPREDATOR وTIMMO2USE وMBAT وغيرها.

اسم AbsInt مشتق من التفسير المجرد ، وهي منهجية قائمة على الدلالات لتحليل البرامج الثابتة . [ 15 ]

مراجع

  1. ↑ كاستنر، د.؛ فرديناند، س. (2011). التحقق الفعال من خصائص السلامة غير الوظيفية عن طريق التفسير المجرد: التوقيت، واستهلاك المكدس، وعدم وجود أخطاء وقت التشغيل . وقائع المؤتمر الدولي التاسع والعشرين لسلامة الأنظمة ISSC2011 لاس فيغاس.
  2. ↑ فيلهلم، راينهارد؛ إنجبلوم، جاكوب؛ إرميدال، أندرياس؛ هولستي، نيكلاس؛ ثيسينغ، ستيفان؛ والي، ديفيد؛ بيرنات، غيليم؛ فرديناند، كريستيان؛ هيكمان، راينهولد؛ ميترا، توليكا؛ مولر، فرانك؛ بووت، إيزابيل؛ بوشنر، بيتر؛ ستاشولات، يان؛ ستينستروم، بير (2008). "مشكلة أسوأ حالة لوقت التنفيذ - نظرة عامة على الأساليب ومسح للأدوات". معاملات ACM لأنظمة الحوسبة المدمجة . 7 (3): 1-53 . CiteSeerX 10.1.1.458.3540 . doi : 10.1145/1347375.1347389 . S2CID 2139310 .  
  3. ↑ فرديناند، كريستيان؛ ويلهلم، راينهارد (1999). "التنبؤ السريع والفعال بسلوك ذاكرة التخزين المؤقت لأنظمة الوقت الحقيقي". أنظمة الوقت الحقيقي . 17 ( 2-3 ): 131-181 . doi : 10.1023/a:1008186323068 . S2CID 28282721 . 
  4. ↑ ناسا (18 يناير 2011). الدعم الفني للإدارة الوطنية لسلامة المرور على الطرق السريعة (NHTSA) بشأن التحقيق في التسارع غير المقصود (UA) لشركة تويوتا موتور (TMC) (تقرير فني). ص 151. 
  5. ↑ فرديناند، كريستيان؛ هيكمان، راينهولد (2007). "تحليل الذاكرة الثابتة ووقت تنفيذ التعليمات البرمجية المضمنة". مجلة معاملات SAE لعام 2006 لسيارات الركاب - الأنظمة الإلكترونية والكهربائية . سلسلة أوراق SAE التقنية. 9 2006-01-1499. doi : 10.4271/2006-01-1499 .
  6. ↑ كاستنر، د.؛ فيلهلم، س.؛ وآخرون . (2010). أستري: إثبات عدم وجود أخطاء وقت التشغيل . مؤتمر البرمجيات والأنظمة المضمنة في الوقت الحقيقي ERTS²، تولوز. 
  7. ↑ معايير تحليل الصوت أوكام SATE VI
  8. ↑ بلاك، بول؛ واليا، كانوارديب (2020). NISTIR8304 - معايير تحليل الصوت أوكام SATE VI (تقرير). المعهد الوطني الأمريكي للمعايير والتكنولوجيا (NIST). doi : 10.6028/NIST.IR.8304 .
  9. ↑ آلت، مارتن؛ مارتن، فلوريان (1995). "توليد محللات فعّالة بين الإجراءات باستخدام PAG". وقائع الندوة الدولية الثانية حول التحليل الثابت (SAS '95) . سلسلة محاضرات في علوم الحاسوب (983): 33-50 . CiteSeerX 10.1.1.37.9598 . doi : 10.1007/3-540-60360-3_31 . 
  10. ↑ ict-prize.org في web.archive.org ، تم استرجاعه بتاريخ 29/09/2023
  11. ↑ سويريس، جان؛ لو بافيك، إرفان؛ هيمبرت، غيوم؛ جيغو، فيكتور؛ بوريوس، غيوم؛ هيكمان، راينهولد (2005). حساب أسوأ وقت تنفيذ لبرنامج إلكترونيات الطيران عن طريق التفسير المجرد . وقائع ورشة العمل الدولية الخامسة حول أسوأ وقت تنفيذ (WCET '05)، مايوركا، إسبانيا. الصفحات 21-24 . 
  12. ↑ فرديناند، سي.؛ هيكمان، ر.؛ لو سيرجنت، ت.؛ لوبيز، د.؛ مارتن، ب.؛ فورناري، إكس.؛ مارتن، ف. (2008). دمج أداة تصميم عالية المستوى للأنظمة الحساسة للسلامة مع أداة لتحليل أسوأ وقت تنفيذ على الملفات التنفيذية . المؤتمر الأوروبي الرابع ERTS - برمجيات الوقت الحقيقي المضمنة، تولوز.
  13. ↑ ديلماس، د.؛ سويريس، ج. (2007). "ASTRÉE: من البحث إلى الصناعة". وقائع الندوة الدولية الرابعة عشرة للتحليل الثابت (SAS'07)، كونغنس لينغبي، الدنمارك . سلسلة محاضرات في علوم الحاسوب 4634، سبرينغر: 437-451 .
  14. ↑ بويسو، أ.؛ كونكيه، إ.؛ وآخرون (2009). التحقق من صحة برمجيات الفضاء باستخدام التفسير المجرد . وقائع المؤتمر الثالث عشر لأنظمة البيانات في مجال الطيران والفضاء، DASIA 2009، إسطنبول، تركيا. 
  15. ↑ كوسو، باتريك؛ كوسو، راديا (1977). التفسير المجرد: نموذج شبكي موحد للتحليل الثابت للبرامج عن طريق بناء أو تقريب النقاط الثابتة . الندوة السنوية الرابعة لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة. الصفحات 238-252 .