Search or add a thesis

Advanced Search (Beta)
Home > Automation of Software Modeling and Verification

Automation of Software Modeling and Verification

Thesis Info

Access Option

External Link

Author

Sultana, Sidra

Program

PhD

Institute

National University of Sciences & Technology

City

Islamabad

Province

Islamabad

Country

Pakistan

Thesis Completing Year

2018

Thesis Completion Status

Completed

Subject

Software Engineering

Language

English

Link

http://prr.hec.gov.pk/jspui/bitstream/123456789/13329/1/PhD%20Thesis-Sidra%20Sultana-MCS-NUST.pdf

Added

2021-02-17 19:49:13

Modified

2024-03-24 20:25:49

ARI ID

1676727709495

Asian Research Index Whatsapp Chanel
Asian Research Index Whatsapp Chanel

Join our Whatsapp Channel to get regular updates.

Similar


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 part focuses 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 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 that verification 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.
Loading...
Loading...

Similar Books

Loading...

Similar Chapters

Loading...

Similar News

Loading...

Similar Articles

Loading...

Similar Article Headings

Loading...

نواب سید محمد علی حسن خان

ایک نواب عالم کی وفات
ہندوستان کے ان پرانے مسلمان خاندانوں میں سے جو شرافت نسب کے ساتھ علم اور دولت دونوں کے جامع ہیں، اب خال خال گھرانے رہ گئے ہیں، انہیں میں سے ایک والا جاہ نواب سید صدیق حسن خان مرحوم کا خاندان تھا، جن کے چھوٹے صاحبزادہ صفی الدولہ حسام الملک شمس العلماء نواب سید محمد علی حسن خان مرحوم نے ۱۹؍ نومبر ۱۹۳۶؁ء مطابق، ۳؍ رمضان المبارک ۱۳۵۵؁ھ کی صبح کو اپنی کوٹھی بھوپال ہاؤ س لال باغ لکھنؤ میں بہتر برس کی عمر میں وفات پائی، افسوس ہے کہ ایک پرانے خاندان کے فضل و کمال اور جاہ و جلال کی یادگار آج مٹ گئی۔
مرحوم ان لوگوں میں تھے جن کی آنکھوں نے مسلمانوں کے علمی و تعلیمی، سیاسی و تمدنی انقلاب کے مناظر دیکھے، وہ پیدا تو ایک ’’کنزرویٹو‘‘ گھرانے میں ہوئے اور اسی ماحول میں تعلیم و تربیت پائی، لیکن فطرت کی طرف سے وہ ایک اثر پذیر اور حساس دل لائے تھے، باوجود اس کے کہ وہ بھوپال میں پیدا ہوئے جہاں حددرجہ قدامت کی حکومت اور سطوت تھی اور ممکن نہ تھا کہ نورمحل میں نئی روشنی کی ایک کرن بھی پہنچ سکے، مگر استعداد طبع دیکھئے کہ کہ خود بخود ادھر طبیعت کا میلان ہوا، سرسید کی جدید تعلیمی تحریک میں اور پھر ندوۃ العلماء کی مذہبی تحریک میں شریک ہوئے اور ہر قسم کی جانی و مالی خدمتیں انجام دیں، مدت تک ندوہ کے اعزازی ناظم رہے، دارالمصنفین کے اساسی ارکان میں تھے اور لکھنؤ کی ہر سنجیدہ تحریک میں ان کا نام سرفہرست رہتا تھا۔
وہ عربی زبان کے عالم، فارسی زبان کے ماہر اور اردو کے مشّاق اہل قلم تھے، فارسی شعر و سخن اور محاورات پر ان کو عبور کامل حاصل تھا، فارسی کا مشکل سے کوئی اچھا شعر ہوگا...

Patterns of Deranged Lipid Profiles in Patients of Chronic Hepatitis C Deranged lipid profile in hepatitis C patients

