Search or add a thesis

Advanced Search (Beta)
Home > Formal Dependability Analysis Using Higher-Order-Logic Theorem Proving

Formal Dependability Analysis Using Higher-Order-Logic Theorem Proving

Thesis Info

Access Option

External Link

Author

Waqar Ahmad

Program

PhD

Institute

National University of Sciences & Technology

City

Islamabad

Province

Islamabad

Country

Pakistan

Thesis Completing Year

2017

Thesis Completion Status

Completed

Subject

Applied Sciences

Language

English

Link

http://prr.hec.gov.pk/jspui/bitstream/123456789/8177/1/PhD%20Thesis%20Waqar%20Ahmad.pdf

Added

2021-02-17 19:49:13

Modified

2024-03-24 20:25:49

ARI ID

1676726225584

Similar


Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, con- dentiality, and integrity. Various dependability modeling techniques have been developed to e ectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paperand- pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. To overcome these limitations, we propose to leverage upon the recent developments in probabilistic analysis support in higher-order-logic theorem proving to conduct accurate and rigorous dependability analysis. This thesis provides a semantic language embedding of the dependability concept that relies on a theory for probabilistic reasoning to develop a framework for formal dependability analysis within the sound environment of higher-order-logic theorem proving. In this thesis, we mainly focus on the formalization of two widely used dependability modeling techniques: (i) Reliability Block Diagrams - a graphical technique used to determine the reliability of overall system by utilizing the failure characteristics of individual system components; and (ii) Fault Trees - used for graphically analyzing the conditions and the factors causing an undesired top event, i.e., a critical event, which can cause the whole system iv v failure upon its occurrence. In particular, we present a RBD and FT-based formal dependability analysis framework that has the ability to accurately and rigorously determine the formal reliability, failure, availability and un- availability of safety-critical systems with arbitrary number of components. To illustrate the practical e ectiveness of our proposed infrastructure, we present the formal dependability analysis of several real-world safety-critical systems, including smart grids, WSN data transport protocols, satellite solar arrays, virtual data centers, oil and gas pipeline systems and an air tra c management system using the HOL4 theorem prover.
Loading...

Similar Thesis

Showing 1 to 20 of 100 entries
TitleAuthorSupervisorDegreeInstitute
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
Mehran University of Engineering and Technology, Jamshoro, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National College of Business Administration and Economics, Lahore, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
Mphil
Riphah International University, Faisalabad, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National College of Business Administration and Economics, Lahore, Pakistan
PhD
National University of Computer and Emerging Sciences, Islamabad, Pakistan
MS
International Islamic University, Islamabad, Pakistan
Riphah International University, Faisalabad, Pakistan
MS
International Islamic University, Islamabad, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
Mehran University of Engineering and Technology, Jamshoro, Pakistan
Mehran University of Engineering and Technology, Jamshoro, Pakistan
Mphil
Government College University, Lahore, Pakistan
Mphil
Riphah International University, Faisalabad, Pakistan
MS
Riphah International University, Lahore, Pakistan
TitleAuthorSupervisorDegreeInstitute
Showing 1 to 20 of 100 entries

Similar Books

Loading...

Similar Chapters

Loading...

Similar News

Loading...

Similar Articles

Loading...

Similar Article Headings

Loading...

رسائل و جرائد

شعر و ادب کو پروان چڑھانے میں ادبی شخصیتوں کا اپنا مقام و مرتبہ ہے یہ کیسے ہو سکتا تھا کہ رسائل و جرائد اور اخبارات ان سے پیچھے رہتے خطہ سیالکوٹ کے مقامی رسائل و جرائد اور اخبارات ادب کی ترقی کے لیے ماضی سے اہم خدمات سر انجام دیتے چلے آرہے ہیں۔ان میں ’’نوائے سماج‘‘،’’ندائے سیالکوٹ‘‘،’’ہمدرد پاکستان‘‘ ،’’محنت کش‘‘ اور ’’شبنم‘‘ اہم رسائل و جرائد میں شمار ہوتے ہیں۔ان رسائل و جرائد اور اخبارات کے باقاعدہ ادبی ایڈیشن بھی شائع ہوتے رہے ہیں۔

          سیالکوٹ کے اخبارات کی موجودہ صف میں ’’صدائے شہر‘‘ ،’’نوائے شمال‘‘ اور ’’اخبار سیالکوٹ‘‘ نمایاں اخبارات ہیں۔رسائل و جرائد کی فہرست میں ’’مرے کالج میگزین ‘‘،’’مفکر‘‘،’’کاوش‘‘، ’’افق‘‘،’’محورِحیات ‘‘، ’’اقدار‘‘، ’’ادراک‘‘، ’’انتخاب‘‘، ’’کیہان‘‘، ’’یدبیضا‘‘، ’’گجر‘‘، ’’کرائیڈن‘‘، اور’’سٹی میگ‘‘آج بھی ادبی خدمات میں اہم کردار ادا کر رہے ہیں۔

          ’’گجر‘‘ ،’’انتخاب‘‘،’’ید بیضا‘‘ تاب اسلم کے شعور و فکر کا نچوڑ ہیں ان تینوں رسائل وجرائد کو تاب اسلم بڑی عرق ریزی سے ادبی دنیا کے سامنے پیش کرتے رہے ہیں۔ان ادبی رسائل نے بہت سے نئے لکھنے والوں کی راہنمائی کا فریضہ سر انجام دیا ہے۔تاب اسلم کے ان جرائد کو نہ صرف سیالکوٹ بلکہ برصغیر پاک و ہند کے نامور ادبا و شعرا ،ناقدین اور محققین کا قلمی تعاون حاصل رہا۔سیالکوٹ کے اہم ادبی رسائل و جرائد کے تعارف کے لیے تفصیل پیش کی جاتی ہے۔

