Automation of Software Modeling and Verification / (Record no. 615908)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03746nam a22001817a 4500 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | NUST |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20260126091414.0 |
| 082 ## - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 005.1,SUL |
| 100 ## - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Sultana, Sidra |
| 9 (RLIN) | 29744 |
| 245 ## - TITLE STATEMENT | |
| Title | Automation of Software Modeling and Verification / |
| Statement of responsibility, etc. | Sidra Sultana |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. | |
| Place of publication, distribution, etc. | Rawalpindi, |
| Name of publisher, distributor, etc. | MCS (NUST), |
| Date of publication, distribution, etc. | 2018 |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | xvii, 121 p |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Formal methods help in quantifying the functional and nonfunctional requirements that are later used in the verification process for safety assurance in real-time systems. System formalism is a crucial step in terms of exploring system’s behavior and listing the non-functional requirements. In the context of real-time systems, the non-functional requirements refer to the verification properties of the system. Formalism in software development life cycle refines every process, starting from the formalization of system's requirements, analysis of system's behavior and exploring its properties, implementation of the problem's solution under consideration and verification of safety critical properties. Rule-based Expert System helps in inferring unknown on the basis of some known input, that is, knowledge and rule-set. Knowledge comprises of something known by an individual called as an expert of that domain. It requires an expert skill set (that is, syntax and notations of the Model Checker and Verifier) in order to model and verify some system in Model Checkers like UPPAAL. This research consists of three parts. Firstly, it explores the variations (two case studies) of traffic light systems, models the systems in UPPAAL model checker and later verifies the safety critical properties of the generated systems like safety, live-ness, fairness, reachability and deadlock freeness. Experimental results are recorded for both systems with variety of search options to check the time efficiency. Second part of the research deals with the computational conversion via translation rules for transforming C++ code into UPPAAL’s automata and then cross-checked the validity of transformation rule set. This partfocuses on providing the rule-based expert system for inferring timed automata (input of UPPAAL Model Checker) on the basis of fact cum input, that is, C++ code. Structural facts are used along with the transformation rule set to get the timed automata that verifies safety properties of selected case studies–multiple variations of Traffic Light<br/>ix<br/>System. Last part of the research is related to the reverse engineering of the verification artifact back to the implemented code. Experimental results of the first contribution show thatverification time used by the UPPAAL model checker is worth mentioning for safety and deadlock freeness properties. Kernel responded all properties in no time, but the deadlock property took 0.01seconds. Elapsed time is the one that responds uniquely for all of the verified properties. Safety property took maximum elapsed time i.e., 0.02 seconds and with fractional change deadlock freeness property has 0.018 seconds of elapsed time used. Outcome of the second part that is, translation from C++ code to UPPAAL model is verified successfully. In the proposed methodology, the correctness of the transformation is crosschecked twice. Firstly, the informally mentioned behavior of C++ program is presented in the transformed automata and secondly the interaction among the functions via function call is preserved in UPPAAL’s automata via synchronization of channels. Third part is successfully reverse engineered from UPPAAL’s automata to C++ code. |
| 650 ## - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | PhD Computer Software Engineering Thesis |
| 9 (RLIN) | 132801 |
| 651 ## - SUBJECT ADDED ENTRY--GEOGRAPHIC NAME | |
| Geographic name | PhD CSE Thesis |
| 9 (RLIN) | 132802 |
| 700 ## - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Supervised by Dr. Fahim Arif |
| 9 (RLIN) | 132700 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Source of classification or shelving scheme | |
| Koha item type | Thesis |
| Withdrawn status | Lost status | Source of classification or shelving scheme | Damaged status | Not for loan | Permanent Location | Current Location | Shelving location | Date acquired | Total Checkouts | Full call number | Barcode | Date last seen | Price effective from | Koha item type | Public note |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Military College of Signals (MCS) | Military College of Signals (MCS) | General Stacks | 01/26/2026 | 005.1,SUL | MCSPhD CS-06 | 01/26/2026 | 01/26/2026 | Thesis | Almirah No.68, Shelf No.5 |