Economics essay No FPGA board result in this paper

ثمن الواجهة غير المفحوصة

ما تكلّفه أعطال الواجهات، باستخدام الأرقام التي يذكرها مصدر أولي فقط، وكل رقم موسوم بأنه تكلفة محاسبية أو تقدير نموذج أو تقدير مسح.

David Charlot, Open Interface Engineering

هذه ترجمة للنسخة الإنجليزية. عند أي اختلاف، تكون النسخة الإنجليزية هي المرجع. الأصل الإنجليزي.

Research studies, not journal finals. Notation is defined in the paper. Analytical energy estimates are not board power. Interactive figures live under /living/. Shared terms: glossary.

Cite this

David Charlot, Open Interface Engineering. ثمن الواجهة غير المفحوصة. Open Interface Engineering. Web: https://research.openie.dev/papers/interface-economics/. PDF: https://research.openie.dev/pdfs/interface-economics.pdf.

الإصدار 1.0، 11 أكتوبر 2026. ملف LaTeX PDF: /pdfs/latex/interface-economics.pdf (المصدر).

الملخص

يجمع هذا المقال التكاليف المنشورة للأعطال التي تقع عند مواضع التسليم بين أجزاء النظام، ويسم كل رقم بحسب الطريقة التي أُنتج بها. ولا يجمعها في مجموع واحد.

بكلمات بسيطة

  1. لبعض الأعطال عند مواضع التسليم ثمن محدد بدقة، مثل مسبار مريخي مفقود كلّف مئات الملايين من الدولارات.
  2. الأرقام الوطنية الأكبر تقديرات مستمدة من مسوح ونماذج، ولا يعدّ أي منها أعطال التسليم وحدها.
  3. تدوين ما يفترضه كل طرف والتحقق منه رخيص، لكن من يقوم به يدفع الثمن بينما يستفيد الجميع، ولذلك يغلب ألا يُنجز.

0. التعريفات والنطاق

الواجهة موضع تسليم يصبح عنده ناتج طرف مدخلًا لطرف آخر: من الذين يحددون ما ينبغي للنظام أن يفعله (المنظّرون)، إلى الذين يبنونه (الصانعون)، إلى الذين يشغّلونه (المستخدمون)، أو بين مستويين من مكدس برمجي وعتادي. وافتراض الواجهة شرط على القيم التي تعبر موضع التسليم يعتمد عليه الجانب المستقبِل لصحة عمله هو، مثل وحدة قياس أو نطاق أو نوع أو إصدار أو غلاف تشغيل. ويكون الافتراض غير مفحوص حين يُعتمد عليه دون أن يُدوَّن أو يُتحقق منه. وتحدد أدبيات هندسية طويلة، من Garlan وAllen وOckerbloom في عدم التوافق المعماري إلى Leveson في الحوادث بوصفها أعطال تفاعل، موضع كثير من أعطال الأنظمة في مثل هذه الافتراضات [19, 20]. يسأل هذا المقال عن تكلفة تلك الأعطال، ولا يجيب إلا بأرقام يذكرها مصدر أولي. ويُوسم كل رقم بنوعه. التكلفة المحاسبية هي ما تعلن وكالة أو شركة أنها أنفقته أو خسرته فعلًا. وتقدير النموذج رقم تنتجه طريقة معلنة من مسوح أو مقابلات أو بيانات ثانوية. والإسقاط قول عن المستقبل. ولا تُجمع الأنواع الثلاثة معًا.

والتكاليف المحاسبية لأعطال الواجهات المنفردة كبيرة ومحددة: فقد كلّف مشروع Mars Surveyor 1998، الذي ضمّ Mars Climate Orbiter، مبلغ $327.6 مليون [1]، ووافقت ESA على 214 مليون ECU لاستعادة مهمة Cluster التي فُقدت مع أول صاروخ Ariane 5 [4]. أما تقديرات النماذج فأكبر وأوسع: فقد قدّر NIST التكلفة السنوية لبنية تحتية غير كافية لاختبار البرمجيات في الولايات المتحدة بمبلغ $59.5 مليار [6]، وتكلفة قصور التشغيل البيني في قطاع المنشآت الرأسمالية الأمريكي بمبلغ $15.8 مليار سنويًا [7]. وقدّر CISQ تكلفة رداءة جودة البرمجيات في الولايات المتحدة بما لا يقل عن $2.41 تريليون في عام 2022، والدين التقني المتراكم بنحو $1.52 تريليون [8]. لا يقيس أي من هذه الأرقام عطل الواجهة وحده. لكن كلًّا منها يتضمنه.