۱۔       مر ے کالج میگزین :

          مرے کالج میگزین کا پہلا شمار ہ نومبر...

Factors Affecting the Failure of Patient Safety Target Indicators in the Regional Hospital of the Datu Beru Takengon Central Aceh

The application of patient safety management is very important in an effort to prevent or minimize the occurrence of adverse patient safety incidents. The purpose of this study was to identify the factors that influence the achievement of patient safety target indicators. The method is a quantitative observational study with a cross sectional study approach. The study population was a nurse who worked in the inpatient room with a sample of 60 people who were taken by purposive sampling. The statistical test used is Multiple Linear Regression Analysis. The results of the Multiple Linear Regression Test show that knowledge, communication systems, commitment and experience (regression coefficient values ​​of 0.164, 1.1192, 0.528 and 1.169 have a positive influence on the achievement of patient safety goal indicators and leadership, risk management systems and reporting systems have a significant influence. Negative impact on the achievement of patient safety target indicators (regression coefficient values ​​of -0.064, - 0.967 and -0.281). The results of the t test were obtained that the communication system is the dominant factor that has a significant effect on the achievement of the patient safety goal indicators. Significant towards the achievement of patient safety target indicators. It is expected that input or consideration for the hospital in evaluating and improving hospital policies in increasing the achievement of patient safety target indicators is in accordance with existing targets.

Redefining Urdu Morphology and Grammar for the Development of an Integrated Sentiment Analysis Framework

The rise of social networking sites and blogs has simulated a bull market in personal opinion; consumer recommendations, product reviews, ratings, and other types of online expressions. For computational linguistic researchers, this fast-growing heap of information has opened an exciting research frontier, referred as, the Sentiment Analysis (SA). For English, this area is under consideration from last decade. But, other major languages, like Urdu, are totally overlooked by the research community. Urdu is a morphologically rich and recourse poor language. The distinctive features, like, complex morphology, flexible grammar rules, context sensitive orthography and free word order, make the Urdu language processing a challenging problem domain. For the same reasons, sentiment analysis approaches and techniques developed for other well-explored languages are not workable for Urdu text. This dissertation presents a grammatically motivated, sentiment classification framework to handle these distinctive features of the Urdu language. The main research contributions are; to highlight the linguistic (orthography, grammar and morphology, etc.) as well as technical (parsing algorithm, lexicon, corpus, etc.) aspects of this multidimensional research problem, to explore Urdu morphological operations, grammar and orthographic rules, to redefine these operations and rules with respect to the requirements of sentiment analysis framework. The orthographical, morphological, grammatical and finally the conceptual details of the language are our target concerns. Additionally, our approach can help in the sentiment analysis of other languages, like Arabic, Persian, Hindi, Punjabi etc. The proposed framework emphasizes on the identification of the SentiUnits, rather than, the subjective words in the given text. SentiUnits are the sentiment carrier expressions, which reveal the inherent sentiments of the sentence for a specific target. The targets are the noun phrases for which an opinion is made. The system extracts SentiUnits and the target expressions through the shallow parsing based chunking. The dependency parsing algorithm creates associations between these extracted expressions. The framework uses the sentiment-annotated lexicon based approach. Each entry of the lexicon is marked with its orientation (positive or negative) and the intensity (force of orientation) score. The experimentation based evaluation of the system with a sentiment-annotated lexicon of Urdu words and two corpuses of reviews as test-beds, shows encouraging achievement in terms of accuracy, precision, recall and f-measure.