پاکستانی معاشرہ اور تعلیمات قرآنی میں بعد

In spite of the fact that Pakistan is an Islamic Republic, 97% of the population is Muslim and majority of it is considered sentimently staunch Muslims; it is a fact that society is not familiar and closely attached with Quranic injunctions. There are many reasons for that such as custom of teaching Quran Nazira (reciting Quran without understanding), Arabic language is not part of curriculum and when it is taught in DiniMadaris, it is taught in boring Grammar Method relying on memorization. Quran is not taught in modern schools, colleges and universities and lower social status of Quran teachers etc. It is absolutely necessary that teaching Quran with comprehension and understanding is given due importance by Ulama, governments and Muslim society at large. It should be made integral part of curriculum in modern schools and universities. Status of Quran/Arabic teachers should be elevated and Arabic language should be taught in an attractive method;  and other necessary measures are taken to make Quran ‘talk of the town’ so that every Muslim understands it and acts upon its injunctions.

Automation of Software Modeling and Verification

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.