1. أنواع الأرقام

تنتقل الادعاءات الاقتصادية عن أعطال البرمجيات في ثلاث صور تتشابه في المظهر وليست متماثلة. ميزانية المشروع سجل محاسبي. والتقدير الوطني للتكلفة ناتج نموذج مدخلاته مسوح ودراسات حالة وافتراضات عن الحجم. والتنبؤ ليس هذا ولا ذاك. ويتبع هذا المقال قاعدة واحدة: يحمل كل رقم نوعه ومصدره وما يعدّه فعلًا.

وتُتداول أرقام لتكلفة “عطل الواجهة” بوصفها مجموعًا سنويًا واحدًا دون طريقة معلنة. ولا يعزل أي من التقديرات الأولية في القسم 3 الواجهات، ولذلك لا يردّها هذا المقال إلى أي مجموع واحد.

2. أعطال منفردة، بتكاليف محاسبية

Mars Climate Orbiter. كانت الواجهة وحدة قياس: بيانات دفعة المحركات الدافعة بوحدة رطل قوة ثانية قُرئت على أنها بوحدة نيوتن ثانية [2]. وتذكر صحيفة وقائع المشروع لدى NASA أن تكلفة مشروع Mars Surveyor 1998 بلغت $327.6 مليون للمسبار المداري ومسبار الهبوط Mars Polar Lander معًا: $193.1 مليون لتطوير المركبات الفضائية، و$91.7 مليون للإطلاق، و$42.8 مليون للتشغيل [1]. وذكرت التقارير المعاصرة أن المسبار المداري وحده مركبة فضائية قيمتها $125 مليون [3]. النوع: تكلفة محاسبية للمشروع، مع رقم مُبلَّغ عنه للمركبة الواحدة.

Ariane 501 وCluster. كانت الواجهة غلاف تشغيل: افترض برنامج أُعيد استخدامه من Ariane 4 نطاقًا للسرعة الأفقية تجاوزه الصاروخ الجديد [5]. وفُقدت أقمار Cluster الأربعة. وتسجّل رواية ESA لعملية الاستعادة الخيارات التي سعّرتها لجنة برنامجها العلمي في عام 1996، ومنها 351 مليون وحدة حسابية لإعادة بناء الأقمار الأربعة وفق التصميم الأصلي، ووافقت ESA في عام 1997 على مهمة استعادة، Cluster II، بتكلفة 214 مليون ECU [4, 17]. النوع: تكلفة محاسبية للاستعادة التي اختارتها ESA، وهي حدّ أدنى للخسارة، لا قيمة الأقمار ولا قيمة العلم الذي تأخر.

وتحدد هاتان الحالتان بنية المشكلة. في كل منهما أدّت كل جهة عملها، ووقعت التكلفة عند الواجهة. وفي كل منهما كان الفحص الذي كان سيكشف عدم التوافق رخيصًا قياسًا إلى الخسارة. ولا يمكن تكبير أي من الحالتين إلى رقم وطني، لأن الحوادث المنفردة ليست عيّنة.

3. تقديرات وطنية، منمذجة

مخطط أعمدة على محور دولار لوغاريتمي للتقديرات الأولية المذكورة في هذا المقال، ملوّنة بحسب النوع. التكاليف المحاسبية: مشروع Mars Surveyor 1998 بمبلغ 327.6 مليون دولار واستعادة Cluster II بمبلغ 214 مليون ECU. تقديرات النماذج: NIST 2004 لقصور التشغيل البيني في المنشآت الرأسمالية الأمريكية بمبلغ 15.8 مليار دولار سنويًا؛ وNIST 2002 لقصور البنية التحتية لاختبار البرمجيات بمبلغ 59.5 مليار دولار سنويًا؛ وStripe 2018 لوقت المطورين المصروف على الشيفرة الرديئة بنحو 85 مليار دولار سنويًا؛ وCISQ 2022 للدين التقني بنحو 1.52 تريليون دولار متراكمة؛ وCISQ 2022 لتكلفة رداءة جودة البرمجيات في الولايات المتحدة بما لا يقل عن 2.41 تريليون دولار في عام 2022.
الشكل 1. التقديرات بحسب النوع. شكل بيانات، محور لوغاريتمي. القيم كما طبعتها المصادر [1, 4, 6, 7, 8, 9]. الأعمدة غير قابلة للجمع: يتضمن مجموع CISQ فئات تتداخل مع أرقام NIST وStripe، ورُسم رصيد (الدين التقني) إلى جانب تدفقات سنوية. وتتوفر نسخة PNG. Open full size · PNG

