تطبيق أساليب التحقق من صحة النموذج الرسمي لواجهة المستخدم

مرحبا يا هبر! أقدم إليكم ترجمة مقالة "تحديد مواصفات UIS" بقلم هيليل واين.

من المؤلف

نسبيا ، صادفت مقالا عن الأساليب الهندسية في تطوير البرمجيات ، حيث تحدث vasil-sd عن التحقق الرسمي من المواصفات لمنتجات البرمجيات التي يتم إنشاؤها. تم استخدام سبيكة مجموعة أدوات. كان أحد العناصر المهيمنة الرئيسية في التعليقات هو تحليل المقال في سياق بعض مشاريع الويب الحديثة ، لأنه مكلف / طويل \ يصعب استخدام طرق رسمية حيث يفعل الجميع بسرعة / بثمن بخس. نظرًا لأن المؤلف أشار إلى مدونة Hillel Wayne ، حيث كانت هذه الأمثلة ، فقد قررت ترجمة بعض مقالاته كإضافة إلى النص الرئيسي لـ vasil-sd

تحذير :

• كل ما يسميه المؤلف بجهاز الحالة المحدودة ، سأتصل بجهاز دولة أو نموذج لجهاز دولة.
• لقد تعلمت بعض المصطلحات من مقال ذكرته سابقًا حول مقاربة هندسية للتنمية. ومع ذلك ، فإن الموضوع بالنسبة لي جديد نسبياً ، لأن كلا المؤلفين (سواء الأجانب وغيرهم) لم يفهموا ذلك - لا أقسم.

مواصفات واجهة المستخدم الرسمية

واجهة المستخدم الجيدة ضرورية لإنشاء البرنامج المناسب. وإذا واجه المستخدمون مشاكل في استخدام البرنامج ، فمن المحتمل أن يقوموا بشيء خاطئ. أفضل عدم العمل على واجهة المستخدم - لا أعتبر نفسي أعلى من ذلك ، لكنه "ليس لي". المؤثرات البصرية والواجهات تسبب لي القلق ، والأشخاص القادرين على التعامل مع كل هذا يسبب لي احتراما مجنونا.

أنا أحب الأساليب الرسمية. صديقي كيفن ليناغ صدر مؤخرا sketch.systems ¹ ، أداة مواصفات رسمية جديدة لمصممي واجهة المستخدم. حسنًا ، دعنا نكتشف ذلك - هل يمكن أن يتغلب حبي على الطرق الرسمية على خوفي؟

المشكلة

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

في Snapshot ، يمكن للمدرسين إجراء "استطلاعات" أو "مقتطفات" بين الطلاب. علاوة على ذلك ، يجمع البرنامج نتائج الاستطلاع ويزود المعلمين بالعديد من التقارير في الوقت الحقيقي في الأقسام التالية: تقرير "الملخص" ، "الطلاب" و "حسب المعايير". بالإضافة إلى ذلك ، قررنا أن يتضمن البرنامج تقرير "إجابات" يمكن فتحه من تقرير "الطلاب" والذي يوفر معلومات حول الإجابات غير الصحيحة.

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

عندما يبدأ النظام في التعقيد ، نحتاج إلى توخي الحذر. هذا يعني كتابة المواصفات. فكيف يمكننا تحديد هذا؟ أرى أن المعلم يمكن أن يكون على شاشة محددة للتطبيق ويمكنه اتخاذ إجراءات للانتقال إلى شاشة أخرى. هذا يقودني إلى فكرة أنه يمكننا اعتبار تصرفات المعلم كآلة حالة محدودة.

آلات الدولة

آلات الحالة المحدودة (FSMs) هي واحدة من أبسط النماذج الرياضية لنظرية الأتمتة المجردة. لديك مجموعة محدودة من الحالات ، ومجموعة من التحولات بين الحالات ، ومجموعة من الأحداث (مشغلات) التي تؤدي إلى انتقالات. يرتبط كل انتقال بحدث ، لذلك إذا حدث الحدث ، قد تتغير الحالة. ³ في نموذجنا ، ستكون الأحداث "يضغط المعلم على الأزرار". وفيما يلي نموذج لآلة الحالة لنظامنا الحالي:


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

1. إذا كنت في تقرير ملخص ، فلن يظهر زر الملخص أو لا يفعل شيئًا.
2. إذا كنت في تقرير ملخص ، فإن زر الملخص يعيد ضبط التقرير.

