Geekly articles weekly

Penerapan metode validasi model formal untuk UI

Halo, Habr! Saya mempersembahkan bagi Anda terjemahan artikel “FORMALLY SPECIFYING UIS” oleh Hillel Wayne.


Dari penulis


Baru-baru ini, saya menemukan sebuah artikel tentang metode Rekayasa dalam pengembangan perangkat lunak , di mana vasil-sd berbicara tentang validasi formal spesifikasi untuk produk perangkat lunak yang sedang dibuat. Paduan digunakan sebagai toolkit. Salah satu leitmotif utama dalam komentar adalah mengurai artikel dalam konteks beberapa proyek web modern, karena mahal \ lama \ sulit untuk menggunakan metode formal di mana setiap orang melakukannya dengan cepat / murah. Karena penulis merujuk ke blog Hillel Wayne, di mana contoh-contoh seperti itu, saya memutuskan untuk menerjemahkan beberapa artikelnya sebagai tambahan pada teks utama vasil-sd

Peringatan :

  • Segala sesuatu yang penulis sebut mesin negara-terbatas, saya akan memanggil mesin negara atau model mesin negara.
  • Saya belajar beberapa terminologi dari sebuah artikel yang saya sebutkan sebelumnya tentang pendekatan rekayasa untuk pengembangan. Namun demikian, topik bagi saya relatif baru, karena kedua penulis (baik asing maupun tidak) bisa mengerti tidak begitu - jangan bersumpah.

Spesifikasi UI Formal


Antarmuka pengguna yang baik sangat penting untuk membuat perangkat lunak yang tepat. Dan jika pengguna memiliki masalah dalam menggunakan program ini, mereka cenderung melakukan sesuatu yang salah. Saya lebih suka untuk tidak bekerja pada antarmuka pengguna - saya tidak menganggap diri saya di atas ini, tapi itu "bukan milikku". Efek visual dan antarmuka membuat saya prihatin, dan orang-orang yang mampu mengatasi semua ini membuat saya sangat respek.

Saya suka metode formal. Teman saya Kevin Lynagh baru-baru ini merilis sketch.systems 1 , alat spesifikasi formal baru untuk desainer UI. Baiklah, mari kita cari tahu - dapatkah kecintaan saya pada metode formal mengatasi ketakutan saya?

Masalah


Kembali di Edmodo, saya sedang mengerjakan antarmuka pengguna untuk aplikasi Snapshot kami. Ini adalah usaha kedua kami yang pertama untuk menghasilkan uang: kami mulai dengan memberi semua guru program gratis, dan kemudian meminta sumbangan atau sesuatu seperti itu. Seperti yang Anda lihat, maka Edmodo tidak berbeda ketajaman bisnis. 2

Di Snapshot, guru dapat melakukan "polling" atau "buncis" di antara siswa. Lebih lanjut, program ini mengumpulkan hasil survei dan memberi para guru beberapa laporan waktu nyata di bagian berikut ini: laporan “ringkasan”, “oleh siswa” dan “menurut standar”. Selain itu, kami memutuskan bahwa program harus memiliki laporan "jawaban" yang dapat dibuka dari laporan "siswa" dan yang menyediakan informasi tentang jawaban yang salah.

KAMI membayangkan bahwa pengguna bergerak di antara laporan dengan menekan tombol yang diperlukan, dan bahwa semua laporan harus dapat diakses dari laporan lain, dengan pengecualian jawaban. Arti kata "tersedia" dalam konteks transisi agak kabur: itu bisa berarti "Anda bisa pergi ke laporan", atau itu bisa berarti "satu klik langsung ke laporan yang diinginkan." Segala sesuatu yang dijelaskan di atas hanya sebagian dari pengguna antarmuka seluruh aplikasi, yang, selain navigasi dalam laporan, memiliki sistem navigasi sendiri.