اختبار البرمجيات، NIST 2002. قدّرت RTI International، لصالح NIST، أن بنية تحتية غير كافية لاختبار البرمجيات كلّفت الاقتصاد الأمريكي ما بين $22.2 مليار و$59.5 مليار سنويًا، على أن الرقم الأعلى هو التكلفة الكلية والرقم الأدنى هو الجزء الذي يمكن للتحسينات الممكنة أن تزيله [6]. وجمعت الطريقة بين مسوح للمطورين والمستخدمين في قطاعين، تصنيع معدات النقل والخدمات المالية، وبين استقراء إلى الاقتصاد الوطني. النوع: تقدير نموذج.

التشغيل البيني، NIST 2004. قدّر Gallaher وزملاؤه، لصالح NIST، تكلفة قصور التشغيل البيني في قطاع المنشآت الرأسمالية الأمريكي بمبلغ $15.8 مليار سنويًا، استنادًا إلى مقابلات ومسوح شملت الملاك والمشغلين والمعماريين والمهندسين والمقاولين [7]. والتشغيل البيني هنا هو القدرة على تبادل بيانات التصميم والتشغيل واستخدامها عبر الأنظمة البرمجية، وهو واجهة بالمعنى المحدد في الملخص. ويذكر التقرير أن رقمه يُغفل تكاليف لم يتمكن من قياسها كميًا. النوع: تقدير نموذج، لقطاع واحد، مقدَّم على أنه متحفظ.

رداءة جودة البرمجيات، CISQ 2022. قدّر Consortium for Information and Software Quality أن تكلفة رداءة جودة البرمجيات في الولايات المتحدة ارتفعت إلى ما لا يقل عن $2.41 تريليون في عام 2022، وأن الدين التقني المتراكم ارتفع إلى نحو $1.52 تريليون [8]. ويبني التقرير المجموع من فئات، هي الأعطال التشغيلية والمشروعات غير الناجحة ومشكلات الأنظمة القديمة وخسائر الجرائم الإلكترونية المنسوبة إلى ثغرات البرمجيات، ويستمد كثيرًا من مدخلاته من مصادر ثانوية؛ ويوزّع مكوّن الجرائم الإلكترونية فيه حصة من توقع عالمي على الولايات المتحدة [8]. النوع: تقدير نموذج مبني جزئيًا على تقديرات أخرى. وهو أكبر رقم موثق في هذا المجال، وهو رقم لجودة البرمجيات ككل، لا للواجهات.

وقت المطورين، Stripe 2018. أفاد مسح أجرته Stripe مع Harris Poll بأن المطورين يقضون نحو 17.3 ساعة أسبوعيًا في أعمال الصيانة مثل تصحيح الأخطاء وإعادة الهيكلة، ونحو أربع ساعات أسبوعيًا على “الشيفرة الرديئة”، وهو ما يقدّر التقرير قيمته بقرابة $85 مليار سنويًا على مستوى العالم [9]. النوع: تقدير قائم على مسح.

ما تشترك فيه هذه الأرقام بنية، لا مجموع. فكل منها يعدّ تكلفة افتراض اعتُمد عليه ولم يُتحقق منه: مسار لم يُختبر، وصيغة بيانات لا تنتقل سليمة، وثغرة عند حدّ فاصل، ونظام قديم لا يستطيع أحد أن يعيد صياغة عقوده. وعدم التوافق الذي لا يُفحص حيث ينشأ يمرّ بوصفه مدخلًا سليم البنية إلى كل مستوى فوقه، فتظهر تكلفته بعيدًا عن سببه، كما في حل الملاحة لمسبار Mars Climate Orbiter، الذي كان متسقًا داخليًا وخاطئًا [2]. ولهذا أيضًا يجب أن تُنمذج التقديرات الوطنية بدل أن تُعدّ.