لقد اخترنا الخيار الثاني. كانت حالتنا الأولية عبارة عن تقرير "ملخص".


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

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


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

الرسوم البيانية هاريل الوضع

لدى معظم ولاياتنا منطق مشترك لما يسمى بالوضع الفائق: كل من "تقاريرنا" الأربعة لها نفس المنطق لتسجيل الخروج من النظام ، والثلاثة الرئيسية لها نفس التحولات. إذا استطعنا تجميعها في تقرير "الحالة الأبوية" ، فكل ما تبقى لنا هو تحديد الانتقال إلى "الخروج" وتوزيع هذا الانتقال في الحالات الفرعية. يشبه المنطق الميراث: حالات الطفل ترث (أو تتجاوز) التحولات من الحالات الأم.

تسمى آلات الحالة المحدودة ذات الحالات المتداخلة آلات الحالة الهرمية ، وهناك عدة طرق مختلفة لإضفاء الطابع الرسمي عليها. إن الطريقة الأكثر ملاءمة لكتابة نماذج آلات الحالة لواجهة المستخدم هي Harel Statechart. ⁴ قواعد لها هي كما يلي:

1. جميع حالات الوالدين مجردة. يجب أن تحدد كل حالة أصل حالة تابعة افتراضية.
2. الحالات الفرعية ترث جميع التحولات الأصل تلقائيًا ، ولكن يمكنها أيضًا تجاوزها.
3. قد يشير الانتقال إلى أي ولاية. إذا قمت بالتبديل إلى الحالة الأصل ، فانتقل بدلاً من ذلك إلى حالته الفرعية الافتراضية. إذا كانت الدولة الفرعية هي أحد الوالدين ، فيتم تحديد الحالة بشكل متكرر.

يمكنك تطوير Harel State Charts في Graphviz وتتعجب من العديد من الرؤوس والحواف والمسرات من الرسوم البيانية الرسومية في كل مرة. سنستخدم واجهة المستخدم الأكثر جمالًا من Sketch.systems:

Snapshot logout -> Login Page Reports summary -> Summary students -> Students standards -> Standards Summary* Students answer -> Answers Standards Answers close -> Students Login Page login -> Snapshot 

_مصدر

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

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


_مصدر

من الناحية المثالية ، سيكون من الجيد رؤية مثل هذه المشكلات بوضوح على الرسم التخطيطي ، مما يعني بعض أتمتة التحقق من النموذج.

تفتيش

مواصفات رسمية لها ميزتان. أحدهما ضمني: العمل على إضفاء الطابع الرسمي يؤدي إلى فهم أفضل للنظام. الآخر واضح: إذا كان لدينا مواصفات رسمية ، فيمكننا التحقق من خصائصها. هل لدينا واجهة المستخدم لديها أي الجمود؟ هل هناك انتقالات ضمنية أو محددة بشكل غير صحيح؟

يمكن لـ Sketch.systems التحقق مما إذا كان لدى Harel State Diagram التنسيق الصحيح ، لكن لا يمكنه التحقق من سلوك النموذج. هناك أدوات أخرى لتحديد حالة جهاز الحالة ، ولا سيما مخططات حالة UML ، ولكن كلها تركز على مواصفات مستوى الرمز ، وليس على مواصفات مستوى النظام. هدفهم هو في النهاية إنشاء رمز C أو Java من مخطط حالة. لكنها منخفضة المستوى للغاية لاختبار الخصائص المجردة ، ونحن على مستوى عالٍ للغاية لا نريد إنشاء الشفرة. إذا كنا نريد اختبارًا رسميًا ، فسوف نحتاج إلى وصف نموذجنا بلغة مواصفات للأغراض العامة.