Liver plays an important role in lipid metabolism and any acute or chronic malfunction of the liver due to viral hepatitis or liver cirrhosis may induce lipid derangements Objective: To determine the patterns of deranged lipid profiles in patients of chronic hepatitis C Methods: It is a prospective, observational study, conducted at Medicine Department, Mayo Hospital Lahore for 6 months i.e.1stJanuary to 30th June 2018. After the ethical approval, 160 diagnosed cases of chronic hepatitis C of ages 18-70 years of either gender were selected by non-probability purposive sampling. Informed written consent was taken. Demographic information such as name, age and gender were recorded. Venous blood samples from patients after 10 to 14 hours of fasting were drawn for lipid profiles and sent to pathology laboratory. All results were expressed as mg/dl. Data were analyzed in SPSS version 22 Results: Out of 160 patients in this study, there were 94 males and 66 females. Total cholesterol was lower in 62.5% patients, normal in 33.75% patients and higher in 3.75% patients. Triglycerides levels were low in 66.25%, normal in 33.125%, and high in 0.625% patients. Low density lipoprotein (LDL) levels were low in 82.5% patients, normal in 10% and raised in 7.5% patients. High density lipoprotein (HDL) levels were low in 95%, normal in 4.375% & high in 0.625% patients Conclusions: Low levels of serum lipids including total cholesterol, triglycerides, LDL and HDL are seen in population suffering from chronic HCV infection.

Modelling of Tlr4 and Jak/Stat Signalling Pathways and Protein-Protein Interaction Studies to Examine the Pathophysiology of Sepsis

In this thesis, the medical condition of sepsis is considered at molecular level (signalling pathways) using computational systems-level approaches in order to get insights into the mechanism of disease progression. Sepsis is the pathological condition provoked due to the presence of bacterial endotoxin in the bloodstream. Subsequently Toll like receptors (TLR)4 and JAK/STAT signalling pathways attempt to reduce the pathogen burden by inducing pro- and anti-inflammatory innate immune responses. However, in some instances, an overwhelmed immune system could not properly regulate the balance between infection and inflammation that may ultimately lead to organ damage and consequently to death. In recent years, there has been an increasing amount of literature on the pattern of pro- and anti-inflammatory response elicited during sepsis, though; there has been a little agreement on the roles of pro- and antiinflammatory cytokines (AiCyts) in sepsis. This study mainly aims to address the controversy behind roles of pro- and anti-inflammatory cytokines in sepsis by modelling the signalling pathway of TLR4 and one of the connected signalling cascades of JAK/STAT using qualitative modelling approach introduced by René Thomas’. The possible system dynamics of TLR4-JAK/STAT signalling pathways are produced for two medical conditions i.e. non-sepsis (type of infections that generally do not cause sepsis) and sepsis along with perturbations in these two cases. As a result, recurrent induction and inactivation of pro-inflammatory cytokines is found as the basic feature associated with sepsis. Besides AiCyts, IFN-β and SOCS-1 are found to mediate down-regulation of pro-inflammatory cytokines at different stages of signalling which cause variation of pro-inflammatory cytokines levels. It is observed that intervention in IFN-β mediated down-regulation of pro-inflammatory cytokines at earlier stages of system dynamics, while intervening the SOCS-1 mediated down-regulation of proinflammatory cytokines at later stages ensures hyper-inflammatory condition. On the other hand, interventions in TLR4, NFκB (transcription factor involved in the TLR4 1 Abstract signalling pathway) and JAK/STAT signalling are good choices for supporting the anti-inflammatory immune responses. Thus only possible protein-protein interactions involved in the initial downstream interactions of TLR4 signalling are studied in order to predict a more appropriate target in these interactions. Previous studies indicated that MyD88 adaptor-like protein (MAL) is an endogenous adaptor protein recognized as an important protein involved in the induction of TLR4 mediated downstream signalling pathway. Moreover, it has also been demonstrated that BTK and PKCδ phosphorylate MAL (positions Tyr86 and Tyr106) which ultimately activates MAL. Thus the modelling of PKCδ and protein-protein interactions of both BTK and PKCδ with MAL is performed in order to explore their competitive interaction. Molecular docking and physicochemical analysis reveals that PKCδ may phosphorylate only Tyr106 of MAL, while BTK may phosphorylate MAL at both positions. Interestingly, the charge and hydrophobicity at interfaces of PKCδ and BTK are found different in nature yet well-compatible with the individual positions of Tyr86 and Tyr106 of MAL. The most prominent findings emerged from this analysis is that position Tyr86 of MAL may explicitly be phosphorylated by BTK, while position Tyr106 of MAL may be phosphorylated by the competing interest of both PKCδ and BTK. In conclusion, this thesis will enhance our understanding about the signalling and protein-protein interactions involved in sepsis which will contribute to the development of drugs and vaccines against the medical condition of sepsis.