Ketika sistem mulai menjadi lebih rumit, kita harus berhati-hati. Ini berarti menulis spesifikasi. Jadi bagaimana kita menentukan ini? Saya melihat bahwa guru dapat berada di layar aplikasi tertentu dan dapat mengambil tindakan untuk pindah ke layar lain. Ini membawa saya pada gagasan bahwa kita dapat mempertimbangkan tindakan guru sebagai mesin negara yang terbatas.

Mesin negara


Finite state Machines (FSMs) adalah salah satu model matematika paling sederhana dari teori automata abstrak. Anda memiliki serangkaian negara terbatas, satu set transisi antar negara, dan serangkaian peristiwa (pemicu) yang memicu transisi. Setiap transisi terkait dengan suatu peristiwa, jadi jika peristiwa itu terjadi, negara dapat berubah. 3 Dalam model kami, acara akan menjadi "guru menekan tombol." Berikut ini adalah model mesin negara untuk sistem kami saat ini:


Model ini menunjukkan dua masalah dengan antarmuka pengguna kami. Pertama, semua mesin negara terbatas memerlukan kondisi awal, tetapi kami tidak memilikinya. Ketika seorang guru mengunjungi halaman laporan, laporan mana yang harus dia lihat pertama kali? Kedua, kami tidak menunjukkan apa yang terjadi ketika Anda mengklik tombol laporan yang sudah Anda lihat. Ini ambigu, karena ada beberapa perilaku:

  1. Jika Anda berada di laporan ringkasan, tombol ringkasan tidak muncul atau tidak melakukan apa-apa.
  2. Jika Anda berada di laporan ringkasan, tombol ringkasan mengatur ulang laporan.

Kami telah memilih opsi kedua. Keadaan awal kami adalah laporan "ringkasan". Model yang diperbarui:


Model ini sangat akurat menyampaikan antarmuka pengguna kami - juga berantakan. Ini adalah batasan yang signifikan dari model mesin keadaan terbatas: semakin banyak transisi antar negara, semakin sulit untuk melihatnya. Dalam kasus kami, dari hampir setiap laporan, dimungkinkan untuk beralih ke laporan lain.

Pengembangan lebih lanjut dari sistem dan pemodelannya menjadi bermasalah. Karena, misalnya, jika kita memperhitungkan bahwa setiap saat guru dapat keluar dari sistem, maka model mesin negara bagian berikutnya sudah akan terlihat seperti ini:


Untuk menambahkan fungsi logout, kami harus menambahkan empat sisi lagi. Pengembangan spesifikasi lebih lanjut dengan pendekatan ini dengan cepat berhenti menjadi suara. Kami membutuhkan beberapa cara untuk mewakili transisi "umum". Untuk ini kita dapat menggunakan negara-negara bersarang, yang akan menyulitkan formalisme kita, tetapi menyederhanakan spesifikasi kita.

Bagan Status Harel


Sebagian besar negara kita memiliki logika umum dari apa yang disebut negara super: keempat "laporan" kami memiliki logika yang sama untuk keluar dari sistem, dan tiga utama memiliki transisi yang sama. Jika kita dapat mengelompokkannya ke dalam laporan "status orang tua", yang tersisa bagi kita adalah menentukan transisi untuk "keluar" dan mendistribusikan transisi ini di negara anak. Logikanya mirip dengan warisan: status anak mewarisi (atau menimpa) transisi status induk.

Mesin negara terbatas dengan status bersarang disebut mesin negara hierarkis , dan ada beberapa cara berbeda untuk memformalkannya. Cara yang paling cocok untuk menulis model mesin negara untuk UI adalah Harel Statechart. 4 Aturan untuknya adalah sebagai berikut:

  1. Semua status orangtua adalah abstrak. Setiap negara induk harus menetapkan status anak bawaan.
  2. Status anak secara otomatis mewarisi semua transisi orangtua, tetapi juga dapat menimpanya.
  3. Transisi dapat menunjukkan status apa pun. Jika Anda beralih ke status induk, alih-alih pergi ke status bawaan anak. Jika status anak juga merupakan orangtua, maka status tersebut ditentukan secara rekursif.