4. الدين التقني حساب واجهات

قدّم Cunningham مفهوم الدين التقني في عام 1992 بوصفه تكلفة شحن شيفرة لا تطابق بنيتها بعدُ ما تعلّمه الفريق، مع فوائد تُدفع عند كل تغيير لاحق إلى أن يُسدَّد الدين [10]. وبيّن Sculley وزملاؤه أن معظم ذلك الدين في أنظمة تعلّم الآلة يقع خارج النموذج، في شيفرة الربط والتهيئة واعتماديات البيانات والمستهلكين غير المصرَّح بهم [11]. وبالمصطلحات المحددة أعلاه، فإن كثيرًا من الدين التقني رصيدٌ من افتراضات الواجهة غير المفحوصة مقيّد في الدفاتر، وفائدته هي التكلفة التي يفرضها عدم توافق لم يُتحقق منه على كل مستوى فوقه، في كل تشغيل.

وتقدير CISQ لنحو $1.52 تريليون من الدين التقني المتراكم في الولايات المتحدة رصيدٌ، مقيس بتكلفة الإصلاح [8]. أما الأرقام السنوية في القسم 3 فتدفقات. والنتيجة الاقتصادية فرضية، تُختبر في القسم 7: قد يكلّف فحص يُدفع مرة واحدة عند حدّ فاصل، على امتداد حمل عمل، أقل من عطل يُدفع ثمنه مجددًا عند كل مستوى يبلغه.

5. المعايير هي الطريقة التي تغلق بها الأسواق الواجهات

درس الاقتصاديون مشكلة الواجهة منذ عقود تحت اسم آخر: التوافقية. فقد بيّن Katz وShapiro أنه حين ترتفع قيمة منتج مع عدد المستخدمين الذين يمكنه العمل معهم، فإن حوافز الشركات لأن تكون متوافقة تعتمد على حجمها وموقعها، وقد توفّر السوق قدرًا أقل مما ينبغي من التوافقية [12]. وبيّن Farrell وSaloner أن السوق قد تبقى عالقة عند معيار قديم، أو تنتقل إلى معيار جديد بسرعة مفرطة، لأن اختيار كل مستخدم يعتمد على ما يختاره الآخرون [13]. وجعل تاريخ David للوحة مفاتيح QWERTY الاعتماد على المسار أمرًا ملموسًا [14]. وبيّن Baldwin وClark أن قواعد التصميم، أي الواجهات المرئية المحددة مسبقًا، هي ما يتيح للصناعات النمطية أن تتشكل أصلًا [15]. ولخّصت مراجعة Swann للحكومة البريطانية الأدلة على أن المعايير تسهم في الإنتاجية والتجارة [16].

والخيط المشترك أن الواجهة منفعة عامة ذات تكاليف خاصة. فتدوين الافتراض والتحقق منه يفيد كل طرف يعبر الحدّ الفاصل، لكن من يتولى التدوين هو من يدفع ثمنه. ولكل طرف سبب لاعتبار التسليم عمل شخص آخر. وهيئات التقييس والجهات التنظيمية ومالكو المنصات هم المؤسسات التي دفعت هذه التكلفة تاريخيًا. والتمثيلات التي تفحصها الآلة، مثل الأنواع التي تحمل وحدات القياس أو المواصفات الصورية التي يفحصها فاحص نماذج [21, 22]، تخفض التكلفة الخاصة لإغلاق الواجهة نحو تكلفة تشغيل فحصها.

6. الشيفرة المولَّدة تعبر الواجهات نفسها

الشيفرة التي ينتجها مولّد آلي تعبر الحدود الفاصلة نفسها التي تعبرها الشيفرة المكتوبة يدويًا: بين مواصفة وتنفيذ، وبين مكتبة ومستخدميها، وبين البرمجيات وعقد التعليمات الذي تحتها. ويحمل كل عبور افتراضات لا يتحقق منها المولّد ما لم يُبنَ لذلك. ولذلك تتصل أرقام القسم 3 بالتوليد الآلي للشيفرة أيضًا. فإذا كانت حصة كبيرة من تكلفة رداءة جودة البرمجيات هي تكلفة افتراضات لم يُتحقق منها عند الحدود الفاصلة، فقد تتجاوز قيمة إغلاق الواجهات قيمة كتابة الشيفرة بسرعة أكبر. هذه فرضية عن موضع القيمة، لا قياس. والبروتوكولات في القسم 7 هي سبيل قياسها.

