Formal verification หากแปลเป็นภาษาไทยจะแปลว่า การทวนสอบเชิงรูปนัย ถึงแม้จะแปลเป็นภาษาไทยแล้ว หลายคนก็ยังสงสัยอยู่ดีว่าแท้ที่จริงแล้วมันคืออะไร หลังจากการพัฒนาโปรแกรมเสร็จแล้วจะบวนการที่สำคัญต่อไปคือการทดสอบโปรแกรม และมีเทคนิคหนึ่งที่เป็นส่วนหนึ่งของกระบวนการทดสอบคือ Verification ในการทดสอบโปรแกรมนั้นส่วนใหญ่ tester จะเป็นคนทดสอบหรือทวนสอบว่าซอฟต์แวร์นั้นเป็นไปตาม spec หรือเปล่า นี้คือวิธีการทวนสอบแบบทั่วๆไป แต่การทวนสอบแบบ Formal verification นั้นเป็นอีกศาสตร์หนึ่งของการทวนสอบ ซึ่งจะมีความซับซ้อนกว่ามาก ใช้ตรรกะและการจำลองแผนภาพเข้ามาใช้ในการทวนสอบ เหมาะสำหรับขนาดใหญ่ที่ต้องการความปลอดภัยสูงจะเกิดข้อผิดพลาดไม่ได้
หากนึกไม่ออกว่าเป็นอย่างไร การจะนำหลักการของ Formal verification นั้นมาใช้กับซอฟต์แวร์ที่ต้องการความปลอดภัยสูงนั้นเป็นอย่างไร ก็ให้นึกภาพตามดังต่อไปนี้
- ปัจจุบันระบบการบินนั้นเป็นแบบ Autopilot แทบทั้งหมด คือเมื่อถึงความสูงระดับหนึ่งซอฟต์แวร์จะเป็นคนควบคุมเครื่องบิน ดังนั้นลองคิดดูว่าหากซอฟต์แวร์นั้นเกิดข้อผิดพลาดจะเกิดอะไรขึ้น
- ระบบรถยนต์ขับเคลื่อนอัตโนมัติใช้ซอฟต์แวร์ในการคำนวณตรวจจับวัตถุและควบคุมความเร็ว หากซอฟต์แวร์คำนวณการเคลื่อนไหวของวัตถุหรือความเร็วผิดพลาดจะเป็นอย่างไร
- เครื่องฉายรังสีจะคำนวณความเข้มแสงก่อนฉายรังสีไปยังคนไข้ จะเป็นอย่างไรหากซอฟต์แวร์คำนวณผิดพลาด
- ระบบสัญญาณไฟจราจร จะต้องมีลำดับการทำงานที่ชัดเจน จะเกิดอะไรขึ้นหากสัญญาณไฟ 2 ฝั่งเป็นสีเขียวพร้อมกัน
ข้อสมมติฐานที่ได้กล่าวมานั้น หากเกิดข้อผิดพลาดขึ้นเพียงแค่ครั้งเดียว อาจจะสร้างความสูญเสียถึงชีวิตของผู้คนได้ ดังนั้นการทวนสอบจะต้องทวนสอบในทุกกรณีที่เป็นไปได้ ซึ่งจะใช้ Formal verification ช่วยในการทวนสอบ
การทวนสอบเชิงรูปนัย (Formal verification) ทำงานอย่างไร
ปกติแล้วการทวนสอบจะแบ่งเป็น formal และ informal verification การทวนสอบแบบ informal verification นั้นส่วนใหญ่จะใช้คนในการทวนสอบหรือทดสอบ ซึ่งอาจจะใช้วิธีการก่อนที่ได้ทำมาทวนสอบ(best practices) คนที่จะมาทำการทวนสอบหรือทดสอบนั้นควรจะเป็นผู้เชี่ยวชาญ การทวนสอบนี้ก็จะมีประโยชน์เช่น เราพัฒนาซอฟต์แวร์เสร็จแล้ว มีทีม tester หรือ user มาเป็นผู้ร่วมทดสอบ แต่การทวนสอบในลักษณะนี้ จะให้ความสำคัญเชิงคุณภาพมากกว่าเชิงปริมาณ หรือการทดสอบอาจจะทดสอบ feature ที่สำคัญและใช้งานบ่อย แต่ area ที่ไม่สำคัญก็อาจจะไม่ได้รับการทดสอบ ดังนั้นการทวนสอบในลักษณะนี้จะไม่สามารถทดสอบ 100% ของกรณีที่เป็นไปได้ทั้งหมด (Incomplete coverage) ต่างจากการทวนสอบเชิงรูปนัยหรือ formal verification ที่จะใช้เครื่องมือทางคณิตศาสตร์เข้ามาช่วยพิสูจน์เพื่อยืนยันผลการออกแบบ การทำ formal verification จะสามารถทำการทวนสอบทุกกรณีที่เป็นไปได้ทั้งหมด (Complete coverage) แต่การทวนสอบแบบ formal verification จะอยู่ในรูปแบบของ logic หรือ model ซึ่งจะต้องมีการแปลง system requirement ให้อยู่ในรูปแบบที่กำหนดไว้ก่อน ถึงจะสามารถทวนสอบได้
Formal Specification แปลง High-level เป็น Low-level requirement
ในช่วงเริ่มต้นของการพัฒนา Requirement ที่ได้มานั้นจะอยู่ในรูปแบบของ High-Level คือเป็นรายละเอียดที่เป็นลักษณะข้อความ แต่อาจจะไม่สามารถนำมาพัฒนาโปรแกรมได้ (Lower-Level)
ในการทวนสอบแบบ Formal verification นั้นอย่างที่ทราบกันว่าเป็นการทวนสอบขึ้นสูง จะต้องแปลง requirement เป็นระบดับ Lower-lever ก่อนถึงจะเริ่มการทวนสอบได้ หลักการสร้างเป็น Lower-lever อย่างหนึ่งคือสร้างแบบจำลองแบบ Formal language การแปลงในลักษณะนี้จะต้องแปลงอยู่ในสัญลักษณ์ทางคณิตศาสตร์ก่อน เช่นหากมี requirement บอกว่ามี "ในวงจรหลอดไฟมีสวิทช์สองตัวต่อแบบอนุกรมกัน สวิทช์แต่ละตัวเป็นสวิทช์แยกของหลอดไฟแต่ละตัว" ซึ่งเราสามารถนำหลักของคณิตศาสตร์มาอธิบายได้ดังนี้
T คือเปิดสวิทช์ F คือปิดสวิทช์
จะสังเกตว่าแค่ requirement เพียงไม่กี่ประโยคก็สามารถแปลงเป็น logic ได้มากมาย ดังนั้นการจะแปลงข้อมูลเป็นในรูปแบบของ Formal language ได้นั้นจะต้องเข้าใจคณิตศาสตร์ที่ได้เรียนมาในช่วงมัธยม โดยจะต้องใช้ความรู้เรื่อง
การเกิด Interleaving และ Concurrency
การที่ software ware ทำงานในกิจกรรมบางกิจกรรมพร้อมกัน อาจจะทำให้เกิดปัญหาได้ เช่น นาย ก ทำการถอนเงินออกจากบัญชี แต่ในเวลาเดียวกัน แฟนของนาย ก ก็ทำการโอนเงินออกจากบัญชีของนาย ก ด้วย หากระบบไม่มีการจัดการแล้ว อาจจะทำให้เกิดข้อผิดพลาดเรื่องบัญชีขึ้นได้ อีกตัวอย่างหนึ่งคือเรื่องสัญญาณไฟจราจรคือจะต้องมีสีเขียวเพียงฝั่งเดียว หากมีสีเขียวสองฝั่งนั้นคือการเกิด Interleaving ดังนั้นเพื่อเป็นการป้องกันไม่ให้เกิด Concurrency หรือ Interleaving เราควรใช้การทวนสอบแบบ Formal verification เป็นอย่างยิ่ง ซึ่งในการทวนสอบนั้นเราสามารถ model มาเพื่อใช้ในการทวนสอบได้
การสร้างแบบจำลอง(Model)
เป็นแผนภาพจำลองที่แสดงถึง state และการเปลี่ยนแปลงของ state เพื่อให้สามารถแสดงถึงพฤติกรรมของระบบได้ การสร้างแบบจำลองขึ้นมานั้นจะใช้ในการดูว่าจะ accept หรือ reject state ลักษณะของแผนภาพคือจะใส่ตัว input string เข้าไป แล้วดูผลว่า accept หรือ reject ใน model ของแบบจำลองก็มีรูปแบบต่างๆที่ใช้ในการสร้างแบบจำลอง เช่น automata, Buchi Automata Kripke, Petri Nets, Coloured Petri Nets เป็นต้น ซึ่งแต่ละ model ก็จะมีลักษณะที่แตกต่างๆกันออกไป ขึ้นอยู่กับจุดประสงค์ของผู้ใช้งานว่าต้องการทวนสอบแบบไหน ก็เลือกใช้ model ที่เหมาะสม
ยกตัวอย่างเครื่องชงกาแฟแบบหยอดเหรียญ ขึ้นแรกจะต้องใส่เหรียญเข้าไป เลือกกาแฟ ชงกาแฟ และรอรับกาแฟ เราสามารถเข้าใจได้ง่ายและสามารถนำไปทวนสอบได้ หากนำไปสร้างเป็นแบบจำลอง ดังภาพ
ตัวอย่างการทำงานของเครื่องอ่านเทป โดยจะมี state เริ่มต้นและเริ่มอ่านตัวอักษรใน state ถัดไปเรื่องๆ แผนภาพจะแสดงถึงการเปลี่ยน state และตัวอักษรว่ามีการทำงานอย่างไร
เนื้อหาจากบทความนี้เป็นเพียงส่วนหนึ่งของ Formal verification ปัจจุบันมีงานวิจัยมากมายที่วิจัยเกี่ยวกับเรื่องนี้ ในอนาคตซอฟต์แวร์จะส่งผลต่อชีวิตประจำวันของเราเป็นอย่างมาก ทั้งทางตรงและทางอ้อม ยิ่งซอฟต์แวร์ที่เกี่ยวข้องถึงชีวิตแล้ว ยิ่งต้องการความปลอดภัยสูง การใช้ศาสตร์ด้าน Formal verification น้น จะช่วยให้เราลดความเสี่ยงและมั่นใจถึงคุณภาพของซอฟต์แวร์ได้
Reference:
1. วิวัฒน์ วัฒนาวุฒิ ภาควิชาวิศวกรรมคอมพิวเตอร์ คณะวิศวกรรมศาสตร์ จุฬาลงกรณ์มหาวิทยาลัย. (2561). Formal Verification การทวนสอบเชิงรูปนัย. พิมพ์ครั้งที่ 1
2. https://en.wikipedia.org/wiki/Informal_Methods_(Validation_and_Verification)
3. Sally C. Johnson, Ricky W. Butler, Formal Methods, https://pdfs.semanticscholar.org/c933/6b13cfe46428f441b5d8614f0827b2861655.pdf
4. Yann Duplouy , Applying Formal Methods to Autonomous Vehicle Control
การทวนสอบเชิงรูปนัย (Formal verification) ทำงานอย่างไร
ปกติแล้วการทวนสอบจะแบ่งเป็น formal และ informal verification การทวนสอบแบบ informal verification นั้นส่วนใหญ่จะใช้คนในการทวนสอบหรือทดสอบ ซึ่งอาจจะใช้วิธีการก่อนที่ได้ทำมาทวนสอบ(best practices) คนที่จะมาทำการทวนสอบหรือทดสอบนั้นควรจะเป็นผู้เชี่ยวชาญ การทวนสอบนี้ก็จะมีประโยชน์เช่น เราพัฒนาซอฟต์แวร์เสร็จแล้ว มีทีม tester หรือ user มาเป็นผู้ร่วมทดสอบ แต่การทวนสอบในลักษณะนี้ จะให้ความสำคัญเชิงคุณภาพมากกว่าเชิงปริมาณ หรือการทดสอบอาจจะทดสอบ feature ที่สำคัญและใช้งานบ่อย แต่ area ที่ไม่สำคัญก็อาจจะไม่ได้รับการทดสอบ ดังนั้นการทวนสอบในลักษณะนี้จะไม่สามารถทดสอบ 100% ของกรณีที่เป็นไปได้ทั้งหมด (Incomplete coverage) ต่างจากการทวนสอบเชิงรูปนัยหรือ formal verification ที่จะใช้เครื่องมือทางคณิตศาสตร์เข้ามาช่วยพิสูจน์เพื่อยืนยันผลการออกแบบ การทำ formal verification จะสามารถทำการทวนสอบทุกกรณีที่เป็นไปได้ทั้งหมด (Complete coverage) แต่การทวนสอบแบบ formal verification จะอยู่ในรูปแบบของ logic หรือ model ซึ่งจะต้องมีการแปลง system requirement ให้อยู่ในรูปแบบที่กำหนดไว้ก่อน ถึงจะสามารถทวนสอบได้
Formal Specification แปลง High-level เป็น Low-level requirement
ภาพลำดับชั้นของ Formal Specification | ที่มา : Formal Methods
ในช่วงเริ่มต้นของการพัฒนา Requirement ที่ได้มานั้นจะอยู่ในรูปแบบของ High-Level คือเป็นรายละเอียดที่เป็นลักษณะข้อความ แต่อาจจะไม่สามารถนำมาพัฒนาโปรแกรมได้ (Lower-Level)
- Abstract specification คือเป็นการบรรลุความต้องการของระบบ
- High-Level design คือการออกแบบเพื่อให้บรรลุความต้องการของระบบ
- Lower-level design คือการตั้งสมมติฐานเกี่ยวกับระบบงานที่จะจำ การออกแบบอัลกอริทึม การวิเคราะห์ระบบงานที่ทำ การแจกแจงรายละเอียดอย่างชัดเจน
- Implementation คือการพัฒนาซอฟต์แวร์
ในการทวนสอบแบบ Formal verification นั้นอย่างที่ทราบกันว่าเป็นการทวนสอบขึ้นสูง จะต้องแปลง requirement เป็นระบดับ Lower-lever ก่อนถึงจะเริ่มการทวนสอบได้ หลักการสร้างเป็น Lower-lever อย่างหนึ่งคือสร้างแบบจำลองแบบ Formal language การแปลงในลักษณะนี้จะต้องแปลงอยู่ในสัญลักษณ์ทางคณิตศาสตร์ก่อน เช่นหากมี requirement บอกว่ามี "ในวงจรหลอดไฟมีสวิทช์สองตัวต่อแบบอนุกรมกัน สวิทช์แต่ละตัวเป็นสวิทช์แยกของหลอดไฟแต่ละตัว" ซึ่งเราสามารถนำหลักของคณิตศาสตร์มาอธิบายได้ดังนี้
T คือเปิดสวิทช์ F คือปิดสวิทช์
| สวิทช์ตัวที่ 1 | สวิทช์ตัวที่ 2 | สถานะหลอดไฟ |
|---|---|---|
| T | T | หลอดสว่าง |
| T | F | หลอดไม่สว่าง |
| F | T | หลอดไม่สว่าง |
| F | F | หลอดไม่สว่าง |
จะสังเกตว่าแค่ requirement เพียงไม่กี่ประโยคก็สามารถแปลงเป็น logic ได้มากมาย ดังนั้นการจะแปลงข้อมูลเป็นในรูปแบบของ Formal language ได้นั้นจะต้องเข้าใจคณิตศาสตร์ที่ได้เรียนมาในช่วงมัธยม โดยจะต้องใช้ความรู้เรื่อง
- ตรรกศาสตร์ การพิสูจน์ ประพจน์ ความเป็นเหตุผล
- ตรรกศาสตร์เชิงเวลา
- เซต ความสัมพันธ์
- พีชคณิตบูลีน
ตัวอย่างคำสั่งที่ใช้ในการควบคุมของภาษา Promela
ที่มา : หนังสือ Formal Verification การทวนสอบเชิงรูปนัย หน้า 140
การเกิด Interleaving และ Concurrency
การที่ software ware ทำงานในกิจกรรมบางกิจกรรมพร้อมกัน อาจจะทำให้เกิดปัญหาได้ เช่น นาย ก ทำการถอนเงินออกจากบัญชี แต่ในเวลาเดียวกัน แฟนของนาย ก ก็ทำการโอนเงินออกจากบัญชีของนาย ก ด้วย หากระบบไม่มีการจัดการแล้ว อาจจะทำให้เกิดข้อผิดพลาดเรื่องบัญชีขึ้นได้ อีกตัวอย่างหนึ่งคือเรื่องสัญญาณไฟจราจรคือจะต้องมีสีเขียวเพียงฝั่งเดียว หากมีสีเขียวสองฝั่งนั้นคือการเกิด Interleaving ดังนั้นเพื่อเป็นการป้องกันไม่ให้เกิด Concurrency หรือ Interleaving เราควรใช้การทวนสอบแบบ Formal verification เป็นอย่างยิ่ง ซึ่งในการทวนสอบนั้นเราสามารถ model มาเพื่อใช้ในการทวนสอบได้
การสร้างแบบจำลอง(Model)
เป็นแผนภาพจำลองที่แสดงถึง state และการเปลี่ยนแปลงของ state เพื่อให้สามารถแสดงถึงพฤติกรรมของระบบได้ การสร้างแบบจำลองขึ้นมานั้นจะใช้ในการดูว่าจะ accept หรือ reject state ลักษณะของแผนภาพคือจะใส่ตัว input string เข้าไป แล้วดูผลว่า accept หรือ reject ใน model ของแบบจำลองก็มีรูปแบบต่างๆที่ใช้ในการสร้างแบบจำลอง เช่น automata, Buchi Automata Kripke, Petri Nets, Coloured Petri Nets เป็นต้น ซึ่งแต่ละ model ก็จะมีลักษณะที่แตกต่างๆกันออกไป ขึ้นอยู่กับจุดประสงค์ของผู้ใช้งานว่าต้องการทวนสอบแบบไหน ก็เลือกใช้ model ที่เหมาะสม
ยกตัวอย่างเครื่องชงกาแฟแบบหยอดเหรียญ ขึ้นแรกจะต้องใส่เหรียญเข้าไป เลือกกาแฟ ชงกาแฟ และรอรับกาแฟ เราสามารถเข้าใจได้ง่ายและสามารถนำไปทวนสอบได้ หากนำไปสร้างเป็นแบบจำลอง ดังภาพ
ภาพการจำลอง coffee machine โครงสร้างด้วย Kripke
ที่มา : Yann Duplouy , Applying Formal Methods to Autonomous Vehicle Control, page5
ตัวอย่างการทำงานของเครื่องอ่านเทป โดยจะมี state เริ่มต้นและเริ่มอ่านตัวอักษรใน state ถัดไปเรื่องๆ แผนภาพจะแสดงถึงการเปลี่ยน state และตัวอักษรว่ามีการทำงานอย่างไร
ภาพ finite-state automata | ที่มา : Formal Languages
เนื้อหาจากบทความนี้เป็นเพียงส่วนหนึ่งของ Formal verification ปัจจุบันมีงานวิจัยมากมายที่วิจัยเกี่ยวกับเรื่องนี้ ในอนาคตซอฟต์แวร์จะส่งผลต่อชีวิตประจำวันของเราเป็นอย่างมาก ทั้งทางตรงและทางอ้อม ยิ่งซอฟต์แวร์ที่เกี่ยวข้องถึงชีวิตแล้ว ยิ่งต้องการความปลอดภัยสูง การใช้ศาสตร์ด้าน Formal verification น้น จะช่วยให้เราลดความเสี่ยงและมั่นใจถึงคุณภาพของซอฟต์แวร์ได้
Reference:
1. วิวัฒน์ วัฒนาวุฒิ ภาควิชาวิศวกรรมคอมพิวเตอร์ คณะวิศวกรรมศาสตร์ จุฬาลงกรณ์มหาวิทยาลัย. (2561). Formal Verification การทวนสอบเชิงรูปนัย. พิมพ์ครั้งที่ 1
2. https://en.wikipedia.org/wiki/Informal_Methods_(Validation_and_Verification)
3. Sally C. Johnson, Ricky W. Butler, Formal Methods, https://pdfs.semanticscholar.org/c933/6b13cfe46428f441b5d8614f0827b2861655.pdf
4. Yann Duplouy , Applying Formal Methods to Autonomous Vehicle Control
