การตรวจสอบรูปแบบเชิงปริมาณ เครือข่ายมหาวิทยาลัย

รายละเอียด

การรวมกันของ ICT (เทคโนโลยีสารสนเทศและการสื่อสาร) ในแอพพลิเคชั่นต่าง ๆ กำลังเพิ่มขึ้นอย่างรวดเร็วเช่นระบบสมองกลฝังตัวและไซเบอร์, โปรโตคอลการสื่อสารและระบบการขนส่ง ดังนั้นความน่าเชื่อถือและความน่าเชื่อถือของพวกเขาจึงขึ้นกับซอฟต์แวร์ ข้อบกพร่องอาจถึงแก่ชีวิตและมีค่าใช้จ่ายสูงมาก (เกี่ยวกับการผลิตสินค้าจำนวนมากและระบบที่สำคัญต่อความปลอดภัย)

ก่อนอื่นต้องสร้างโมเดลของระบบจริง ในกรณีที่ง่ายที่สุดโมเดลจะสะท้อนสถานะที่เป็นไปได้ทั้งหมดที่ระบบสามารถเข้าถึงและช่วงการเปลี่ยนภาพที่เป็นไปได้ทั้งหมดระหว่างรัฐในระบบการเปลี่ยนสถานะ (ที่มีป้ายกำกับ) เมื่อเพิ่มความน่าจะเป็นและเวลาที่ไม่ต่อเนื่องให้กับแบบจำลองเรากำลังติดต่อกับโซ่มาร์คอฟแบบเวลาไม่ต่อเนื่องซึ่งจะสามารถขยายได้ด้วยระยะเวลาต่อเนื่องไปยังโซ่มาร์คอฟแบบต่อเนื่อง มีการใช้พิธีการทั้งสองอย่างกว้างขวางในการสร้างแบบจำลองและประเมินประสิทธิภาพและความน่าเชื่อถือของคอมพิวเตอร์และระบบการสื่อสารในหลากหลายโดเมน พิธีการเหล่านี้เป็นที่เข้าใจกันดีมีความน่าสนใจทางคณิตศาสตร์ในขณะเดียวกันก็มีความยืดหยุ่นเพียงพอที่จะสร้างแบบจำลองระบบที่ซับซ้อน

การตรวจสอบแบบจำลองจะเน้นไปที่การประเมินคุณภาพของแบบจำลอง ในฐานะที่เป็นวิธีการตรวจสอบอย่างเป็นทางการการตรวจสอบรูปแบบการวิเคราะห์
การทำงานของรูปแบบระบบ ต้องระบุคุณสมบัติที่ต้องวิเคราะห์ในตรรกะที่มีไวยากรณ์และความหมายที่สอดคล้องกัน สำหรับทุกสถานะของโมเดลจะถูกตรวจสอบว่าคุณสมบัตินั้นถูกต้องหรือไม่
จุดสนใจหลักของหลักสูตรนี้คือการตรวจสอบแบบจำลองเชิงปริมาณสำหรับโซ่มาร์คอฟซึ่งเราจะหารือเกี่ยวกับอัลกอริธึมการคำนวณที่มีประสิทธิภาพ วัตถุประสงค์การเรียนรู้ของหลักสูตรนี้มีดังนี้:

- แสดงคุณสมบัติความน่าเชื่อถือสำหรับระบบการเปลี่ยนแปลงประเภทต่างๆ
- คำนวณวิวัฒนาการเมื่อเวลาผ่านไปสำหรับโซ่ Markov
- ตรวจสอบว่าสถานะเดียวตรงตามสูตรที่กำหนดหรือไม่และคำนวณความพึงพอใจที่ตั้งไว้สำหรับคุณสมบัติ