Anda dapat mengembangkan Harel State Charts di Graphviz dan merasa ngeri di banyak simpul, tepi, dan kelezatan grafik grafik setiap saat. Kami akan menggunakan antarmuka pengguna yang jauh lebih baik dari 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


sumber

Saya akan merekomendasikan mengikuti tautan ke diagram, sebagai dia interaktif. Anda dapat mengklik transisi dan melihat bagaimana kondisi berubah. Ini adalah keuntungan besar Diagram Negara Harkel: mereka tidak hanya formal dan ringkas, tetapi juga kinetik. Anda bisa meneliti mereka.

Saat mempelajari grafik, saya menemukan kesalahan: Anda bisa langsung dari "jawaban" ke "standar". Ini dapat diperbaiki dengan menjadikan "jawaban" sebagai keturunan langsung dari "input" daripada "laporan":


sumber

Idealnya, akan menyenangkan untuk melihat dengan jelas masalah seperti pada diagram, yang menyiratkan beberapa otomatisasi verifikasi model.

Periksa


Spesifikasi formal memiliki dua keunggulan. Salah satunya adalah implisit: bekerja pada formalisasi mengarah pada pemahaman yang lebih baik tentang sistem. Yang lain eksplisit: jika kita memiliki spesifikasi formal, kita dapat memeriksa propertinya. Apakah antarmuka pengguna kami memiliki deadlock? Apakah ada transisi yang ditentukan secara implisit atau tidak tepat?

Sketch.systems dapat memeriksa apakah Diagram Status Harel memiliki format yang benar, tetapi tidak dapat memeriksa perilaku model. Ada alat lain untuk menentukan keadaan mesin negara, khususnya diagram keadaan UML, tetapi semuanya berorientasi pada spesifikasi level kode, dan bukan ke spesifikasi level sistem. Tujuan mereka adalah untuk akhirnya menghasilkan kode C atau Java dari diagram keadaan. Tetapi mereka terlalu rendah untuk menguji sifat abstrak, dan kami terlalu tinggi untuk ingin menghasilkan kode. Jika kita menginginkan tes formal, kita perlu menggambarkan model kita dalam bahasa spesifikasi untuk tujuan umum.

Untungnya, untuk kasus ini cukup mudah dilakukan. Untuk ini, kita akan menggunakan Alloy, karena itu paling akurat dapat mencerminkan struktur Diagram Negara Harel. 5 Kita dapat menggunakan ekstensi tanda tangan untuk mewakili status bersarang: "Standar" memperluas "Laporan" berarti bahwa setiap bit "Standar" juga merupakan "Laporan", yang setara dengan pernyataan bahwa ini adalah keadaan anak dalam Diagram Harel yang sesuai. Ini menyederhanakan definisi transisi. Masing-masing dari mereka diwakili oleh satu predikat tunggal yang membutuhkan waktu (t), keadaan awal (awal) dan keadaan akhir (akhir), dan menyatakan bahwa keadaan pada saat t berubah dari awal ke akhir untuk t.next. Terlepas dari kenyataan bahwa status induk adalah abstrak, kita masih dapat menggunakannya sebagai awal dan memanfaatkan transisi induk.

 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] }

Sekarang kita dapat memeriksa properti model kita. Sebagai contoh, apakah mungkin untuk mendapatkan laporan "jawaban" tanpa melalui laporan "siswa"?

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

Kami juga dapat mensimulasikan contoh ketika seseorang keluar dan masuk lagi:

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

Paduan menyediakan berbagai spesifikasi yang cukup luas. Dengan verifikasi properti tertentu, misalnya, tupiokov, kesulitan mungkin timbul. Namun, saya bukan orang pertama yang melihat seberapa baik Alloy bekerja dengan diagram keadaan. Profesor Nancy Day baru-baru ini mengumumkan varian Alloy yang disebut DASH, yang menambahkan semantik kelas satu Diagram Harel ke Alloy. Anda dapat membacanya di sini .