7. القضايا والبروتوكولات

القضية E1 (حصة الواجهة). في مجموعة من أعطال البرمجيات ذات التكاليف المحاسبية، تتجاوز حصة التكلفة التي سببها افتراض واجهة منتهَك، بالمعنى المحدد في الملخص، الحصة التي يقع سببها كليًا داخل جهة واحدة.

البروتوكول. خذ مجموعة عامة من الحوادث تتضمن حقولًا للتكلفة، مثل تقارير الحوادث لدى الوكالات أو الإيداعات التنظيمية. يصنّف مرمّزان كل سبب على أنه سبب واجهة أو سبب داخلي باستخدام التعريفات الواردة في الملخص، دون اطلاع على التكلفة. أبلغ عن حصة الواجهة الموزونة بالتكلفة مع فترة bootstrap، وعن درجة اتفاق المرمّزين.

القضية E2 (الفحوص تؤتي ثمارها). لحمل عمل ثابت، تكون تكلفة إضافة فحص صريح عند واجهة أقل من التكلفة المتوقعة للأعطال التي يرفضها، مجموعةً على كل مستوى كان العطل سيبلغه لولا ذلك. وصوريًا، لواجهة تُعبر مرة، لتكن تكلفة فحص واحد بالدولار، و احتمال أن ينتهك عبورٌ الافتراض، و التكلفة بالدولار التي يفرضها انتهاك غير مكتشف عند المستوى من المستويات التي يبلغها. يؤتي الفحص ثماره حين ، أي حين . ولدى الحالتين المحاسبيتين في القسم 2 قيمة من رتبة دولار، ولذلك يتحقق الشرط لأي فحص تقل تكلفته عن دولار لكل عبور.

البروتوكول. على نظام معروفة تكاليف تشغيل مستوياته، احقن انتهاكًا لكل افتراض واجهة مسجّل على مجموعة ثابتة من البذور، مع تسجيل تكلفة كل فحص وتكلفة كل انتهاك غير مكتشف حيث يقع. أبلغ عن كلتيهما بالجول وبالدولار بسعر معلن.

القضية E3 (إغلاق الواجهة يخفض تكلفتها الخاصة). حين يكون افتراض الواجهة جزءًا من تمثيل مشترك ويُفحص بالبناء، تنخفض تكلفة إغلاقه على طرف واحد نحو تكلفة تشغيل الفحص.

البروتوكول. اختر تسليمًا حقيقيًا بين مؤسسات، مثل مواصفة تُسلَّم إلى منفّذ. انقله في ذراع بوصفه توثيقًا نثريًا، وفي الذراع الأخرى بوصفه تمثيلًا تفحصه الآلة. سجّل ساعات العمل على جانبي التسليم والأعطال الواقعة عند الواجهة في كل ذراع، مع فترات Wilson بنسبة 95%.

8. الخاتمة

تكلفة الواجهات غير المفحوصة حقيقية وكبيرة وسيئة القياس. يمكن تسعير الأعطال المنفردة بدقة، وهي تُظهر أن الخسارة تقع عند حدّ فاصل ظنّت كل جهة أنه يخص غيرها. والتقديرات الوطنية نماذج، وأكبرها يصف جودة البرمجيات ككل. لا يذكر أي مصدر أولي تكلفة عطل الواجهة وحده، ولا يقدّم هذا المقال رقمًا لها. وما تدعمه الأدلة بنية: تكاليف تنشأ عند الحدود الفاصلة، وتنتشر صعودًا وتتراكم دينًا، في أسواق توفّر أقل مما ينبغي من المنفعة العامة المتمثلة في واجهة مفحوصة. وتبيّن قضايا القسم 7 كيف يمكن اختبار هذه البنية.

المراجع

[1] NASA Jet Propulsion Laboratory, “Mars Climate Orbiter Fact Sheet,” Mars Surveyor 1998 project. Archived copy: https://web.archive.org/web/20121003073752/http://mars.jpl.nasa.gov/msp98/orbiter/fact.html

[2] Mars Climate Orbiter Mishap Investigation Board, Phase I Report. NASA, 10 November 1999. https://llis.nasa.gov/llis_lib/pdf/1009464main1_0641-mr.pdf

