Reliable operation of every day use computing system, from simple coffee machines to complex flight controller system in an aircraft, is necessary to save time, money, and in some cases lives. System testing can check for the presence of unwanted execution but cannot guarantee the absence of such. Probabilistic model checking techniques have demonstrated significant potential in verifying performance and reliability of various systems whose execution are defined with likelihood. However, its inability to scale limits its applicability in practice.
This thesis presents a new model checker, STAMINA, with efficient and scalable model truncation for probabilistic verification. STAMINA uses a novel model reduction technique generating a finite state representations of large systems that are amenable to existing probabilistic model checking techniques. The proposed method is evaluated on several benchmark examples. Comparisons with another state-of-art tool demonstrates both accuracy and efficiency of the presented method.
| Identifer | oai:union.ndltd.org:UTAHS/oai:digitalcommons.usu.edu:etd-8740 |
| Date | 01 August 2019 |
| Creators | Neupane, Thakur |
| Publisher | DigitalCommons@USU |
| Source Sets | Utah State University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | All Graduate Theses and Dissertations |
| Rights | Copyright for this work is held by the author. Transmission or reproduction of materials protected by copyright beyond that allowed by fair use requires the written permission of the copyright owners. Works not in the public domain cannot be commercially exploited without permission of the copyright owner. Responsibility for any use rests exclusively with the user. For more information contact digitalcommons@usu.edu. |
Page generated in 0.0022 seconds