Nilai


Apakah semua ini memiliki nilai? Apa yang membuat diagram keadaan interaktif lebih baik dari sekadar catatan dalam bahasa Inggris? Jelas, sebuah digram menjadi lebih bernilai saat Anda meningkatkan skala. Saya ingat bahwa dalam proyek Snapshot ada sekitar dua lusin layar guru bersarang di beberapa hierarki besar. Tanpa spesifikasi formal, kami tidak dapat menguji pekerjaan kami. Sejauh yang saya ingat, beberapa kesalahan yang kami lakukan:

  • Kami lupa menganggap "penutupan laporan respons" sebagai peristiwa, dan "respons" menjadi jalan buntu
  • Membuat survei baru memiliki banyak rute daerah yang benar-benar tidak kita butuhkan.
  • Kami tidak menentukan perilaku antarmuka pengguna setelah membuat survei, jadi kami mengembalikan guru ke layar pembuatan survei, ia berpikir bahwa selama kesalahan survei tidak dibuat dan diciptakan kembali
  • Sulit mendapatkan beberapa layar, jadi tidak ada yang pergi ke sana.

Saya pikir memiliki spesifikasi formal akan banyak membantu. Menulis contoh yang saya buat di atas membutuhkan waktu sekitar lima menit untuk ditulis, dan spesifikasi untuk aplikasi lengkap akan memakan waktu kurang dari dua jam. Jika, bahkan pada tahap desain, ini membantu kami menemukan setidaknya satu kesalahan yang terdaftar, kami akan menghemat banyak waktu kemudian.

Kesimpulan


Kami membahas spesifikasi formal interaksi pengguna dengan UI. Dapatkah cinta saya pada metode formal mengatasi rasa takut saya terhadap UI? Astaga tidak. Jika Anda mengikuti tautan ke Sketch.systems, Anda mungkin melihat bahwa Anda dapat melampirkan prototipe dalam Javascript ke diagram keadaan Anda. Ini sihir!

Terlepas dari ketakutan saya, saya pikir ada beberapa potensi dalam metode formal. Orang biasanya menganggapnya sebagai hal akademis murni yang digunakan secara eksklusif oleh NASA. Tema utama blog ini adalah bahwa metode formal adalah alat yang ampuh untuk pekerjaan sehari-hari. Saya terutama mempertimbangkan aplikasi mereka ke sistem backend dan paralel, karena saya menikmatinya. Tetapi penggunaannya tidak terbatas hanya pada preferensi saya. Metode formal sangat penting untuk antarmuka pengguna. Saya tidak berpikir State Diagram Harel sejauh ini merupakan notasi terbaik, tetapi ini adalah langkah pertama yang baik.

Ngomong-ngomong, hei, saya menyarankan metode formal . Beritahu bosmu!


  1. Peringatan, saya adalah salah satu dari alpha testrovers. Sebagian besar tanggapan saya seperti "Anda harus membuatnya lebih rumit!". Ya, saya seorang penguji alfa. [kembali]
  2. Pada 2017, mereka memperoleh 1 juta dan kehilangan 20 juta. [kembali]
  3. Mesin negara terbatas memiliki banyak kesamaan dengan mesin negara terbatas deterministik, yang merupakan komponen penting dari ilmu komputer. Perbedaan utama dalam bidang aplikasi: penggunaan mesin keadaan terbatas deterministik dibenarkan oleh "set bahasa reguler yang dikenali", penggunaan mesin keadaan terbatas oleh "konsistensi spesifikasi" [kembali]
  4. Pesaing utama adalah UML State Diagram, yang pada dasarnya mewakili Harer State Diagram, melengkapi dengan spesifikasi kodenya. Lebih ekspresif, tetapi sulit untuk dianalisis. [kembali]
  5. Jika Anda tidak terbiasa dengan Alloy, saya menulis beberapa artikel di sini dan di sini .

Source: https://habr.com/ru/post/id469379/

More articles:


All Articles