[3] A. Pollack, “Two Teams, Two Measures Equaled One Lost Spacecraft,” The New York Times, 1 October 1999. https://archive.nytimes.com/www.nytimes.com/library/national/science/100199sci-nasa-mars.html

[4] European Space Agency, “Cluster will fly again!,” press release N° 12 1997, 26 March 1997. https://www.esa.int/Newsroom/Press_Releases/Cluster_will_fly_again

[5] J. L. Lions (chair), Ariane 5 Flight 501 Failure: Report by the Inquiry Board. European Space Agency, 19 July 1996. https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf

[6] RTI International for the National Institute of Standards and Technology, The Economic Impacts of Inadequate Infrastructure for Software Testing, Planning Report 02-3, May 2002. https://www.nist.gov/system/files/documents/director/planning/report02-3.pdf

[7] M. P. Gallaher, A. C. O’Connor, J. L. Dettbarn and L. T. Gilday, Cost Analysis of Inadequate Interoperability in the U.S. Capital Facilities Industry, NIST GCR 04-867, 2004. doi:10.6028/NIST.GCR.04-867

[8] H. Krasner, The Cost of Poor Software Quality in the US: A 2022 Report. Consortium for Information and Software Quality, 2022. https://www.it-cisq.org/the-cost-of-poor-quality-software-in-the-us-a-2022-report/

[9] Stripe, The Developer Coefficient, with Harris Poll, September 2018. https://stripe.com/files/reports/the-developer-coefficient.pdf

[10] W. Cunningham, “The WyCash portfolio management system,” OOPSLA 1992 Addendum, ACM SIGPLAN OOPS Messenger 4(2), 1993, pp. 29 to 30. doi:10.1145/157710.157715

[11] D. Sculley, G. Holt, D. Golovin, E. Davydov, T. Phillips, D. Ebner, V. Chaudhary, M. Young, J.-F. Crespo and D. Dennison, “Hidden Technical Debt in Machine Learning Systems,” Advances in Neural Information Processing Systems 28, 2015. https://papers.nips.cc/paper_files/paper/2015/hash/86df7dcfd896fcaf2674f757a2463eba-Abstract.html

[12] M. L. Katz and C. Shapiro, “Network Externalities, Competition, and Compatibility,” American Economic Review 75(3), June 1985, pp. 424 to 440. RePEc:aea:aecrev:v:75:y:1985:i:3:p:424-40. https://www.jstor.org/stable/1814809

[13] J. Farrell and G. Saloner, “Standardization, Compatibility, and Innovation,” RAND Journal of Economics 16(1), 1985, pp. 70 to 83. doi:10.2307/2555589

[14] P. A. David, “Clio and the Economics of QWERTY,” American Economic Review 75(2), Papers and Proceedings, May 1985, pp. 332 to 337. RePEc:aea:aecrev:v:75:y:1985:i:2:p:332-37. https://www.jstor.org/stable/1805621

[15] C. Y. Baldwin and K. B. Clark, Design Rules, Volume 1: The Power of Modularity. MIT Press, 2000. doi:10.7551/mitpress/2366.001.0001

[16] G. M. P. Swann, The Economics of Standardization: An Update. Report for the UK Department for Business, Innovation and Skills, 2010. https://www.gov.uk/government/publications/economics-of-standardisation-update-to-report

[17] European Space Agency, “The Resurrection of the Cluster Scientific Mission,” ESA Bulletin 91, 1997. https://www.esa.int/esapub/bulletin/bullet91/b91cred.htm

[19] D. Garlan, R. Allen and J. Ockerbloom, “Architectural mismatch: why reuse is so hard,” IEEE Software 12(6), 1995, pp. 17 to 26. doi:10.1109/52.469757

[20] N. G. Leveson, Engineering a Safer World: Systems Thinking Applied to Safety. MIT Press, 2012. doi:10.7551/mitpress/8179.001.0001

[21] A. Kennedy, “Types for Units-of-Measure: Theory and Practice,” in Central European Functional Programming School, Lecture Notes in Computer Science 6299, Springer, 2010, pp. 268 to 305. doi:10.1007/978-3-642-17685-2_8

[22] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker and M. Deardeuff, “How Amazon Web Services uses formal methods,” Communications of the ACM 58(4), 2015, pp. 66 to 73. doi:10.1145/2699417