لحسن الحظ ، من السهل جدًا القيام بهذه الحالة. لهذا ، سوف نستخدم سبائك ، لأنه يمكن أن يعكس بدقة أكثر دقة مخطط هاريل ستيت. ⁵ يمكننا استخدام امتدادات التوقيع لتمثيل الحالات المتداخلة: "تمدد" "المعايير" تعني "التقارير" أن كل جزء من "المعايير" هو أيضًا "تقرير" ، وهو ما يعادل العبارة التي تشير إلى أن هذه حالة تابعة في مخطط هاريل المقابل. هذا يبسط تعريف التحولات. يتم تمثيل كل واحد منهم بتقييم واحد يستغرق وقتًا (t) والحالة الأولية (البداية) والحالة النهائية (النهاية) ، ويعلن أن الحالة في الوقت t تنتقل من البداية إلى النهاية لـ t.next. على الرغم من أن حالات الوالدين مجردة ، فلا يزال بإمكاننا استخدامها كنقطة بداية والاستفادة من انتقالات الوالدين.

 open util/ordering[Time] sig Time { state: one State } abstract sig State {} abstract sig Login extends State {} abstract sig Reports extends Login {} one sig Logout extends State {} one sig Students, Summary, Standards extends Reports {} one sig Answers extends Login {} pred transition[t: Time, start: State, end: State] { t.state in start t.next.state in end } pred logout[t: Time] { transition[t, Login, Logout] } pred login[t: Time] { transition[t, Logout, Summary] } pred students[t: Time] { transition[t, Reports, Students] } pred summary[t: Time] { transition[t, Reports, Summary] } pred standards[t: Time] { transition[t, Reports, Standards] } pred answers[t: Time] { transition[t, Students, Answers] } pred close_answers[t: Time] { transition[t, Answers, Students] } fact Trace { first.state = Summary all t: Time - last | logout[t] or login[t] or students[t] or summary[t] or standards[t] or answers[t] or close_answers[t] } 

الآن يمكننا التحقق من خصائص نموذجنا. على سبيل المثال ، هل من الممكن الحصول على تقرير "الإجابات" دون الاطلاع على تقرير "الطلاب"؟

 check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7 // valid 

يمكننا أيضًا محاكاة مثال عندما يقوم شخص ما بتسجيل الخروج بتسجيل الدخول مرة أخرى:

 run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7 

توفر سبائك مجموعة واسعة إلى حد ما من المواصفات. مع التحقق من خصائص معينة ، على سبيل المثال ، tupiokov ، قد تنشأ صعوبات. ومع ذلك ، أنا لست أول شخص يرى مدى عمل سبيكة مع الرسوم البيانية للدولة. أعلنت الأستاذة نانسي داي مؤخرًا عن مجموعة متنوعة من السبائك تسمى DASH ، والتي تضيف دلالات الدرجة الأولى من Harel Diagrams إلى Alloy. يمكنك أن تقرأ عنها هنا .

قيمة

هل كل هذا له قيمة؟ ما الذي يجعل مخطط الحالة التفاعلية أفضل من الملاحظات باللغة الإنجليزية فقط؟ بالتأكيد ، يصبح digram أكثر قيمة عند القياس. أتذكر أنه في مشروع Snapshot ، كان هناك حوالي 24 شاشة للمعلمين متداخلة في عدة تدرجات هرمية كبيرة. بدون مواصفات رسمية ، لم نتمكن من اختبار عملنا. بقدر ما أتذكر ، بعض الأخطاء التي ارتكبناها:

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

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

استنتاج

ناقشنا المواصفات الرسمية لتفاعل المستخدم مع واجهة المستخدم. هل يستطيع حبي الأساليب الرسمية التغلب على خوفي من واجهة المستخدم؟ يا الهي لا. إذا اتبعت الارتباطات الخاصة بـ Sketch.systems ، فربما ترى أنه يمكنك إرفاق نموذج أولي في Javascript بمخطط الحالة الخاص بك. هذا هو السحر!

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

بالمناسبة ، مهلا ، أنصح بالأساليب الرسمية . أخبر رئيسك!

---

1. تحذير ، كنت واحدا من الخلاف ألفا. كان معظم تعليقاتي مثل "يجب أن تجعل الأمر أكثر تعقيدًا!". نعم ، أنا اختبار ألفا. ^[عودة]
2. في عام 2017 ، كسبوا 1 مليون وخسروا 20 مليون. ^[عودة]
3. تشترك آلة الحالة المحدودة كثيرًا مع آلة الحالة النهائية الحتمية ، والتي تعد مكونًا مهمًا في علوم الكمبيوتر. الفارق الرئيسي في مجال التطبيق: استخدام آلة الحالة المحدودة الحتمية له ما يبرره "مجموعة من اللغات العادية التي يتعرف عليها" ، واستخدام آلة الحالة المحدودة عن طريق "تناسق المواصفات" ^[عودة]
4. المنافس الرئيسي هو مخطط ولاية UML ، الذي يمثل أساسًا مخطط Harer State Diagram ، المكمل بمواصفات الكود. هو أكثر تعبيرا ، ولكن من الصعب تحليلها. ^[عودة]
5. إذا لم تكن معتادًا على السبائك ، فقد كتبت عدة مقالات حوله هنا وهنا .