Science, Irving K. Barber Faculty of (Okanagan)
Computer Science, Mathematics, Physics and Statistics, Department of (Okanagan)
DSpace
UBCO
Mahato, Pradeep Kumar
Master of Science - MSc
University of British Columbia
Software specifications define system behavior, usage guidelines, requirements and act as a tool for debugging. However, quite often, such specification documentation is either missing or carries outdated information due to the evolutionary nature of the software development process. As a result, system operators, developers, and users face difficulties during the production phase due to limited or no information. The problems get even more serious in safety-critical systems. Safety-critical systems are used in many important tasks such as automotive, disaster relief operations, monitoring patient's medical health, and more. In this thesis, we attempt to address the problem of mining missing or outdated software requirement specifications from system traces. We present several approaches to enable system operators to better understand software behavior. We present three tools QMine, MMTQ, and MINTS for mining software specifications from system traces. QMine and MMTQ perform template-based mining for a quantitative regular expression and timed quantitative regular expression with linear time complexity respectively. We propose a novel formalism of timed-quantitative regular expressions that incorporate both events, quantitative values, and time constraints all within a single specification. We realize the limitations of QMine and MMTQ with the need for a human-crafted template as their basis. In an attempt to alleviate this issue, we propose, MINTS a framework that extracts system behavior using traces from the system in an unsupervised approach. MINTS is capable of revealing various system states and the relationship among the state transitions. It then extracts dominant temporal patterns from the extracted relationship model. We use system traces from a custom-built Hexacopter that uses QNX operating system for extracting the dominant temporal patterns. We subsequently mine the quantitative properties using the templates extracted by MINTS for validation. We discuss the soundness and completeness of our frameworks along with their applicability in various industrial settings. Our frameworks are scalable and have been deployed on various industry strength traces.
SPECIFICATION MININGFRAMEWORKS FOR COMPLEXSOFTWARE SYSTEMSbyPradeep Kumar MahatoB.Tech Hons., NIT Jamshedpur, 2013A THESIS SUBMITTED IN PARTIAL FULFILLMENT OFTHE REQUIREMENTS FOR THE DEGREE OFMASTER OF SCIENCEinThe College of Graduate Studies(Computer Science)THE UNIVERSITY OF BRITISH COLUMBIA(Okanagan)October 2021© Pradeep Kumar Mahato, 2021The following individuals certify that they have read, and recommend tothe College of Graduate Studies for acceptance, a thesis/dissertation entitled:SPECIFICATIONMINING FRAMEWORKS FOR COMPLEX SOFT-WARE SYSTEMSsubmitted by Pradeep Kumar Mahato in partial fulfilment of the require-ments of the degree of Master of ScienceDr. Apurva Narayan, The Irving K. Barber Faculty of ScienceSupervisorDr. Jeff Andrews, The Irving K. Barber Faculty of ScienceSupervisory Committee MemberDr. Fatemeh Fard, The Irving K. Barber Faculty of ScienceSupervisory Committee MemberDr. Eric Li, Faculty of ManagementUniversity ExamineriiAbstractSoftware specifications define system behavior, usage guidelines, require-ments and act as a tool for debugging. However, quite often, such specifi-cation documentation is either missing or carries outdated information dueto the evolutionary nature of the software development process. As a result,system operators, developers, and users face difficulties during the productionphase due to limited or no information. The problems get even more seriousin safety-critical systems. Safety-critical systems are used in many impor-tant tasks such as automotive, disaster relief operations, monitoring patient’smedical health, and more.In this thesis, we attempt to address the problem of mining missing oroutdated software requirement specifications from system traces. We presentseveral approaches to enable system operators to better understand softwarebehavior. We present three tools QMine, MMTQ, and MINTS for min-ing software specifications from system traces. QMine and MMTQ performtemplate-based mining for a quantitative regular expression and timed quanti-tative regular expression with linear time complexity respectively. We proposea novel formalism of timed-quantitative regular expressions that incorporateboth events, quantitative values, and time constraints all within a single spec-ification. We realize the limitations of QMine and MMTQ with the need fora human-crafted template as their basis. In an attempt to alleviate this issue,we propose, MINTS a framework that extracts system behavior using tracesfrom the system in an unsupervised approach. MINTS is capable of revealingvarious system states and the relationship among the state transitions. It thenextracts dominant temporal patterns from the extracted relationship model.We use system traces from a custom-built Hexacopter that uses QNX operat-ing system for extracting the dominant temporal patterns. We subsequentlymine the quantitative properties using the templates extracted by MINTS forvalidation. We discuss the soundness and completeness of our frameworksalong with their applicability in various industrial settings. Our frameworksare scalable and have been deployed on various industry strength traces.iiiLay SummarySoftware documentation contains technical guidelines explaining detailsabout the software system. Such documentations often accompany every sys-tem. However, quite often these software specification documents are missingor hold outdated information. Sometimes, they are very brief and only providean overview of the system.This thesis aims to reduce the gap between the system and the usage ofthe system. We present 3 approaches that can be used to extract dominantsystem properties from system traces. The extracted summarization describesthe system behavior.System specifications are presented in the form of graphs. Graphical repre-sentation enables users from various domains to easily understand the system’sbehavior. Additionally, we also present a framework to mine interesting sys-tem properties using templates.ivPrefaceThis thesis titled “Extraction of system specification” presents a novelpattern mining framework capable of extracting the system specification in anunsupervised fashion. We also present 2 pattern-mining frameworks to extractquantitative summaries from the system logs. I carried out my research ob-jectives under the supervision of Dr. Apurva Narayan. Materials presented inChapter 2 is published as Mahato et al. [MN] while Chapter 3 and Chapter 4are submitted and is under review at “Workshop on Human-Centric SoftwareEngineering & Cyber Security (HCSE&CS-2021)” and “IEEE 21st Interna-tional Conference on Software Quality, Reliability and Security (QRS) 2021”respectively.Some of the datasets were collected from Dr. Apurva Narayan while otherswere collected from an open-source data repository (mentioned alongside eachexperimental section except the ones related to Hexacopter). Additionally, allexperiments and analyses were performed entirely by me.Material presented in Chapter 2 was presented in [MN] Dec. 2020 IEEE.Reprinted, with permission, from Pradeep K. Mahato et al., QMine: A Frame-work for Mining Quantitative Regular Expressions from System Traces, 2021IEEE 20th International Conference on Software Quality, Reliability and Se-curity Companion (QRS-C), Dec. 2020.During my stay, I also worked with RICHs Food and published our re-search work at the 2020 IEEE Symposium Series on Computational Intelli-gence (SSCI) titled “Robust Supply Chains with Gradient Boosted Trees”[MN20] during my internship, however, this thesis does not contain any of itspublished research work.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viiiList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixAcknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . xDedication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiChapter 1: Introduction . . . . . . . . . . . . . . . . . . . . . . . . 11.1 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.1.1 QMine: A Quantitative Regular Expression Mining Frame-work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.1.2 MMTQ: A framework to mine and monitor Timed Quan-titative Regular Expression . . . . . . . . . . . . . . . . 41.1.3 MINTS: A Temporal Specification Miner . . . . . . . . 41.2 Thesis structure . . . . . . . . . . . . . . . . . . . . . . . . . . . 5Chapter 2: QMine: A Quantitative Regular Expression Min-ing Framework . . . . . . . . . . . . . . . . . . . . . . 62.1 Related Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.2.1 Quantitative Regular Expressions . . . . . . . . . . . . . 112.3 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122.3.1 Normalizer . . . . . . . . . . . . . . . . . . . . . . . . . 132.3.2 QMine Algorithm . . . . . . . . . . . . . . . . . . . . . 132.3.3 QMine Filter . . . . . . . . . . . . . . . . . . . . . . . . 15viTABLE OF CONTENTS2.3.4 QRE Parser . . . . . . . . . . . . . . . . . . . . . . . . . 172.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182.4.1 Memory Requirements . . . . . . . . . . . . . . . . . . . 182.5 Experimentation . . . . . . . . . . . . . . . . . . . . . . . . . . 202.5.1 Evaluation using Synthetic Traces . . . . . . . . . . . . 20Chapter 3: MMTQ: A framework to mine and monitor TimedQuantitative Regular Expression . . . . . . . . . . . 233.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243.2 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293.3.1 Memory Requirements . . . . . . . . . . . . . . . . . . . 293.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313.4.1 Evaluation using Synthetic Traces . . . . . . . . . . . . 31Chapter 4: MINTS: A semi-supervised Temporal SpecificationMiner . . . . . . . . . . . . . . . . . . . . . . . . . . . . 334.1 Related Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . 344.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 354.3 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . 374.3.1 Formation of the Trietimed . . . . . . . . . . . . . . . . . 374.3.2 Pruning . . . . . . . . . . . . . . . . . . . . . . . . . . . 414.3.3 Event Prediction . . . . . . . . . . . . . . . . . . . . . . 434.3.4 Dominant Property extraction . . . . . . . . . . . . . . 444.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464.5 Experiment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 494.5.1 Evaluation using Synthetic Trace . . . . . . . . . . . . . 50Chapter 5: Experimental Analysis and Conclusion . . . . . . . . 535.1 Experimental Analysis . . . . . . . . . . . . . . . . . . . . . . . 535.1.1 Problem Statement . . . . . . . . . . . . . . . . . . . . . 545.1.2 Data set . . . . . . . . . . . . . . . . . . . . . . . . . . . 545.1.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 555.1.4 Comparison of Result with Baseline Framework . . . . . 655.2 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 695.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71Appendix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79Appendix A: Additional Experimental Results . . . . . . . . . . . . 79viiList of TablesTable 2.1 QMine Complexity . . . . . . . . . . . . . . . . . . . . . 19Table 2.2 Analysis for QRET Size, Alphabet and Compilation time 21Table 3.1 MMTQ Complexity . . . . . . . . . . . . . . . . . . . . 30Table 4.1 Temporal Properties used for mining in MINTS . . . . . 45Table 4.2 Comparison of various specification miners . . . . . . . . 48Table 5.1 Hexacopter Dominant Properties . . . . . . . . . . . . . 56Table 5.2 Hexacopter Temporal Properties . . . . . . . . . . . . . 58Table 5.3 Specification Mined using QMine . . . . . . . . . . . . . 60Table 5.4 Event mapping as used in QMine . . . . . . . . . . . . . 60Table 5.5 Event mapping as used in MMTQ . . . . . . . . . . . . 61Table 5.5 continued from previous page . . . . . . . . . . . . . . . 62Table 5.5 continued from previous page . . . . . . . . . . . . . . . 63Table 5.6 Quantitative Specification Analysis using MMTQ . . . . 64Table 5.7 Comparison of QMine, MMTQ and MINTS with TREand StreamQRE . . . . . . . . . . . . . . . . . . . . . . 66Table 5.8 Comparison of monitoring capability for QMine, MMTQw.r.t StreamQRE . . . . . . . . . . . . . . . . . . . . . . 68Table A.1 Summary of quantitative values on the Arrhythmia Dataset . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80Table A.2 Android application usage with transition over 2 appli-cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82Table A.3 Android application usage with transition over 3 appli-cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84Table A.4 Server Call analysis with varying window interval . . . . 87Table A.5 Server Call analysis with fixed window frame and varyingwindow transitions . . . . . . . . . . . . . . . . . . . . . 88Table A.6 Richter magnitude of simultaneous earthquakes . . . . . 89Table A.7 Summary of quantitative values mined on the DiabetesData set . . . . . . . . . . . . . . . . . . . . . . . . . . . 91viiiList of FiguresFigure 1.1 Finite State Machine of an Automated Teller Machine(ATM) . . . . . . . . . . . . . . . . . . . . . . . . . . . 2Figure 1.2 Timed Finite State Machine of an Automated TellerMachine(ATM) . . . . . . . . . . . . . . . . . . . . . . 3Figure 2.1 Sample Arrhythmia Data with both quantitative andqualitative values . . . . . . . . . . . . . . . . . . . . . 7Figure 2.2 QMine Worklfow . . . . . . . . . . . . . . . . . . . . . . 12Figure 2.3 Thread distribution in QMine . . . . . . . . . . . . . . 15Figure 2.4 Varying number of events in QTrace . . . . . . . . . . . 21Figure 2.5 Varying number of distinct event . . . . . . . . . . . . . 22Figure 3.1 MMTQ Worklfow . . . . . . . . . . . . . . . . . . . . . 26Figure 3.2 Varying total number of events . . . . . . . . . . . . . . 32Figure 3.3 Varying distinct event . . . . . . . . . . . . . . . . . . . 32Figure 4.1 MINTS Framework . . . . . . . . . . . . . . . . . . . . 37Figure 4.2 Sample Representation of Trietimed . . . . . . . . . . . 40Figure 4.3 Clock constraints are evaluated at depth 2 . . . . . . . 40Figure 4.4 Determination of clock constraint . . . . . . . . . . . . 42Figure 4.5 Event Prediction . . . . . . . . . . . . . . . . . . . . . . 44Figure 4.6 Trace length vs extraction time . . . . . . . . . . . . . 50Figure 4.7 Depth of Trietimed . . . . . . . . . . . . . . . . . . . . . 51Figure 4.8 Increasing alphabet size . . . . . . . . . . . . . . . . . . 51Figure 4.9 Sample illustration of Trietimed with depth as 5 . . . . 52Figure A.1 Battery usage for transition over 2 applications . . . . . 85Figure A.2 Server usage analysis . . . . . . . . . . . . . . . . . . . 88ixAcknowledgementsFirst and foremost, I would like to thank Dr. Apurva Narayan for hiscontinuous support that made this thesis possible. He constantly kept en-couraging and supporting me during my entire stay at UBCO. His advice andsuggestion have greatly helped me improve professionally. I would forever beindebted to him for providing me an opportunity to pursue my Masters underhis leadership.Additionally, I would also like to thank Dr. Fatemeh Fard for reaching outand discussing the opportunities at UBCO. I am deeply grateful to you forgiving me a glimpse of hope during my Master’s application process. I amalso grateful to Dr. Jeff Andrews for providing valuable feedback that helpedshaped my thesis as well as to Dr. Eric Li for assisting in structuring thethesis from a more general perspective. My colleagues at UBCO kept me stayin an optimistic mindset during my research tenure. I am thankful to RishabSharma who helped me in keeping a sane mindset. His punctuality is whatmade me keep moving forward and meet all the deadlines satisfactorily.Finally, I could not have completed my thesis without the blessing of myparents and my wife. They have always stood by me and I am forever indebtedto my family.xDedicationTo my wife and my family for encouraging and continuously supportingme throughout my journey.xiChapter 1IntroductionWith the advent of computers, especially powerful hardware and internetaccessibility, the use of technology has been deeply ingrained in our modern-day lives. Straight from using morning alarms to ordering breakfast, from re-questing a cab ride to talking to people using phone, from tutoring to schedul-ing appointments with a doctor, and many more, we have become increasinglydependant on technology. [Mac, gsd] reports that by 2030, there will be morethan 6 billion users interacting with an electronic gadget. All software systemsprovide an interface for the user to communicate with a device. There can bemultiple software running within a software. For example, a web browser andmusic player executes on a base software system, known as the operating sys-tem. Software is developed by humans and is used by humans. With rapidchange in our lifestyles, all software must be developed and updated peri-odically. Google Playstore currently holds over 5 million applications [Sha]and it is projected that 1.2 billion software (or applications) will be in use by2030. As a result, documenting and maintenance of any software become veryimportant.Software specifications outline a set of rules that describe the system be-havior. These rules are necessary to understand the current system workflowand help in the development of software, troubleshooting for possible bugswithin the system, and more. Specifications can be communicated in mul-tiple ways, such as by adding documentation describing each function usedinside the software, providing sequence diagrams describing the communica-tion between the internal modules, etc. However, often these specifications aremissing or are not tracked appropriately. This can be due to tight deadlines forfeature implementation [LSF], ignorance from the developer to update an olderspecification [dSAdO, Mor, KM], etc. As a result, maintaining the softwarebecomes increasingly challenging for new developers [LLb]. Troubleshootingof production bugs becomes difficult due to the lack of information, migrationof the original developer into a different organization or team, etc. Therefore,the need to learn system specifications automatically using system traces withminimal human interaction is desirable.Specification mining is the process of learning system properties from theexecution logs. System behavior and the interaction with the user are recordedin traces. Traces record system events in chronological order. Temporal spec-1Chapter 1. Introductionification mining is the extraction of system properties with the notion of time.Temporal specification mining is a heavily studied topic [DACa, Lama, DACb].Template-based specification mining has drawn significant attention [MN,NCJF, LLb, WGY]. Template-based specification mining uses user-definedtemplate and pattern matching techniques to extract relevant properties. Spec-ification mining is extensively used in anomaly detection [LLb], software veri-fication [ES], system modeling [LPBa, Lo], etc.Pattern-based specification mining uses sequences of characters and eventsas a template. Regular expressions are a powerful tool for pattern mining.Regular expressions extract patterns that match a sequence of events or asimilar combination of sequences. Regular expressions are tools widely usedin text classification [MN, NCJF, NCJF], anomaly detection [LLb], etc. Reg-ular expressions can be represented as Finite State Machine. The term ’StateMachine’ was first coined by Hopcroft and Ullman in 1979 [HU]. State Ma-chines are graphical representations of different stages that the system under-goes during its entire execution lifecycle. It is composed of nodes that areinterconnected through edges. Node and edges describe the potential statesof the system as well as the relationship among such states. Finite State Ma-chine(FSM) contains a finite set of nodes. There are two variants of FSMnamely, Deterministic FSM and Non-Deterministic FSM. Figure 1.1 is anabstract illustration of a Finite State Machine for an Automated Teller Ma-chine(ATM). ATM enables customers to withdraw (or deposit) money, reviewtheir account balances, and more without the necessity of visiting a physicalbank to perform the same set of activities. Graphical representation of thestate machine includes the final state denoted by a concentric circle.Figure 1.1: Finite State Machine of an Automated Teller Machine (ATM)Deterministic Finite State Machine defines a system behavior that is con-stant while Non-deterministic Finite State Machines describe a system be-havior that changes with every execution. In this thesis, we only considerdeterministic finite state machines.Finite Automaton or Finite State Machines can be extended with the no-tion of time and are referred to as Timed Automata (TA) [ACZ+20]. Timed21.1. ContributionAutomata carries an additional clock constraint over the transition edge. Asa result, where the state of the system changes, it must be carried out with afixed set of actions and valid clock constraints. Clock constraints are definedby the clock valuation function and specify the time interval that must besatisfied. Figure 1.2 presents a Timed Finite State Machine representation ofan ATM. Each action is followed by a time interval. User must perform theaction within the given interval and failing to do so would result in the resetof the machine. TA are extensively used in safety-critical systems such as pro-cess engineering, medical devices, safety equipment, etc. These systems aretime-sensitive and must strictly comply with time. Timed Automata enablesthe extraction of temporal specifications of the system.Figure 1.2: Timed Finite State Machine of an Automated Teller Ma-chine(ATM)However, template-based specification mining is challenging due to itsheavy emphasis on domain knowledge [Ulu, UFAMa], a requirement for con-stant update with every system update [LSF], and is highly time-consuming[MN, tre]. These templates have very limited customization capability duringruntime and fail to adapt to the dynamic behavior of the system.1.1 ContributionAs a result, the necessity for mining system specifications while requiringlow domain knowledge is of interest. In this thesis, I present few techniques tomine system specifications using system traces. The following sections brieflyexplain the techniques and their application.1.1.1 QMine: A Quantitative Regular Expression MiningFrameworkSystem Traces or Log files are records of system behavior over time. Theselogs are often sorted in chronological order. Traces contain events and are31.1. Contributionsometimes followed by a numeric value. This numeric value describes the eventand is called quantitative value. Quantitative Regular Expressions (QRE) areextensions of a regular expression with the emphasis on the quantitative value.Quantitative Regular Expression was proposed by Alur et al. [MRA+a]. QREenables monitoring of system properties (in the form of quantitative values)using a neat formalism of regular expression. QRE can be used to studythe behavior of patient’s health records. StreamQRE [MRA+a] uses QREto monitor health as the records are continuously streamed into the systemfor validating against pre-defined properties. StreamQRE is a template-basedmonitoring framework and, to a certain extent, requires domain knowledge tobuild the monitoring template.Objective: Our primary aim is to reduce the dependency on the neces-sity of domain knowledge for building the specification monitoring template.Therefore, we developed QMine [MN], a framework to mine and subsequentlymonitor interesting QRE patterns in a semi-supervised approach. QMine in-ternally uses FSM and adds the benefits of quantitative attributes to performits mining task.1.1.2 MMTQ: A framework to mine and monitor TimedQuantitative Regular ExpressionSafety-critical systems are best modeled using Timed Automaton (TA)because TA are time-sensitive FSM and enables tighter control over the state-flow within the system compared to a traditional FSM. This is achieved usinga global clock guarding every state transition that allows a change in systemstate only if both the action and the clock constraints are satisfied. The systemreaches an accepting state only if a series of actions are performed within thetime bounds defined for each action. Therefore, time must be considered toextract precise system behavior for safety critical system.Objective: We aim to take advantage of the benefits a TA provides andinclude them in the mining of QRE properties. MMTQ extends QMine withthe addition of time and performs mining of all temporal specifications fromthe system traces with time-bound.1.1.3 MINTS: A Temporal Specification MinerThe input template for QMine and MMTQ are significantly generalizedcompared to StreamQRE. However, QMine and MMTQ extract and monitorsystem properties, based on user-defined templates.Objective: Build a framework for automatically learning the temporalproperties of a system from system traces. We developed MINTS to constructa TA of a system using the system traces in an unsupervised manner. We then41.2. Thesis structureuse the constructed TA to extract a set of dominant temporal specificationsthat describes the system. Our model can be used for system verification,anomaly detection, monitoring, and many more applications.All the above frameworks were validated with real-world traces and arehighly scalable.1.2 Thesis structureThe remainder of the thesis is structured as follows: Chapter 2 provides anoverview of QMine. Chapter 3 explains MMTQ while Chapter 4 presents ourframework MINTS for unsupervised extraction of system properties. Finally,I conclude my work in Chapter 5 with detailed experiments along with a briefdiscussion on the current limitations and future work.5Chapter 2QMine: A QuantitativeRegular Expression MiningFrameworkIn the past few decades. technology has evolved rapidly. The growth inthe Information Technology sector has witnessed some of the greatest booms.In 1965, Gordon E. Moore made an observation on the doubling of the numberof transistors in a span of every two years and termed it as Moore’s Law. Suchobservation became entirely true. In comparison to the 1990s, the number oftransistors has roughly doubled every two years. In the modern age, we seeelectronic gadgets, of the size of a grain of rice, containing millions of tran-sistors and are capable of achieving numerous responsibilities. Devices, espe-cially electronic devices, are extremely powerful and competent in performingtasks that were not comprehensible few years back. With such dense circuitboards and progress in the field of scientific research, modern-day electronicdevices are remarkably potent. The underlying software systems have becomeextremely user-friendly and effective in addressing their problem statement.Modern-day software spews out an exorbitant amount of data every second.Forbes reported an estimated 2.5 quintillion bytes of data are produced everyday (that’s 2.5 followed by 18 zeros) [Mar]. Software systems produce logsthat record the system behavior over time. System behavior can be specific tothe internal functioning of the system or interactions with the user. Systemlogs are useful in studying the pattern of the system (or the subject using it).However, with such powerful computing devices, the underlying software sys-tem has become increasingly complex. Complex software is difficult to debug,contains millions of line of code and are loosely specified [LLb]. Data min-ing and machine leaching techniques assist in understanding the underlyingbehavior.The temporal behavior analysis of a program is an extensively studiedtopic [DAC99, Lamb, Lee]. It involves mining temporal patterns [Wik], au-tomated program comprehension, and associated tasks such as anomaly detec-tion, intrusion detection, and others. In most cases, temporal pattern miningtechniques are aided by association rule mining for extracting relevant tempo-6Chapter 2. QMine: A Quantitative Regular Expression Mining Frameworkral properties [LLa]. Mined specifications are valuable since they can be usedfor a wide variety of activities in the software development life cycle (SDLC).Mined specifications can assist in automated verification techniques becausethey provide an easy and user-friendly way to describe program specifications.Figure 2.1: Sample Arrhythmia Data with both quantitative and qualitativevaluesFor instance, consider Figure 2.1, which presents pre-processed electro-cardiogram or ECG readings for arrhythmia patients. It may be importantfor these traces to satisfy temporal property such as “Age, sex, and bodydimensions are always followed by heartbeat and patient’s class”. More-over, the heartbeat should be within certain statistical limits. Most researchin temporal specification mining focuses on the ordering of events [ABL02,LMP, ECH+, YEB+, YEa]. Such as, a request is always followed by a re-sponse. However, combining temporal properties with a quantitative streamhas been explored using the formulation of quantitative regular expressionsin QRE [AFR] and its applications in real-time monitoring systems such asStreamQRE [MRA+a, MRA+b].In this chapter, we propose a novel framework, QMine, for mining temporalproperties in the form of quantitative regular expressions (QRE) from systemtrace. Our model takes a custom QRE specification template along with a setof trace logs. QRE mining framework enables one to describe system behaviorusing both sequences of events and the quantitative property of respectiveevents.This chapter is structured as follows, Section 2.1 briefly outlines some rel-evant studies around our work while Section 2.2 introduces the preliminariesnecessary for the understanding of our model. We then briefly explain Quan-titative Regular Expressions and the associated operations in section 2.2.1followed by the methodology of our model, QMine in Section 2.3. Section 2.4contains discussions related to the complexity of our model while Section 2.5presents experimental results using synthetic traces.72.1. Related Studies2.1 Related StudiesMining specification/requirements of computer programs is a well-studiedtopic in computer science [LKHL]. In software engineering, a myriad of specifi-cation mining techniques exists depending on the kind of specifications such asautomata, temporal rules, sequence diagrams, and others [LKHL]. They alsovary depending on the type of input provided to the models where static anal-ysis or model checking takes source code as input whereas, dynamic analysistechniques mine from the execution trace.Mining likely temporal specifications of programs from system traces havebecome popular [LPBb]. Critical and commonly occurring behavioral patternsare typically provided to the mining frameworks, which then mine system spec-ifications of that form. The mining techniques identify a set of specificationsthat are satisfied by traces w.r.t. certain criteria.Many programs lack formal temporal specifications, and mined specifica-tions are therefore valuable since they can be used for a wide variety of activ-ities in the software development life cycle (SDLC). These activities includesoftware testing [DKM+], automated program verification [KP], anomaly de-tection [CJK], debugging [GS], etc.The work is inspired by [AFR] where an abstract language of QRE is pre-sented for specifying complex numerical queries over data streams and [NCJF]where a framework is presented for mining timed regular expressions fromsystem traces. StreamQRE is an application of QREs for monitoring and ispresented in [MRA+a, MRA+b]. It is an attempt for computing quantitativesummaries from data streams in real-time. With increasing complexity andobstructions arising for real-time decision making in emerging IoT applica-tions, the author of the paper provides a streaming framework that aims tosolve this specific problem. StreamQRE aims at providing statistical analysisin real-time by processing system trace log.TRE mining framework presented in [NCJF] mines for all possible patternsin a system-generated trace file. This provides both flexibility and rigor to theuser. Yet TRE is limited to event traces. In another work, authors mineproperties in the form of nested words by using a restricted class of context-free grammar called the nested word automaton from system traces [NBF].2.2 PreliminariesTraces record the behavior of the system. Traces are specific to theircorresponding system however generally traces contain events along with de-scriptions related to the events. They are sorted in chronological fashion. Theassociated descriptions can be in the form of long textual descriptions, system-82.2. Preliminariesspecific status codes, numerical values, or more. In this chapter, we considerthe associated description in the form of numerical values. We use the termmeasurement value or simply measurement while referring to such numericalvalues. In this section, we introduce the necessary terminology associated withour QMine framework.Definition 2.1 (Event). Any action performed within a system that leads tochange in system state.Definition 2.2 (Trace). Group of events forms traceDefinition 2.3 (QTrace or Quantitative Trace). A series of traces with quan-titative values between them forms a trace file with mixture of events andquantitative values.Definition 2.4 (Alphabet). Alphabet of events (Σ) is a set of all possibleevents.Events are a representation of the system and user behavior. We use αito represent an event and Σ to represent global set of events. Therefore, asystem with n unique events will have < α1, α2, · · · , αn >∈ Σ.Most industrial and IoT systems generate traces that are in the form oflog files and sensor data. Temporal property miners can be used to extractuseful information from log files and subsequently statistical analysis can beperformed on sensor data. Some research addresses both events in conjunctionwith quantitative values for monitoring systems behavior [MRA+a]. There isno framework reported to date that mines specifications/properties of systemsthat comprise of both events and quantitative values.Quantitative regular expressions have been proposed by [AFR] as a high-level declarative language for specifying queries over data streams in a modularway. It has been shown that QREs have good theoretical properties and areefficient for streaming applications. Therefore, the most intuitive applicationfor QREs is in the runtime monitoring of queries in streaming data. However,the mining of QRE is an unexplored territory.Cyberphysical systems, Internet-of-Things (IoT) devices, safety-critical in-struments, and more, produce traces in a staggering amount. In general,these traces contains events and are associated with some measurement thatdescribes the event. For instance, let’s consider record of patient’s medicalhealth (see Fig 2.1). Each attribute is associated with a measurement de-scribing the attribute such as Age 75 explains the Age of the patient as being75 years old. In this example, attributes can be considered as events from thesystem (that is, the medical device which was used for recording the patient’shealth) along with a measurement value. Such a pattern of alternating eventand measurement value can be classified as a QTrace (Quantitative Trace).92.2. PreliminariesIt must be noted that while all Quantitative Trace can be considered as aTrace, the reverse is not always true. Sometimes, traces can contain eventswith missing measurement values. In such a situation, we simply discard thesample or use a placeholder value for the measurement. A placeholder valuecould be the moving average (MA) associated with the specific event.Moreover, measurement values such as heartbeat, blood oxygen level, al-titude reading, and more are tracked using sensor modules. Temporal Spec-ification Miners can be used to extract meaningful information from tracesconsisting of sensor values. In [MRA+a], a static and valid Quantitative Reg-ular Expression template is used to monitor system properties. Traces arestreamed into the system in a real-time fashion. The monitoring system pro-vides real-time statistical analysis about the subject using the real-time trace.The restriction with such monitoring applications is regarding the monitoringtemplate. Specification templates are pre-determined before their applicationin the monitoring application.There are two major demerits with such an approach. Firstly, once themonitoring application is initiated, only the predetermined template can bemonitored. In order to monitor for a different specification property, the en-tire application has to be reinitiated with a different specification template.Secondly, the specification property template is system-specific and cannot beused for a different system.QMine resolves both these flaws by employing placeholder-based regularexpression. Our QMine framework mines properties from system traces thatcombine both events and signals simultaneously. Furthermore, QMine minesfor all possible pattern combinations specific to the generic template beforebeginning the monitoring application. It must be noted that the primarystrength of QMine is in mining various specification properties. Monitoringof the mined specification property is an extended feature of our framework.Our framework mines the input pattern provided using a specific template asdefined below.Definition 2.5 (QRET). A QRET is a valid template if it contains at leasttwo events (αi, αj) ∈ Σ and a series of m quantitative values q1 · · · qm boundedby αi and αjMore precisely, the most rudimentary form of QRET can be explained asQRET = α1Rα2 , where R is a set of real numbers.QMine is a template-based mining framework. We use the term eventvariable to denote a placeholder for an event and M to represent a quantitativevalue. For instance, a QRET 0 ·M ·1 represents “an event 0 is always followedby a quantitative value followed by an event 1 ”. It is important to note herethat M represents the quantitative part of QRET that can overload a variety102.2. Preliminariesof mathematical operations. We use τ to denote the number of event variables.In the above example, τ is 2.Definition 2.6 (Binding). Let V be a finite set of events in a QRET and Σrepresent alphabet of events. Then a binding is a function b : V → Σ . Thenumber of unique event variables in QRET is the dimension of the templateand is represented by τ .Definition 2.7 (Support Potential). The support of a QRET instance pi ona trace t is the number of time points of trace t which falsify pi.Definition 2.8 (Support). The support of a QRET instance pi on a trace t isthe number of time points of trace t which do not falsify pi.Definition 2.9 (Confidence). The confidence of QRET instance pi on a tracet is the ratio of trace support to trace support potential.The ranking component we use is a combination of support and confidence.The effectiveness of selecting a meaningful subset of specifications depends onpicking a good set of thresholds.Since the total number of mined QRET instances is often very large in realsystems, we would ideally keep the confidence value at 100%. However, themotivation to reduce this threshold slightly is due to the presence of imperfecttraces. Traces can be imperfect as a result of dropped events or executionof faulty programs. In such cases, dominant properties may not be perfectlysatisfied in the collected traces. Reducing the threshold will thus includedominant properties from imperfect traces.We examine different threshold values for both support and confidence andevaluate the best thresholds for reducing all feasible properties to adjust thedominant and interesting properties.2.2.1 Quantitative Regular ExpressionsThe work on StreamQRE [MRA+a] presents a framework that monitorsqueries in the form of modular patterns and an operation to be performed onthe quantitative values over streaming data provided in the form of QREs.Every pattern must be defined in terms of QRE combinators.Our framework supports combinators (atomic, iter, split, and choice) fromthe work of Alur et. al. [AFR, MRA+a]. QMine uses Ragel [Thu] for imple-menting the finite state machines. Ragel provides support for injecting user-defined action for every state change during transition within a finite statemachine.112.3. Methodology2.3 MethodologyIn this section, we discuss the architecture of our QMine framework. Figure2.2 provides a high level working of QMine framework. The QMine frameworkrequires two inputs: a real-world trace log in the QTrace format and a QREtemplate (QRET). These 2 inputs are fed to the normalizer module that pre-processes the trace as outlined in section 2.3.1, if needed. Subsequently, weFigure 2.2: QMine Worklfowhave the QMinecore module that maintains the thread pool of the finite statemachines for QMine instances. Each QMine finite state machine instancemines a single sub-sequences of QRET. Section 2.3.2 provides further detailsof the QMinecore algorithm. QMinecore outputs a mine-map ξ that holds allinstances of mined patterns and their related statistical details. The noveltyand substantial advantage of QMine are in the fact that once all instances aremined and stored in ξ, one can then query the mined results for other patterns122.3. Methodologythat prevent from going over the entire trace again. The mined results provideease of querying for various post-execution result analysis.The QMine filter module allows users to analyze for any pattern of interestwith ability to overload a statistical operation (currently QMine support µ(mean), σ (variance), min, and max) of interest to the engineer. Let us denotethe pattern template of interest as QRET. The event mapping dictionary η andmine-map ξ are available through the normalizer and the QMinecore module.Any log trace would typically consist of three types of events: (1) EventA marking the start of the pattern (2) measurement M, a set of numericalvalues (3) Event B marking the end of the pattern, and similar subsequentoccurrences.To illustrate our approach lets us consider two regular expressions R1 andR2 as pre-condition and post-condition patterns of interest with a quantitativemeasurement between the two expressions as M . Hence, QRET for such ascenario can be represented as (R1 ·M ·R2). Let us consider both R1 and R2have a single variable then our expression becomes 0 ·M · 1 where 0 and 1 areplaceholders for events in the trace alphabet Σ.Overall, QMine framework has four modules which define its working.These can be listed as below:− Normalizer− QMinecore− QMine Filter− QRE ParserIn the following sections we shall describe in the detail the four modulesof the QMine framework.2.3.1 NormalizerThe main goal of the normalizer is preprocessing of the input trace. This isrequired in case the set of events Σ is not available priori to mining propertiesfrom the traces and if the trace is not in the QTrace format. However, in mostcases the alphabet of the system under consideration is available.2.3.2 QMine AlgorithmAt the heart of our QMine property mining framework is QMinecore drivenby the QMine algorithm. This algorithm takes in the system trace in theQTrace format and QRE template to mine specifications that conform to theprovided QRET. Our algorithm uses Ragel [Thu] to implement finite state132.3. Methodologymachines and a multi-threading approach to achieve speedup. Algorithm 1provides a pseudo-code of the module.Algorithm 1: QMine(QRET, QTrace, Σ, ξ)Input: QRET, QTrace, alphabet Σ, mine-map ξResult: Mined properties for QTraceGenerate all permutations of QRET from ΣInitialize Finite State Acceptor (FSA)Set all threads with ξ and the FSADivide QTrace segments per threadforeach segment ∈ QTrace segments domineInternal (segment, ξ, FSA)endThe main objective of the Algorithm 1 is to mine all occurrences of allpatterns specified by a template in a given QTrace. We provide our QTrace,alphabet set Σ, and QRET as input. We initialize the thread pool vectoralong with finite state machines by generating all possible permutations ofQRET using the binding function. We subsequently initialize our threads andmaintain their counts th-count. We begin with recursively extracting QTracesegments that match the structure of the given QRET template and assignthem to a thread for processing. The algorithm iterates over each QTracesegment where each thread matches the segment with the FSA to find if itreaches an accepting state or an error state. Each thread returns a valueTRUE if its underlying finite state machine reaches an accepting state. Thethread that returns TRUE, is removed from our thread pool, and the mine-map is updated to reflect the results. The mine-map ξ, is available to eachthread and upon reaching the accepting state of the finite state acceptor all thetracked quantitative values are inserted in ξ for further statistical operationsas desired.All threads maintain mutual exclusion with respect to the mine-map, ξ.Consider a thread t, where t ∈ 〈t0, t1, · · · tth-count−1〉. All thread execute in-structions in their respective memory space except for operations on mine-mapξ. The update operation on ξ only happens in case a full match is found for apattern in the trace segment processed by the thread. The framework ensuresthat each sub-sequence is processed by one and only one thread at a time. Thisguarantees that more than one thread’s finite-state acceptor never reaches anaccepting state. Therefore, there would be only one update operation on ξat any time. Thus a race condition over mine-map ξ is guaranteed to nothappen.Figure 2.3 pictorially displays the allocation of segments of QTrace per142.3. MethodologyFigure 2.3: Thread distribution in QMinethread. Each thread handles only a single segment at a time. The threadallocation scheme reads the system QTrace event by event and continues topass it to a thread till it encounters a variable type (event/quantitative) thatmarks the start of the next instance of QRET. The scheme evaluates apriorithe variable/place holder for instantiating a new thread to take into consid-eration overlapping events between pattern occurrences. Consider QRET =0.M.1.M.2 with alphabet {A0, A1, A2} and a system trace A0 1 A1 3 A2 4 A05 A2 7 A1 8 A0, then the trace segment distribution over 3 thread is presentedbelow:− thread 1 is assigned to A0 1 A1 3 A2 segment− thread 2 is assigned to A1 3 A2 4 A0 segment− thread 3 is assigned to A2 4 A0 5 A2 segmentMulti-threading provides parallelism and speed up to our mining frame-work. Our scheme analyzes the available resources on the computer systemand accordingly modulates the number of threads required for program exe-cution.Algorithm 2 shows the working of an individual thread for each QTracesegment. The algorithm takes a trace segment, mine-map, and finite-stateacceptor as the input. Finite-state acceptor processes the trace segment and ifFINISH state is reached then mine-map is updated to reflect the count of themined pattern. The mine-map gets a new pattern added to the list if it doesnot exist in the list of already mined patterns. Our approach ensures that allpatterns are mined and accounted for in the system.2.3.3 QMine FilterOnce the entire trace has been processed by the QMine framework, thesummary of the patterns is represented in mine-map. One can develop awhole range of queries that can be answered by this abstraction, mine-map, ofthe system trace. For instance, we can now perform a variety of mathematicaloperations on the quantitative values in each instance of the mined pattern.152.3. MethodologyAlgorithm 2: mineInternal(segment, ξ, FSA)Input: QTrace Segment, ξ, FSAResult: Mined property satisfied by a QTrace segmentaction EVENTrecord patterns for QTrace Segment matchaction NUMpush digit to ξaction FINISHmatch overall patternpush ξ into global shared space & increment countreturn TRUE // Accepting stateaction ERRORremove inserted values from ξreturn FALSE // Error StateIn this work, we show how a filter can evaluate an average µ and standarddeviation σ for each pattern. The QMine filter can easily be extended to avariety of metrics that can help summarize the system trace under considera-tion. QMine filter also acts as a ranking module for mined properties whereit uses the combination of support and confidence provided by the user toextract dominant properties.Algorithm 3: evaluate(Query,ξ)Result: List of dominant patterns with µ, σInput: Query Pattern, ξ, Support, ConfidenceFilter patterns with Support & Confidence thresholdif Query Pattern ∈ ξ with Support & Confidence then/* compute µ and σ */endAlgorithm 3 takes as input a user-defined pattern instance in the QRETformat. The query searches through the mine-map in linear time and pro-vides instance counts, µ and σ for each of the quantitative variables in theQRET (or queried instance) with pre-specified or custom values for supportand confidence rules. Moreover, the negation of a variable in QRET is han-dled during post-processing by querying for a negated instance in the QMine’sfilter module.162.3. Methodology2.3.4 QRE ParserQREs are a declarative way of specifying quantitative regular expressionsin a hierarchical way as introduced by Alur et. al. [MRA+b]. We provide aninterface the allows engineers and developers to provide patterns and QRETsin a hierarchical format using the formalism provided by [AFR, MRA+a].The goal is to provide options to users to input their queries in either format,however keeping the mining framework generic for quantitative data streams.Our parser can convert hierarchical QREs to QRET format and vice-versa.This provides a wider advanced audience with familiarity with QREs and theones without it to use the tool for their analysis of complex systems.We present some basic parsing examples to show the relationships betweenQRE operators defined in Section 2.2.1 and QRET structure. Some basickeywords are:− E : E corresponds to an event placeholder− M : M corresponds to quantitative value− iterOp : iterOp corresponds to iterate operation.iterOp : (x, y)→ x+ y− splitOp : splitOp corresponds to concatenation operation.splitOp : (x, y)→ zExample 1. Create template R1 ·M ·R2 where M ← [0− 9] +Solution: In the given template, R1 and R1 are pre and post condition forpattern of interest with a quantitative measurement M in between them. Thiscan be converted to the QRE formulation based and expressed asR1 : QRE〈QTrace, τ〉 = atom(R1 ← R1.type = E) (2.1)M : QRE〈QTrace, τ〉 = atom(M ←M.type = M) (2.2)R2 : QRE〈QTrace, τ〉 = atom(R2 ← R2.type = E) (2.3)Using the atomic expression from Equation 2.1, 2.2 and 2.3, we can performsplit assplit1 : QRE〈QTrace, τ1〉 = split(R1,M, splitOp) (2.4)Thus using Equation 2.4 and associative property, we finally deduce our tem-plate asQRET : QRE〈QTrace, τ〉 = split(split1, R2, splitOp)= split(· · · ,M,R2, splitOp) (2.5)172.4. DiscussionUsing property 2.5, large and complex QRET can be formed. For furtherunderstanding of QREs one may refer to the work [AFR, MRA+a].Our QMine filter, presented in algorithm 3 taken QTraceuser as input.Our algorithm handles user-defined QTraceuser as plain text or in the formof a regular expression. For any dictionary event that must be negated, weprovide QTraceuser in the form of regular expression and our filter handles suchexpression automatically. We leverage the basic software implementation ofget or find available in all modern software engineering tools.2.4 DiscussionIn this section, we would like to show that our algorithm is correct, sound,and complete. Since QMine mines all possible instances of a QRET from thesystem trace. We argue that the technique we proposed and described in thisarticle is sound and complete. By sound, we mean that a mined specificationreported by our algorithms satisfies the given thresholds for confidence andsupport in the provided input traces. This is the case because our algorithmcontinuously keeps track of the success and reset rates for each QRE instancein the result mine-map. The rates are direct results of the execution of theacceptor automaton for the QRE on a trace and are used for calculation of theconfidence value for the QRE instance. Given that the reported rates and thederived confidence value are valid, it follows that the derived support value isvalid as well. Therefore, any mined specification that our algorithms reportsatisfies the confidence and support constraints.By characterizing our technique as complete, we mean that our algorithmsreport all the mined specifications that comply with the given thresholds forconfidence and support in the provided input traces. Upon reading an eventsequence from the trace, our technique examines every QRE instance that canbe affected. All the evaluation results are contained within the mine-map, theresults for every QRE instance will be considered when evaluating against theconfidence and support thresholds. Therefore, the algorithm will report allthe QRE instances, the mined specifications, that comply with the confidenceand support constraints.2.4.1 Memory RequirementsThe proposed quantitative regular expression mining technique requiresmemory space for the mine-map, the finite state acceptor, and the trace con-tents. The storage requirements for the mine-map are directly influenced byτ and Σ. The mine-map scales up to hold the evaluation results of every QREinstance generated by binding the events from Σ to the τ event variables in182.4. Discussionthe QRET. There are Στ possible TRE instances, thus we need O(Στ ) spaceto hold the acceptor results.The space requirements of the mine-map grows proportionally to τ , thenumber of symbols in the desired property. Complex properties that encodea relationship between a large number of events will result in higher valuesof τ . Increasing values of τ in turn will result in exponential space growth.However, the majority of properties of interest represent relationships amonga few events only [YEb, DACa]. Therefore, in general, the dimension τ of thematrix will remain small.The number of unique events Σ in the trace will depend on the complexityof the program or system. However, Σ has a much smaller effect on the growthof the mine-map since it only affects the base number in the exponential spacecomplexity.Next, we consider the storage requirements for the finite state acceptorused to evaluate the QRE. The storage required for the FSM is proportionalto the number of its states [HMUa]. If τ is the length of the QRE, then anequivalent NFA has O(τ) states and an equivalent DFA has at most O(Στ )states. Similar to the mine-map, complex properties that encode a lot ofrelationships between events result in exponential space growth for the FSM.However, a majority of interesting properties will remain simple [DACa].Lastly, the storage requirements for the trace are equivalent to the lengthof the trace, O(L), and for storing our mine-map where the worst-case spacerequirements are O(στ ). Our mining approach examines one event from thetrace at a time, without needing to store any past or future events for context.It also does not perform any changes in the contents of the trace. Thus thetrace is stored only once and never replicated.The proposed technique is thus scalable with the growing trace size Land with the growing event alphabet Σ. This is important since we have nocontrol over the events and traces generated by real systems. The technique issensitive to growing values of τ . However, as we already mentioned, in practicethis will not be a concern since properties remain relatively simple as shownin the evaluation section with industry grade case studies.Table 2.1: QMine ComplexityComplexity AnalysisTime O(Στ + L)Space O(Στ + L)Execution O(Στ + L/(th-count) thoh)Table 2.1 shows the space and time complexity for QMine. Execution com-192.5. Experimentationplexity refers to the time taken for parallel execution whereas time complexitystates the theoretical time bound for the same. Expression thoh represents themulti-threading overhead in the system. It is important to highlight at thispoint that the time and space complexity of QMine is linear with respect tothe length of the trace which makes is a promising approach when mining overlarge system traces.2.5 ExperimentationIn this section, we demonstrate the performance and scalability of our ap-proach using a set of synthetic traces. Chapter 5 provides detail related tothe application and experimental analysis of QMine using real-world traces.The implementation is done using C++. Ragel1 is a framework we used tosynthesize Finite State Automata for QREs. For the experiments, we used asingle eight-core Intel i7-2630QM CPU with 8 GB of RAM running on Ubuntu18.04 64 bit with GCC version 7.5.0. With the application of QMine softwareon the real-world Arrhythmia data set, our experiments demonstrate the per-formance and scalability by using different combinations of QRET and tracelengths.2.5.1 Evaluation using Synthetic TracesSystem traces related to the real-world data set are good for validatingthe correctness and for quick analysis of an algorithm. It provides a betterunderstanding and helps in strengthening the purpose of an algorithm.We perform validation on scalability and performance using synthetic tracesby adjusting the following parameters: τ , alphabet size Σ, and length ofQTrace. We record the overall execution time and memory requirements.Setup 1 (Memory and Compilation Time): In this case, we fix aQRET, 0 ·M · 1, where 0 and 1 are event place holders and M correspondsto a numerical quantity. We also fix the trace length but vary the alphabetlength Σ. Since we compute and compile for all possible patterns using theplaceholders in our QRET and alphabets in Σ, understanding the compilationtime and space complexity for our program is also crucial.Table 2.2 demonstrates the time taken by QMine to compile different pat-tern combinations. For illustration purposes we have shown QRET with onlyτ = 2 and τ = 3 while varying the number of unique events Σ.The results in Table 2.2 show an exponential growth in the time takenwhich is due to the generation of such a large number of patterns for the given1http://www.colm.net/open-source/ragel/202.5. ExperimentationTable 2.2: Analysis for QRET Size, Alphabet and Compilation timeQRET Alphabet Size Total QRE Instances Compile Time Taken (ms)0M110 90 2,84050 2450 2,955500 249500 61,2741000 999000 247,7280M1M210 720 2,91220 6840 3,25850 117600 23,114100 970200 638,822alphabet Σ. However, this is only a one time task and most practical systemshave limited alphabet size and pattern requirements.Setup 2 (Mine Time): We evaluate the scalability of our frameworkQMine with respect to the trace length and the alphabet size.Figure 2.4: Varying number of events in QTraceFigure 2.4 presents comparison for time taken to mine based on total eventcount. For this experiment, we restricted our τ for QRET to 2 and alphabetΣ = 26 while varying the number of events in the system trace. We areinterested in learning the impact of trace size in terms of the total number ofevents in the trace versus the mining time. We replicated our experiment 10times to ensure reproducibility and reliability in our results. Figure 3.2 showsthat our QMine scales linearly with increase in trace length.In Figure 2.5 we present the scalability analysis of QMine by varying thealphabet length Σ and keeping other parameters constant such as the dimen-sionality of QRET, τ = 2 and length of the trace L = 10, 000.212.5. ExperimentationFigure 2.5: Varying number of distinct eventThe results of Figure 2.5 and Figure 2.4 provide empirical evidence forthe correctness of our space-time complexity analysis. Here we see that thetime complexity of our algorithm is linear with respect to the length of thetrace (L) and exponential to the number of place holders (τ) in the QRET.The experimental results confirm the asymptotic analysis of our algorithm’scomplexity.22Chapter 3MMTQ: A framework tomine and monitor TimedQuantitative RegularExpressionTraces contain events describing the activities or states the system un-dergoes during runtime. In safety-critical systems and industrial applica-tions, traces contain events along with some form of quantitative measure-ments. Along with the event and measurements, the time of occurrence isalso recorded. Time plays an important role in safety-critical systems. Forexample, in the case of Airplanes, the sequence of events and the time ofoccurrence for each event is extremely important. Right from the start ofan aircraft preparing to take-off, during the entire flight journey, and untilits landing towards the end, the inflight software system, as well as the pilots,constantly monitor system behavior for any possible anomaly. In the situationof an aircraft, an event could be defined as the movement of the flappers oractions performed by the pilot such as steering action and many more. Suchevents must occur within a satisfactory time-bound. If a flapper takes toolong to flip or flips too quickly, it can cause catastrophic consequences. Theterm too long and too short are normally defined by domain experts.Mining events in association with time helps extract dominant temporalpatterns. It also allows detecting an anomaly within the system by observingthe system traces. In the previous chapter, we introduced QMine, a miningframework to extract specification properties using the formalism of Quan-titative Regular Expressions. Quantitative Regular Expressions provide thebenefit of analyzing and monitoring measurements associated with the events.QMine offers the completeness of the mined result alongside being highly scal-able. Although QMine considers the sequence of events nevertheless, it doesnot consider the time of occurrence of events. The input QRET has no in-formation regarding the relation between events with time. As a result, theextracted QRET instances do not carry time information.We address the above limitation with our MMTQ framework. MMTQ233.1. Preliminariesconsiders the relationship of events with time during the mining phase. Weconsider MMTQ as an extension to our QMine framework with the addition oftimed constraints. Thus, MMTQ also carries the same benefit of QRE miningalong with including timing constraints.This chapter introduces our MMTQ framework and is structured as follows:Section 3.1 provides a brief description related to the changes in the QRETsyntax for the sake of including time constraints. It must be noted that sinceMMTQ is an extension of QMine, we only provide the necessary preliminariesunder the introduction of time constraints. Section 3.2 provides a drive-through into the methodology of our framework followed by a time and spacecomplexity discussion in Section 3.3. Section 3.4 provides an experimentalanalysis using synthetic traces. We request the reader to refer to Chapter 5and Appendix 5.3 for a real-world evaluation of our framework.3.1 PreliminariesTraditional specification mining uses the ordering of events to extract pat-terns of interest. Thus the extracted pattern carries latent temporal informa-tion. However temporal information extends far beyond just the sequence ofevents. Alongside event order, the timing of events also plays an importantrole. Classical automata theory deal only with event ordering. Including theinformation of time adds richness to the automata. Consequently, the formedautomata and the patterns thus extracted carry a relatively large amount ofinformation. The primary application of such timed automata is evident in asafety-critical system where the ordering of events along with the relative timeof occurrence is important. Alongside including quantitative summarization,such as mean or standard deviation over the measurement values. We use suchformalism in our MMTQ framework.As already mentioned, since MMTQ is an extension of QMine with theaddition of time, therefore we skip similar definitions and only include theones that are required for understanding the timed extension.Definition 3.1 (QTracetimed). A QTrace which is associated with a times-tamp for every eventMost software systems contain traces in the form of sensor data recordingsand log files. Traces are usually recorded with a central system clock whereeach event entry has a timestamp. Using temporal mining property, one canmine for essential information and subsequently perform statistical analysis onboth the quantitative measurements and events at each data point. It mightalso be crucial to obtain such analysis in real-time. While some researchhas been done in this field that addresses both events and its measurements243.2. Methodology(refer [MRA+a, MN]), to the best of our knowledge no framework mines forproperties of systems comprising of both events and quantitative values withtime constraints.As defined in [tre, NCJF], a Timed Regular Expression (TRE) is a time-bounded regular expression which contains event variables and are boundedwith some time intervals. For example, a TRE as < 0.1 > [x, y] represents“ event variable 0 is followed by event variable 1 within a time interval [x,y]”.Henceforth, we define a Timed Quantitative Regular Expression (QREtimed)as a timed regular expression through the notion of quantitative measurementassociated with an event.Definition 3.2 (QREtimed). A QREtimed is a valid expression if it contains atleast two TRE (TREi, TREj) and a series of M quantitative values q1 · · · qmbounded by TREi and TREj. These events and quantitative values shouldhave time intervals respectivelyMore precisely, the most rudimentary form of QREtimed can be explainedas QREtimed = TRE1 R[x1, x2] TRE2 where R is a set of real numbers asmeasurements and〈x1, x2, · · · , 〉 ∈ R represents time stamp.The definition of Binding, Support Potential, Support, and Confidenceexactly follows the same definition from QMine. Similar to QMine, we decreasethe value of confidence from 100% due to the presence of imperfect traces ina real-world application.3.2 MethodologyIn this section, we discuss the architecture of our MMTQ framework. Fig-ure 3.1 provides a high level working for our MMTQ framework.The MMTQ framework takes two inputs: a real-world trace which is in-ternally converted to a valid QTracetimed and a valid QREtimed. In situationswhere the input is a valid QTrace, time-bound restrictions in QREtimed canbe suppressed using [-1,-1] as the constraint.MMTQ begins by forming a finite state machine using the given QREtimed.We use Ragel2 for implementing the finite state machines along with time in-terval checks. Ragel provides precise control over the matching of patterns.The advantage of such granularity enables us to manually track each mea-surement as they occur between two TRE instances. For each valid QREtimedinstance, we simultaneously store them in a central database (DB). Addition-ally, the user provides a valid query (pattern of interest) to MMTQ whichthen finds all matching instances from the DB. A query is valid if it complies2http://www.colm.net/open-source/ragel/253.2. MethodologyFigure 3.1: MMTQ Worklfow263.2. Methodologywith the initial specification template, QREtimed supplied to MMTQ. In or-der to increase the scalability of our framework, MMTQ internally divides thestreamed QTracetimed into smaller chunks. These chunks are processed ondifferent threads since the correlation of one chunk over the other is mutuallyexclusive. Such parallelism enables a near real-time monitoring experiencethereby enabling MMTQ to successfully mine as well as monitor for suchpattern of interest. Moreover, the patterns stored in DB can be used for fur-ther analysis, if not real-time, thereby completely eliminating the necessityof re-mining for such patterns. In Figure 3.1, the term Encoder and Decoderrefers to the parsing of raw input trace to QTracetimed and that of changinghuman-readable user query into that understood internally by the frameworkrespectively.Currently, MMTQ supports µ (mean), σ (variance), min, and max althoughit can be overloaded with any statistical operation to allow user to analyze theirsubject of interest.Algorithm 4 provides a general overview of the internal working of the sys-tem. Initially, QTracetimed and QREtimed is provided as an input to MMTQalong with connection to a database and the alphabet set Σ. Using Ragel,MMTQ generates a FSA representation of QREtimed and initializes all threadswith the same along with the connection to the database. Then it proceedssubdividing QTracetimed into smaller valid chunks and thereby offloading themining task to the available threads.Algorithm 4: minePropertiesInput: QTracetimed,QREtimed, alphabet Σ, DBResult: Mined propertiesGenerate a generic formulation for QREtimed from ΣInitialize the Finite State Acceptor (FSA)Initialize all threads with DB and the FSASplit QTracetimed into event-segment and time-segmentforeach segment ∈ QTracetimed dosegmentMine (segment, DB, FSA)endAlgorithm 5 takes as input such valid chunks and executes on individualthreads. Initially, MMTQ searches for valid QRE patterns and eventually,upon successful match, it further validates the time-bound within and acrossTREs. A pattern is classified a ‘valid’ match only if it agrees entirely with thegiven QREtimed. All valid matches are subsequently inserted into DB therebyenabling MMTQ to mine for all valid patterns.All threads maintain mutual exclusion with respect to the database, DB.273.2. MethodologyAlgorithm 5: segmentMineInput: QTracetimed, DB, FSAResult: Mined property the subsegment of QTracetimedaction EVENTrecord patterns for QTracetimed Segment matchrecord event entry & exit timestamp onceaction NUMpush digit to DBaction FINISHmatch overall patternvalidate timeframe within and among eventif valid thenpush DB into global shared spaceupdate instance countsreturn TRUE // Accepting Stateelsegoto action ERRORendaction ERRORremove inserted values from DBreturn FALSE // Error State283.3. DiscussionEach thread executes instructions in their own memory space. The controllerfor the thread enters records into the DB as soon as the FSA reaches anaccepting state. Synchronization lock is enabled for any operation involvingthe database thereby preventing a possible race condition over the shared DB.Moreover, each valid QTracetimed segment is processed by one and only onethread during the entire mining process as a result MMTQ never runs into arace condition.3.3 DiscussionSoundness and completeness are two measures that are highly interrelatedin the logic inference system. While the soundness of an algorithm states itsdegree of a true result, completeness addresses all possible inputs and doesnot miss any. Since MMTQ mines all possible valid QREtimed instances fromthe system trace, we claim that our algorithm is sound and complete. This ispossible because of our finite state acceptor which would reach an acceptingstate only if the sub-sequence complies with the time-bounded as defined inQREtimed. Moreover, we break the entire trace into chunks of similar patternsizes thus considering all overlapping sub-sequences that could occur within thewindow transition. This makes sure that we cover all possible sub-sequencesof events that would have, ideally, met a satisfying condition. Our algorithmcontinuously keeps track of success rates for each valid pattern instances in DBwhich can be used to calculate the confidence and support value. Given thatour algorithm is sound and complete, it follows that the reported confidenceand support values would also be valid. Thus our algorithm satisfies confidenceand support constraints for any mining specification.3.3.1 Memory RequirementsIn this section, we would discuss the time and space complexity of ouralgorithm. The storage requirement for the database is influenced by τ and Σ.Since the generated FSA mines for all possible patterns thus a higher value ofτ would exponentially increase the space complexity. In such a case, a total ofΣτ TRE instances could be possible which would occupy O(Στ ) space to holdthe acceptor results.A higher value of τ would ideally suggest complex relationships between alarge number of events. However, the majority of properties of interest repre-sent relationships among a few events only [YEb, DAC99]. Hence realisticallythe dimension τ of the matrix will remain small.The number of unique events Σ in the trace will depend on the nature ofthe system. While, we do suggest reducing the number of events of interest toa lower degree, by filtering off the irrelevant cases, in a situation of a complex293.3. Discussionsystem this might not be a practical solution. However, increasing Σ wouldpractically not have any drastic effect on the execution time.Since the generated FSA is generic in nature with respect to QREtimed,the storage requirement for the finite state acceptor thus used would be con-stant. We begin by calculating an upper bound for the number of place-holders required to represent our Σ. For example, a regular expression of[a−z][0−9]{2} would accommodate 2600 unique events. Thus a TRE such as〈0.(1.2)+〉[0, 0] can be represented as eventSeq (eventSeq eventSeq)+ whereeventSeq = [a− z][0− 9]{2}. It must be noted that the given QREtimed mustbe deterministic in nature. Eventually, using basic pattern matching withthe stored mined properties and the query, we provide the ease of mining forany complex event pattern that might be of interest. However, a majority ofinteresting properties will remain simple [DAC99].Lastly, the storage requirements for the trace are equivalent to the lengthof the trace. Our mining approach examines one event from the trace at atime as a result we do not store any past or future events. Thus the spacecomplexity for MMTQ is O(L).With growing trace size L, τ , and Σ, MMTQ must handle numerous chunksand complex patterns. Due to our generic FSA, MMTQ is only affected bythe size of the database. However, as previously discussed, in practice thiswill not be a concern since properties remain relatively simple as shown in theevaluation section with industry grade case studies.Table 3.1: MMTQ ComplexityComplexity AnalysisTime O(τ + L)Space O(Στ + L)Execution O(τ + L/(th-count) +thoh)Table 3.1 shows the space and time complexity for MMTQ. Execution com-plexity refers to the time taken for parallel execution whereas time complexitystates the theoretical time bound for the same. Expression thoh represents themulti-threading overhead in system. It is important to highlight at this pointthat the time and space complexity of MMTQ is linear with respect to thelength of the trace which makes is a promising approach when mining overlarge system traces.303.4. Evaluation3.4 EvaluationWe also demonstrate the strength of our system using synthetic traces.Our machine runs on Ubuntu 18.04 (64 bit) using GCC version 7.5.0 withunderlying specification of a single quad-core Intel i7-2630QM CPU clockedat 2.0 GHz and 8 GB system memory. Our framework along with test dataset is avalaible online3. For performance and scalability analysis, MMTQis evaluated by varying combinations of QREtimed, trace lengths, and time-bounds on the synthetic trace files. Experimental analysis of MMTQ usingreal-world traces is presented in Chapter 5.3.4.1 Evaluation using Synthetic TracesWhile system trace provides a reasonable understanding and aids in strength-ening the purpose of an algorithm, scalability and its complexity are also im-portant parameters that must be measured. To verify our algorithm againstextreme load and complexity we run experiments using synthetic traces withvarying parameters.Using synthetic traces, we present our validation on scalability and perfor-mance using by changing the few parameters such as τ , alphabet size Σ, andlength of QREtimed. We record the memory and time requirements for ourMMTQ.Setup (Mine Time): We evaluate the scalability of our framework withrespect to the trace length and the alphabet size.Figure 3.2 presents comparison for time taken to mine based on total eventcount. For this experiment, we reduced our alphabet Σ = 26 and τ to 2 whilevarying the number of events in the synthetic log. Our prime interest is indetermining the impact of the larger amount of events on the mining time. Wereplicated our experiment 10 times to ensure reproducibility and reliability inour results.Figure 3.2 shows the QREtimed scales linearly with increase in trace length.Figure 3.3 we present the scalability analysis of QMine by varying thealphabet length Σ and keeping other parameters such as the dimensionality ofQREtimed, τ = 2 and length of the trace L = 10, 000. Interestingly, MMTQshows a very slight increase in mining time as alphabet size is increased. This isdue to our pattern tracking capability over individual segments and eventuallygenerating all possible patterns that adhere to the given time bounds as earlierspecified. The slight increase in duration could be accounted for various otherfactors such as occupancy of other process threads in the system.The results of Figure 3.3 and Figure 3.2 provide empirical evidence for thecorrectness of our space-time complexity analysis. The time complexity of our3https://github.com/AnonymousDS/TQMine313.4. EvaluationFigure 3.2: Varying total number of eventsFigure 3.3: Varying distinct eventalgorithm is linear with respect to the length of the trace (L) while linear withrespect to the number of place holders (τ).32Chapter 4MINTS: A semi-supervisedTemporal Specification MinerIn the previous chapters, we explored our mining algorithm specificallybased on template-based specification mining. Template-based specificationmining has gained considerable prominence [LLb, WGY]. In template-basedspecification mining, a user-defined template is fed into the model as inputthat matches similar patterns from the system traces. Specification miningis useful in software engineering for verification [ES], generalization of systembehavior [LPBa, Lo], anomaly detection [LLb], etc. However, Template-basedextraction of temporal properties is difficult and tedious. They are majorlybased on expert domain knowledge [UFAMa, UFAMb, Ulu] or are restrictivedue to poor customization during mining [NCJF, MN]. Moreover, due tothe evolutionary nature of software development, template-based temporalmining requires a constant update with every software modification. With therequirement of domain knowledge, the use of such template-based specificationmining gets limited. Both QMine and MMTQ suffer from these limitations.Timed Automata (TA) [BY] is a Finite Automata extended with clockvariables and added constraints on the state transitions. State transitionsare restricted with time bounds on the events. As a result, the system statechanges only when the occurrence of the event is satisfied by the time-bound.TA is primarily used in the field of formal methods and software engineeringsuch as model-testing [WN], system verification [ES], testing control flow incommunication systems [DKEB], computer-aided process engineering [SSE],etc. TA is also used in safety-critical systems such as medical devices, auto-mobiles, safety equipment [WN, MRA+a], where the occurrence of an eventand the timing of the event is of paramount importance.A direct solution to the requirement of domain knowledge for template-based specification mining is the extraction of workflow. The term workflowmeans the internal functioning of the system and can be represented usingsequence diagram, finite-state machine [LLb, Ulu], etc. Finite-state machines(FSM) are a rich graphical representation of a system workflow. FSM canbe used as a reference for sequence diagrams. The extraction of a finite-statemachine is predominantly carried out in an unsupervised fashion. Previousstudies (refer [WGY, LLb, Ang87, ACZ+20]) used various approaches to ex-334.1. Related Studiestract FSM from system logs. However, to the best of our knowledge, no workhas been done to extract timed automata in an unsupervised fashion.In this chapter, we propose a novel unsupervised specification mining tech-nique. Our framework takes a set of system traces and builds a custom timed-trie network. Less frequent patterns are filtered out and only the most recur-rent patterns are retained in the final system representation. The trie networkcontains nodes and edges, representative of system state and transition amongstates respectively. Edges define the necessary event with the clock constrainton the event. Our framework can be used to extract the most frequent tem-poral patterns or be used as a runtime monitor to detect anomalies.We begin by defining a trace, state machine with time-constrained eventtransition, and trie data structure. We then explain the construction of ourcustom-timed trie along with custom pruning to filter and strengthen themodel. Multiple pruning steps are applied to extract only the dominant pat-terns. We use association rules of support and confidence for pattern extrac-tion.This chapter is structured as follows, in Section 4.1 provides an overview ofthe current research in the domain of temporal specification mining. Section4.2 briefly introduces few notations necessary for the understanding of ourframework. Section 4.3 explains the various components and working of theframework followed by discussion and experiment in Section 4.4 and Section4.5 respectively.4.1 Related StudiesModeling system using finite state machines is a well-studied topic [tre,UFAMb]. In [Ang87], Angluin presented an approach to learn system be-havior. It uses a series of queries and counterexample to infer the hiddenautomaton. It follows a pattern of Minimally Adequate Teacher where thelearner tries to find the abstract representation of the system that the teacheris only aware of. Regular language expresses these abstract representations ina relatively simple form [LLb]. Few recent studies [LLb, WGY] used varia-tions of regular languages to model system behavior. [tre, LPBa], uses patternmatching while [WGY, ACZ+20] studies the system behavior in the form ofregular expressions. In [Vaa], Vaandrager uses a Mealy Machine [SG] as aminimally adequate teacher along with a MAPPER that provides a deter-ministic output for any given input. The primary role of the MAPPER is toperform a translation between input and output states. Similar approacheshave also been proposed in [AJU, ACZ+20].Alternatively, Input-Output Automata (IOAutomata) are used to modelthe system behavior of a distributed network. IOAutomata uses actions such344.2. Preliminariesas input, output, and internal activities to establish the relationship betweendifferent components. In [AV], the author uses IOAutomata as a teacher andtrains the Mealy machine to learn the target black-box model’s workflow.The notion of time can be naturally extended using Timed Automata.Timed Automata (TA) include the clock constraint over the transition edgebetween each state. In [tre], Alur proposed the concept of timed regularexpressions. Timed regular expressions are an extension of regular languageswith the knowledge of time. In [Ulu, UFAMa, UFAMb], Ulus et al. extendedtimed regular expression to define timed derivatives. In Formal logic, deriva-tives are a very neat algebraic tool used to build computation models. Thebenefit of derivatives is in the speed for sequential computations. Since timeseries is a form of a continuous stream of non-decreasing discrete timed data,extending derivatives with a set of timed relations is novel [UFAMa]. MON-TRE [Ulu] uses timed derivatives to perform real-time pattern matching withtime bounds. Albeit coming up with pre-defined timed relations is challenging.In [MN], the authors propose QMine, a framework for mining quantitativeproperties from system traces. Quantitative properties are associated withevents and numerical measurements in the system traces. These propertiescan be used to not only understand system behavior but also assists in taskssuch as anomaly detection, runtime monitoring, intrusion detection etc. Nev-ertheless, quantitative regular expressions do not consider timing constraintsexplicitly. Cutulenco et al. in their work [NCJF] proposed an approach tomine system properties using user-defined templates in the form of timed reg-ular expressions. Yet due to the rapid expansion in the software developmentlifecycle the necessity to update these templates becomes tedious.In [PMM17], the author uses timed k-tail (TkT) to create a timed au-tomaton. A set of traces are collected from a software system and for eachtrace, an automaton is generated. The automaton uses a relative clock forthe clock constraint function and the final step involves merging all the au-tomatons. The clock constraint is then generalized for the merged automaton.The final timed automaton represents the states in the software system. TkThas promising experimental results yet has high time complexity due to de-pendency on multiple traces. In this work, we present an approach to minetemporal properties with no apriori knowledge about the system behavior.Our approach scales linearly with trace size.4.2 PreliminariesFinite State Machine (FSM) [ACZ+20] are used to model system interac-tions among various sub-components. System behavior is generally modeledin terms of a directed graph. G : {V,E} where system states are represented354.2. Preliminariesby vertices V while edges E represents the relationship between the two con-necting states. FSM helps explain complex system behaviors in explainablegraphical representations thereby assisting in troubleshooting for bugs, fasteronboarding of new developers, and identifying system specifications among afew. There are two variants of FSM, namely deterministic finite state machines(DFA) and non-deterministic finite state machines (NFA). In NFA, transitionamong states is not unique as a result multiple outcomes are possible howeverDFAs are deterministic in nature. In this work, we focus only on deterministicfinite state machines.Timed Automata [ACZ+20] are an extension of Finite State Machines withthe addition of time constraint over the transition function. More formally,a one-clock timed automata contains a clock variable c along with a set ofconstraints φc : >|c  i where  = {<,=, >,≤,≥} and i ∈ N. We use > torepresent true while ⊥ denotes false for {>,⊥} ∈ B. The clock is set to zerowhen φc evaluates to > or is left unchanged in the case of ⊥. Timed Automatacan be represented as A = (Σ, Q, q0, F, c, δ), where Σ is the set of alphabetswhile Q is a finite set of states, q0 ∈ Q is the initial state, F ∈ Σ are the setof accepting states and δ is the transition function along with c as the clockvaluation. The transition function (δ) can be expressed as δ(qi, α, ct) → qjwhere {qi, qj} ∈, α ∈ Σ and ct : >. δ(qi, α, ct) → qj implies that the systemreaches a state qj from qi due to an action α within a valid clock constraint,ct. ∆t denotes the time taken to transition from the present state to the nextstate. We consider a clock constraint to be valid if the ∆t is within the clockinterval [m,n] where {m,n} ∈ N.A path defined as ρ : q0(α1,c1)−−−−→ q1 (α2,c2)−−−−→ q2 (α3,c3)−−−−→ · · · → qn, implies atransition sequence from the initial state q0 to the final state qn through thecourse of multiple valid actions within its time constraints. A path is calledaccepting, if the final state is an accepting state. Paths are representativeof one complete execution. A trace is a set of path, = {ρ1, ρ2, · · · } where{ρ1, ρ2, · · · } are execution paths.Clock valuation function, ct = ct−1 + δ where δ ∈ N denotes continuousnon-decreasing unit of time. Moreover, clock valuation can be representedin the context of a global clock or a local clock. In the case of a local clockvaluation, after every transition the internal clock is reset to 0. In our work,we use the clock valuation in the context of local clock unless otherwise stated.Trie is a common and famous data structure mostly referred to as an n-arytree. Each vertex contains multiple edges to its successor vertices. However, atrie data structure does not contain a closed loop. Trie can be representativeof a non-minimal finite state machine. We use such a representation to learnand extract dominant patterns from the system. Depth (d) of a trie is the364.3. Methodologymaximum distance from the root to its leaf nodes.d = argmaxρj , ∀j ∈ (4.1)Association rule mining measures the degree of a pattern association againstthe entire trace. Support and confidence are two common ways to measureassociation [ABC]. Support measures the probability of a certain patternagainst all possible pattern lists while confidence measures the likelihood ofthe pattern given part of the pattern has already occurred.4.3 MethodologyFigure 4.1: MINTS FrameworkOur Timed-Trie (Trietimed) representation is a special type of Timed-Automaton (TA). Trietimed consists of nodes and edges representing statesand transitions with clock constraint. This section explains the constructionof the Trietimed. There are 4 components for extracting the Trietimed froma system trace. Fig 4.1 provides the overall framework for our proposed ap-proach. We discuss each component briefly in the following sections.4.3.1 Formation of the TrietimedMINTS builds the Trietimed using system traces. System trace is cleanedand pre-processed before feeding as input to MINTS. Processed trace mustcontain events and the time associated with the events. Alphabet set consistsof unique events present in the trace. Additionally, 2 hyper-parameters must374.3. Methodologyalso be provided into the framework, that are depth D and threshold ρ. Ddescribes the maximum depth of the generated Trietimed and threshold ρ isused for pruning of branches (explained in Section 4.3.2).Algorithm 6 provides an overview of the steps required to build the Trietimed.Trietimed is constructed progressively. At every step, a window of size d slidesover the trace. For each window, the segment of the trace is used to buildthe Trietimed. tracesubd denotes a subtrace formed with a window of size d.A trace can contain multiple window instances of size d, therefore multipleinstances of tracesubd would be formed. Since the window slides by 1 event ata time, the segments overlap with the neighboring window. This iterative useof adjacent segments helps retain the transition of events among the window.Once all the segments of size d are processed, the framework increments thevalue of d. The construction begins with d = 1 and terminates at d = D. Line6 - 6 and Algorithm 7 outlines the above-mentioned steps.Algorithm 6: buildGraphInput: trace, DResult: Trietimedroottrie ← NULLforeach d in [1, D] doforeach Segment of trace of length d (tracesubd) in trace dotraverseAndBuild(roottrie, tracesubd , 0)endevaluateAtDepth(roottrie, d)endreturn roottrieHowever, before incrementing the window size d, all the leaf nodes of theTrietimed are processed. The processing step involves evaluation of the clockconstraint (c) and is outlined in Algorithm 8. Trietimed stores the events onthe edges along with the transition time difference from the parent node tothe child node. Nodes represent states that the system may undergo duringexecution. These records of transition time are used to find the time bounds(i.e min and max) for the clock constraint. Although MINTS uses the rangedefined by 2 standard deviation(σ) across mean(µ) to evaluate the bounds,users can override the evaluation function. Using such a range helps in filteringoff the outliers and covers 95 % of the data set. For brevity, in this paper werefer to such a range as partially complete range (denoted by `a). A directapplication of such time-bound is in the field of anomaly detection whereevents with abnormal transition time deviate significantly.Transitions that occur outside the time bounds are dropped and only thevalid transitions are used to estimate the probability of transition from parent384.3. Methodologystate to the child state for the given event (Line 8) (explained in Section 4.3.3).It must be noted that MINTS assumes that the system spends approximatelythe same amount of time in the current state before transitioning to the nextstate.Algorithm 7: traverseAndBuildInput: nodetrie, tracesubd , posif pos < len(tracesub)− 1 thenFind the state node, nodechild for transition event e at pos intracesubdif ∆t satisfies constraint ct thenRecursively call traverseAndBuild(nodechild, tracesub, pos+ 1)elseReject traversal (to drop the outliers) and returnendelseif nodetrie does not contain state with transition event e thenCreate and add a state node newNodetrie with transition evente as a child to nodetrieendend394.3. MethodologyFigure 4.2: Sample Representation of TrietimedFigure 4.3: Clock constraints are evaluated at depth 2404.3. MethodologyFigure 4.2 shows a sample illustration of an intermediary step involvedduring the construction of our timed trie network. For each transition, MINTSrecords all the ∆t transition time steps between the events.4.3.2 PruningBefore proceeding with the extraction of dominant properties and the prob-ability analysis, we ensure our model is representative of the most prevalentpatterns. Therefore, we filter off all the traversal paths for which ρ ≤ P. Thisis accomplished by only selecting those timed transitions which fall under theempirically evaluated distribution.Algorithm 8: evaluateAtDepthInput: nodetrie, dwhile desired depth is not reached doKeep traversing downendEvaluate mean (µ) and variance (σ) using the list 〈time− list〉Update the permissible range 〈tmin, tmax〉 for nodedepthtrie with the rangecontaining 2 standard deviations (σ) of 〈time− list〉 ( nodedepthtrie← 〈µ− 2σ, µ+ 2σ〉)Update nodedepthtrie with the transitions where ∆t is within range〈tmin, tmax〉Compute the probability of transition (Pte)More formally, a normal distribution is defined and stored within eachnode’s clock constraint c (Refer algorithm 8). The normal distribution isevaluated using all recorded transitions at this transition step and therebythe outliers are filtered off to reduce the formation of transition for the nexttime step. It is common to use an acceptable transition time to be within the`a (refer line 8 in algorithm 8). We do acknowledge, that this step, in turn,could reduce precision (in terms of validity of event transitions), however, theprimary objective of MINTS is to extract the dominant patterns.414.3. MethodologyFigure 4.4: Determination of clock constraint424.3. MethodologyFigure 4.4 shows the steps involved in measuring the clock constraint4.Please note, the interval constraint objective function can be changed by theuser and it is not necessarily fixed on IQR. Figure 4.3 displays the graph withclock constraint c after evaluation. Moreover, since the clock constraint isevaluated before the construction of the network at the next depth, only apartial trie network is filled with c.4.3.3 Event PredictionThe real-world performance of a model measures its effectiveness. Given asequence of events, many machine learning models, such as Recurrent Neuralnetworks (RNN), Long-Short Term Memory (LSTM) [AAGES], can be usedto predict future events. Although these models have high accuracy, they lackthe capability to represent the learned behavior. While FSM can represent thesystem workflow with nodes and edges, modeling the system workflow requiresdomain knowledge. MINTS builds a TA that can be used for various taskssuch as even prediction.Algorithm 9: probabilityOfTransitionInput: nodetrie, tracesubdwhile desired depth is not reached doKeep traversing down with tracesubdendComputer the overall time-interval for all event, e ∈ Σforeach t in 〈time− interval〉 doforeach event e ∈ Σ doCompute probability of transition at time tendendReturn the overall Transition Probability for each event in the〈time− interval〉Algorithm 9 outlines our event prediction approach. Trietimed stores thetotal count of valid transitions from each state (except the final states). Thetransition probability for each event (i.e edge) is computed and stored in thenode. The transition probability assists the framework to predict the nextevent. Moreover, since all the transition times are recorded, MINTS is capableof predicting an event with ∆t time step in the future.4Normal Distribution Image Credit: By Jhguch at en.wikipedia, CC BY-SA 2.5 https://commons.wikimedia.org/w/index.php?curid=14524285434.3. MethodologyFor example, if there exists 3 transitions from state q3, namely for event〈{a : [1, 2, 2, 2, 3, 3]}, {b : [2, 2, 3, 3, 4, 5] {c : [1, 1, 3, 5, 5, 5]}〉, then in such caseP1a = 1/3 = 0.33, P2a = 3/5 = 0.6, P3b = 2/5 = 0.4 and so on, where Pte repre-sents probability of transition to event e at time t. This process is repeated forall time steps and eventually, we obtain the event transition probability overtime for all the states q3. Figure 4.5 presents the output from event predictionmodule of the Trietimed .4.3.4 Dominant Property extractionAdditional PruningAlthough our model, at this stage, has been pruned once (refer section4.3.2), we employ additional indirect pruning to avoid extraction of irrelevantproperties. We classify such pruning as indirect since the approach does notexplicitly prune the branches of our Trietimed, yet, it only permits traversalover fewer paths.Figure 4.5: Event PredictionOur model takes a hyper-parameter, P which determines the thresholdover the probability of transition. Only those branches, from the root node,are considered which contain a minimum Pte above P (refer expression 4.3.4).argminjPj , ∀j ∈ ρi (4.2)444.3. MethodologyAlgorithm 10: pruneTreeInput: nodetrie, Pforeach child of nodetrie doif Pchildnodetrie < P thenPrune the stem i.e childelseRecursively call pruneTree(child, P)endendThe method is effectively a depth-first traversal from the root node.Algorithm 10 provides a brief overview of the steps involved in pruning thetree. The main idea is to remove all the stems which has Pte less than the userdefined P. This helps in exposing the dominant patterns.Table 4.1: Temporal Properties used for mining in MINTSName Property TemplateResponse [-P]*; (P; [-S]*; S; [-P]*)*Alternating [-P,S]*; (P; [-P,S]*; S; [-P,S]*)*MultiEffect [-P,S]*; (P; [-P,S]*; S; [-P]*)*MultiCause [-P,S]*; (P; [-S]*; S; [-P,S]*)*Temporal propertiesTemporal patterns have been well studied by Yang and Evans [YEc]. Intheir work, 8 most common and relevant patterns have been suggested for tem-poral property mining. We have evaluated our algorithm with 4 such patternswhile the option of extending such properties with user-defined properties hasbeen provided. Table 4.1 presents the temporal properties that were usedfor the evaluation of our MINTS framework. The time bounds for the givenproperty template applies within the central enclosed sequence of event. Forexample, for Response temporal pattern, a possible time-bounded expressioncould be [−P ]∗; (P ; [−S]∗;S〈x, y〉; [−P ]∗)∗ where x and y are the start andend of the time interval.454.4. Discussion4.4 DiscussionComplexity AnalysisAlgorithm 11 is use in the construction of Trietimed. The program takes asinput, the trace along with the window length of subsequent events, d. Wedenote D as depth since it defines the maximum height of our Trietimed.Moreover, algorithm 11 also takes Σ as input, however for simplicity, weavoid representing it in our minimal representation for Trietimed generation.Algorithm 11: Abstract Representation of Trietimed GenerationInput: trace, DResult: graphtimedforeach depth d in D dosubtrace← { set of all segments of length d from trace }foreach subtracei in subtrace dotraverse and build the Trietimedendevaluate and prune the weak stems at depth dendreturn roottrieFor each depth d ∈ [1, D], we traverse and build our Trietimed. For a givendepth d, line 11 extracts all subtraces of length d from the input trace. Thisoperation takes O(n-d) time while traversal and building of the Trietimed(line11 - 11), for level d, takes constant time i.e O(1).We also store ∆t, i.e the relative time for the current action from theprevious state. Line 11 performs pruning for stems at depth d using the IQRrange. This time bound can be defined as [µ − xσ, µ + xσ], where µ and σare the average time step and the standard deviation over the stored list of∆t while x is a constant used to define the range, for example x = 1 defines arange within 1 standard deviation.This takes constant time, O(1) however since there are Σd stems at depthd, thus the entire operation takes O(Σd) time.Total time for step d = n− d+ n− d+ Σd= 2n− 2d+ Σd≈ n− d+ Σd(4.3)464.4. DiscussionThus, the overall time complexity until depth D can be expressed asTotal time =D∑d=1(n− d+ Σd)=D∑d=1n−D∑d=1d+D∑d=1Σd≈ nD −D2 + ΣD(4.4)Although the equation 4.4 contains an exponential term ΣD, it must benoted that with each pruning being performed at step d, the next iterationfor step size d + 1 would skip traversing those stems that were already beingpruned at step d. Moreover, a large value of D does increase the uncertainty ofthe learned behavior. However, the worst-case complexity do stay at O(nD−D2 + ΣD).Feature ComparisonTable 4.2 provides a brief overview of few specification mining algorithms5.UPPAAL-SMC [DLL+15] (an extension of UPPAAL) is a statistical modelchecking tool and is widely used for real-time verification of systems. InUPPAAL-SMC, the real-time system must be modeled before performing spec-ification verification. Linear-time Temporal Logic (LTL) is a propositionallogic modeling approach with timed modalities. Modalities can be of twotypes, future modalities (always, until, eventually, next) and past modali-ties (historically, since, once, previously). Texada [LPBa] is a popular LTLSpecification mining tool. However, Texada lacks representation of the ex-tracted specification as State Machines. The approach presented in [WGY]and [ACZ+20] are fundamentally based on the concept of Active Learning andextract a neat representation of the system in the form of a State Machine.Yet, the time complexity of these algorithms is very high to be considered forpractical use. MONTRE [Ulu] is a rich tool for timed pattern monitoring al-beit it requires a monitoring template as input. TRE Automaton [NCJF] andQMine [MN] suffer from a similar problem with a requirement of a mining tem-plate. MINTS successfully overcomes all the above-mentioned shortcomingswhile being highly scalable for real-world applications.5Only the most relevant algorithms are compared474.4. DiscussionTable 4.2: Comparison of various specification minersAlgorithm(Author names used ifalgorithm has no name)FeaturesPatternExtractionTimed PatternExtractionPatternMonitoringTimed PatternMonitoringDFA Extraction Timed DFA ExtractionProbabilityEstimationUPPAAL SMC [DLL+15] X X XTexada [LPBa] X XWeiss et al. [WGY] X X XJ. An et al. [ACZ+20] X XMONTRE [Ulu] X XCutulenco et al. [NCJF] X X X XQMine [MN] X XMMTQ X X X XMINTS X X X X X X X484.5. ExperimentCorrectnessIn this section, we formally show the correctness of our algorithm.Theorem 4.1. Let trace denote the system trace while TrieDtimed representthe extracted Timed Automaton in the form of our custom timed Trie datastructure and D denotes the depth of TrieDtimed, then TrieDtimed is formallycorrectProof We will prove by induction that TrieDtimed is formally correct.Base case: When D = 1, Trie1timed has only 1 root node (or the initialstate) and Σ children where Σ denotes the alphabet set.Induction Hypothesis: Let Triedtimed is correct where 1 < d < DInduction Step: Since Triedtimed is a Trie data structure (also referred to asprefix tree), it can be stated that the formed tree at depth d corresponds toall prefixes (or sub-segments) of length [1, d]. It must be noted that not allsub-segments of length d must be present in Triedtimed however the reverse istrue. This is because, during pruning, MINTS drops the segments that arerarely traversed. Nevertheless, all the prefixes formed from the [1, d] mustalways be present in trace.In the next iteration for d + 1, MINTS extracts all the segments of sized + 1. It then proceeds with appending leaf nodes at depth d + 1 providedthe prefix of the segment is valid and can be traversed from the root node.Subsequently, MINTS performs pruning to remove any path traversal thatwere rarely traversed. Thus the final Tried+1timed is formed and is correct sinceall the prefixes present in Tried+1timed can be found in trace.Therefore, Triedtimed is formally correct for all d ∈ [1, D].4.5 ExperimentIn this section, we discuss the performance, scalability, and efficiency ofour approach. We used a synthetic data set to evaluate our framework. Ourimplementation is available online6. All experiments were carried out in asingle quad-core Intel i7-2630QM CPU clocked at 2.0 GHz with 8 GB systemmemory and running on Ubuntu 18.04 (64 bit) using GCC version 7.5.0 andPython 3. Unless otherwise stated, each experiment was replicated 10 times,and the mean value was recorded. We request the reader to refer to Chapter5 for experimental analysis using real-world trace.6https://github.com/AnonymousDS/timedStateTrie494.5. Experiment4.5.1 Evaluation using Synthetic TraceFigure 4.6: Trace length vs extraction timeReal-world traces provide practical use cases for a framework. We mea-sure the scalability of the framework on synthetic traces. We used multiplesynthetic traces by varying the three parameters namely, alphabet size(Σ),length of pattern during mining (as depth D of the trie), and length of thetrace (L). Such comparison offers a better understanding of the scalability ofa framework over space and time. We mined for the dominant and temporalpatterns (refer Table 4.1) while keeping P = 0.50. Below we describe eachsetup and its finding in more detail.Setup 1: Real-world traces are large. Understanding the relationship ofthe trace length L over time, while keeping depth and alphabet size constant,is important to determine the scalability of a framework. Therefore, for thisexperiment, we kept D = 5, P = 0.50 and Σ = 10Figure 4.6 presents the relationship of trace length over time. It is evidentthat MINTS scales linearly with time while varying the trace length.Setup 2: In this setup, we were interested in understanding the strengthof the framework while mining for longer patterns. The intent is to learn longtemporal patterns. Therefore, while keeping the length of trace constant at100000 events and comprising of 10 unique events (Σ = 10), we altered Dfrom [3, 30]. It must be noted that prediction accuracy decreases as futuretime horizon increases. Therefore, we kept the upper bound of D = 30.As evident from Figure 4.7, MINTS grows almost linearly over time byvarying the length of the extracted pattern. This does corroborate our the-oretical finding of ≈ O(ΣD + nD). The effect of exponentiation over Σ isminimal since Σ in practice is a small value.504.5. ExperimentFigure 4.7: Depth of TrietimedFigure 4.8: Increasing alphabet size514.5. ExperimentSetup 3: Finally, we generated multiple synthetic traces of length 100000events while altering the alphabet size. Depth D was kept at 5. Such exami-nation helps understand the efficiency of our framework in situations involvinga large number of events. Figure 4.8 displays the relationship of varying thenumber of unique events against time.As apparent from Figure 4.8, MINTS grows linearly with respect to timeas shown in Section 4.4. Therefore, it can be stated that MINTS do indeedexhibit ≈ O(Σ) while D and L are kept constant.Figure 4.9: Sample illustration of Trietimed with depth as 5As discussed in Section 4.4, experimental analysis establishes the scalabil-ity of our framework. Figure 4.9 provides a sample illustration of the learnedtimed model from our approach. While the nodes represents the states, theedges represents 〈α, c,Pqiqi−1 ,Pqi 〉 where α is the event, c is the clock constraintwith the interval [a, b]∀a, b ∈ N, Pqiqi−1 as the transition probability from pre-vious state(qi−1) to the current state(qi) and Pqi as the transition possibilityto the current state considering the all possible transitions.52Chapter 5Experimental Analysis andConclusionIn this chapter, we perform experimental analysis using real-world traces.We begin with our pattern extraction framework, MINTS. MINTS is capable ofmodeling a timed automaton using just the system traces. A timed automatonthus formed, has numerous advantages and applications. The most basic beingthat of extracting temporal patterns. Hence, we use the modeled TA to extract2 properties from the system traces, namely the temporal patterns and thedominant patterns. We then use the insights of the extracted patterns toform our quantitative templates for QMine and MMTQ. In order to formthe quantitative templates, in addition to events, we also include the priorityassociated with each thread-event. By the term thread-event, we refer to thoseevents that were caused by the system thread. Apart from thread-event, ourreal-world system trace contains other events as well such as those originatingdue to function call. We use QMine to understand the change in prioritybetween threads while MMTQ to understand the change in priority with time-specific bounds. It must be noted that the results mentioned in this chapter area mere snapshot of the comprehensive result that our framework provides. Ourobjective is to demonstrate the capability of our framework while we providethe freedom to the system administrators and domain experts to better formthe specification template.We begin with experimental analysis using a real world data set in Section5.1. Section 5.1.1 provides a brief description of our problem statement fol-lowed by Section 5.1.2 that furnishes details about our data set. We then applyour models and explain the results in Section 5.1.3 followed by Conclusion andsome future work in Section 5.2 and 5.3 respectively.5.1 Experimental AnalysisWhile synthetic traces provides the feasibility to measure a system’s scal-ability and reliability in a controlled scenario, it does not provide any insightsin the practicality of a framework. A framework’s effectiveness can only bemeasured using real-world traces. While there are limitless experiments that535.1. Experimental Analysiscan be performed using countless data set available, we choose to use systemtraces from a hexacopter drone system. We used this data set to performanalysis using all the 3 frameworks. In extension to our hexacopter trace, wealso used various other real-world traces specifically for QMine and MMTQ(refer to Appendix 5.3 and 5.3). In this section, we explain our experimentalanalysis in greater detail.5.1.1 Problem StatementThe goal of our work and this thesis is to build a reliable and robustspecification mining framework. We aim to extract meaningful insights thatcould be used by the system administrators and domain experts to betterunderstand the system behavior. Therefore, for our experimental analysis, weattempt to achieve the following objectives:− Construct a timed automaton of the system using its system traces− Extract dominant and temporal specification patterns using the con-structed timed automaton− Extract quantitative specification properties− Apply time-bounds to extract time-sensitive quantitative specificationproperties5.1.2 Data setMany safety-critical systems, such as medical devices, electronic automo-biles, IOT systems, use Blackberry QNX Operating System. ONX is a real-time Unix-like operating system primarily used in embedded devices. It isequipped with tracelogger7 which assist in recording interaction within andacross the operating system. Since tracelogger operates at the kernel level,it is a useful utility to track system interrupts, inter-process communication,thread callbacks, and many more. We used tracelogger to capture such in-formation from an operational hexacopter that uses QNX operating systeminternally. The data set contains over 600 thousand events. After a few basicprepossessing, like conversion of .kev files to .csv, replacing the escape charac-ters in the event with some dummy placeholder, and sorting in non-decreasingorder of the timestamp, we applied our approach to extract interesting proper-ties. For property extraction, we considered only the Event and the associatedtimestamp while discarding the remaining features.7https://www.qnx.com/developers/docs/7.0.0/index.html#com.qnx.doc.neutrino.utilities/topic/t/tracelogger.html545.1. Experimental Analysis5.1.3 ResultsIn this section, we perform experimental analysis using the combination ofall 3 of our framework.MINTSFor evaluation and extraction of such properties, we used 4 temporal prop-erties as shown in Table 4.1. For brevity, we extracted only top 3 proper-ties from each temporal pattern, however, MINTS would present all possibletemporal properties from the system trace and rank them according to theircounts. We also extracted dominant patterns which were prevalent in theentire system along with their support and confidence measure.555.1. Experimental AnalysisTable 5.1: Hexacopter Dominant PropertiesSerial Pattern Count Support Confidence1 [-INF,0]SND MESSAGE [1373,9332]THREPLY 16234 0.029 0.9882[-INF,0]SYNC CONDVAR WAIT 82 [3222,156765]MSG SENDV 11[0,0]SND MESSAGE [576,5867]THREPLY2042 0.003 0.9993 [-INF,0]THWAITPAGE [647,1773]THRUNNING [677,6843]REC PULSE 1744 0.003 0.9144 [-INF,0]MSG READV 16 [26259,85259]MSG REPLYV 15 623 0.007 0.2575[-INF,0]MSG WRITEV 17 [2087,15713]MSG WRITEV 17[3487,20070]SND PULSE EXE113 0.000 1.000565.1. Experimental AnalysisA total of 384 properties were extracted from the system trace amongwhich Table 5.1 presents 5 interesting patterns. We kept the P = 0.45 andD = 10. We represent events and their temporal relationship as E1[a, b]E2where {E1, E2} ∈ Σ and {a, b} ∈ N. For example [-INF,0]THWAITPAGE[647,1173]THRUNNING [677, 6843]REC_PULSE represents THWAITPAGE as theinitial event followed by THRUNNING within a clock constraint c of [647, 1173]milliseconds and is then followed by REC_PULSE within a clock constraint cof [677, 6843] milliseconds. In this case, REC_PULSE is the final event in thepath ρ : q0(α0,c1)−−−−→ q1 (α1,c2)−−−−→ q2 (α2,c3)−−−−→ q3, where α0 = THWAITPAGE, α1 =THRUNNING, α2 = REC_PULSE, c1 = [0, 0], c2 = [647, 1173] and c3 = [677, 6843].Few insights from the study of these patterns suggests MSG_WRITEV opera-tions having significantly higher execution time compared to MSG_REPLY eventwhile THREPLY takes fewer milliseconds to initiate after the event SND_MESSAGE.These relationship are usually an expected behaviour since write operationsdo take longer duration compared to read and threads always communicateasynchronously which causes latency in receiving a response. Deviation froma conventional pattern can assist in detecting anomaly in a system.The measurement for support is low (this is because in our experiment,over 95% of the support measures were lower than 3 decimal places). This isprimarily due to the presence of clock constraint over the transition edges inthe Trietimed where a pattern of depth D must satisfy all the constraints in itspath. This filters majority of possible similar patterns from the constructedtimed-trie. Meanwhile, the confidence measures have a value of almost ≈ 1that explains the constant internal behavior of the Hexcopter system. Forexample, an event SND MESSAGE will always be followed by THREPLY and itsconfidence would be 1. MINTS also provides the capability to extract patternsbased on a user-defined threshold for support and confidence.575.1. Experimental AnalysisTable 5.2: Hexacopter Temporal PropertiesType From-To Event Pattern Count Support ConfidenceResponsePatternSND MESSAGE - THREPLY [-INF,0]SND MESSAGE [1373,9332]THREPLY 16234 0.029 0.988THREADY - MSG REPLYV 15 [-INF,0]THREADY [371,1246]MSG REPLYV 15 11069 0.029 0.367EVENT 2 - MSG RECEIVEV 14 [-INF,0]EVENT 0 [0,0]MSG RECEIVEV 14 1496 0.002 0.499AlternatingPatternTHRECEIVE - THRUNNING [-INF,0]THRECEIVE [306,640]THRUNNING 9040 0.068 0.996SND PULSE EXE - REC PULSE [-INF,0]SND PULSE EXE [2109,9901]REC PULSE 6886 0.015 0.110SYNC CONDVAR WAIT 82 - MSG SENDV 11 [-INF,0]SYNC CONDVAR WAIT 82 [3222,156765]MSG SENDV 11 2061 0.003 0.453MultiCauseTIMER TIMEOUT 75 - EVENT 1 [-INF,0]TIMER TIMEOUT 75 [1330,22081]EVENT 1 1490 0.002 0.452MSG READV 16 - MSG REPLYV 15 [-INF,0]MSG READV 16 [26259,85259]MSG REPLYV 15 623 0.007 0.257CONNECT FLAGS 43 - MSG SENDV 11 [-INF,0]CONNECT FLAGS 43 [824,3063]MSG SENDV 11 36 0.000 0.494MultiEffectTIMER TIMEOUT 75 - EVENT 1 [-INF,0]TIMER TIMEOUT 75 [1330,22081]EVENT 1 1490 0.002 0.452REC PULSE - BUFFER [-INF,0]REC PULSE [925,2049]BUFFER 28 0.001 0.013THWAITPAGE - THRUNNING [-INF,0]THWAITPAGE [647,1773]THRUNNING 768 0.003 1.000585.1. Experimental AnalysisTable 5.2 captures few of the temporal properties that MINTS detected(a total of 190 temporal matches were found). These results certainly helpdraw critical insights related to the behavior of the system, such as responsiverelationship for events like SND_MESSAGE to THREPLY or THREADY toMSG_REPLYV_15 to name a few. It also provides the temporal relationshipacross different temporal properties.We believe such properties would be extremely useful for system expertsand analysts in understanding along with troubleshooting system behavior.Moreover, establishing a relationship between numerous events/componentswith time does impart a better temporal understanding of the system.QMineThe internal peripherals of a hexacopter drone are relatively smaller insize compared to the peripherals found in common household desktops andlaptops. As a result, with reduced size, the total throughput of the systemalso reduces. Every operation, irrespective of how simple it can be, carries acost when executed. This is due to the limited raw power from such small IoTdevices. Therefore, each and every operation is important and must be care-fully crafted in order to not exhaust much of system resources. Moreover, suchsmall systems lack high multi-core performance due to the limited availabilityof low-powered powerful processors. Thus, much of the internal operations areexecuted using system threads. Threading provides parallelization capabilityand can be used to reduce the execution time.In this experiment, we processed the previous data set by selecting only theevents associated with a thread. Furthermore, every system thread contains apriority level. The priority level is an integer that ranges from 0(low priority)to 31(high priority). Priority level explains the importance of a thread. Athread’s importance becomes a key factor while resolving the allocation ofresources by the system in a deadlock situation. A thread with lower priority isthe last in line when high priority threads are in a blocking state. Thus, it canbe important to understand the priority level associated with each combinationof threads. The processed data set contain event and its associated priority.We used these two pieces of information to form our QTrace. We then usea simple mining template to understand the change in priority in betweentwo event. Our QRET template becomes 0.M.1 where 0 and 1 are eventplaceholders and M is the quantitative measure (in our case that would bethe priority number). Table 5.3 provides a brief overview of our mining result.For brevity, we only present a small snapshot of our mining result while theuser can obtain the entire mining outcome from our framework.Table 5.3 provides a brief snapshot of our mining effort using QMine. Asalready mentioned, QMine generates a large FSM that accepts all possible595.1. Experimental AnalysisTable 5.3: Specification Mined using QMinePattern From ToThread PriorityMean Variance Min Max Countf.[0-9]+.h THRECEIVE THRUNNING 13.02 4.81 10.00 24.00 41449h.[0-9]+.e THRUNNING THREADY 13.86 5.13 10.00 24.00 40157g.[0-9]+.h THREPLY THRUNNING 11.43 2.56 10.00 16.00 17967h.[0-9]+.g THRUNNING THREPLY 11.41 2.54 10.00 16.00 17640f.[0-9]+.f THRECEIVE THRECEIVE 33.74 65.01 10.00 255.00 38k.[0-9]+.h THWAITPAGE THRUNNING 16.00 0.00 16.00 16.00 1804QRET instances from a given QRET. In our case, we used 0.M.1 as ourQRET. Moreover, we converted all the events into a reduced form as shownin Table 5.4. The primary intention of reducing the events is to shrink thesize of the generated FSM. Since a FSM is a graph-based data structure whereeach node contains a letter from a given expression and nodes are connectedusing edges, therefore a reduced form of system event would also shrink thesize of the formed FSM. Table 5.3 shows the transition threads and the extentto which their associated priority changes. As evident, the priority levelsassociated with a thread differ during operation. Such insights can be helpfulfor system administrators to monitor system behavior and detect anomalieswhen the deviation increases than that of normal conditions.Table 5.4: Event mapping as used in QMineID Event Alphabet1 THCONDVAR a2 THJOIN b3 THMUTEX c4 THNANOSLEEP d5 THREADY e6 THRECEIVE f7 THREPLY g8 THRUNNING h9 THSEND i10 THSIGWAITINFO j11 THWAITPAGE k605.1. Experimental AnalysisMMTQIn the previous sections, we extracted the temporal pattern and then per-formed quantitative specification mining using QMine. This enabled us to un-derstand the deviation of priority level during the transition of thread eventswithin the system. MINTS provide representative knowledge about the rela-tions of the various system events along with the time of occurrence. Whilethe analysis carried out using QMine gave us insights into the change in prior-ity level among events. Yet, QMine does not consider the time of occurrenceamong the events. Additionally, we also were interested in finding the pre-ceding and succeeding events associated with such thread events. This wouldallow us to identify the specific system events that could be the prime causeof such deviations.In this experiment, we included all events however only considered the mea-surement as the thread priority value for our QREtimed expression. Therefore,our QREtimed expression becomes < 0.1 > [0, 0].M [x, y]. < 2.3 > [0, 0]. Weignored the time bounds within each TRE while considered a range [x, y] fortime bounds across TRE. Thus, we kept changing the value of x and y withan appropriate time unit. Similar to our previous effort, we transformed allsystem events into their reduced form. Table 5.1.3 shows all the system eventsand their reduced form. Additionally, we parsed our system trace into a validQTracetimed.Table 5.5: Event mapping as used in MMTQID Event Alphabet1 0x00000029 a02 0x0000002d b03 0x0000002e c04 0x00000044 d05 0x00000049 e06 BUFFER f07 CONNECT ATTACH 39 g08 CONNECT CLIENT INFO 42 h09 CONNECT DETACH 40 i010 CONNECT FLAGS 43 j011 EVENT-0 k012 EVENT-1 l013 EVENT-2 m014 EVENT-3 n0615.1. Experimental AnalysisTable 5.5: continued from previous pageID Event Alphabet15 MSG CURRENT 10 o016 MSG DELIVER EVENT 21 p017 MSG ERROR q018 MSG ERROR 13 r019 MSG INFO 19 s020 MSG READV 16 t021 MSG RECEIVEV 14 u022 MSG REPLYV 15 v023 MSG SENDV 11 w024 MSG SENDVNC 12 x025 MSG WRITEV 17 y026 PATHMGR OPEN z027 PROCCREATE NAME a128 PROCTHREAD NAME b129 REC MESSAGE c130 REC PULSE d131 REPLY MESSAGE e132 SIGNAL f133 SIGNAL RETURN 27 g134 SIGNAL WAITINFO 32 h135 SND MESSAGE i136 SND PULSE EXE j137 SYNC CONDVAR SIG 83 k138 SYNC CONDVAR SIGNAL 83 l139 SYNC CONDVAR WAIT 82 m140 SYNC MUTEX LOCK 80 n141 SYNC MUTEX UNLOCK 81 o142 THCONDVAR p143 THCREATE q144 THJOIN r145 THMUTEX s146 THNANOSLEEP t147 THREADY u148 THRECEIVE v149 THREPLY w150 THRUNNING x1625.1. Experimental AnalysisTable 5.5: continued from previous pageID Event Alphabet51 THSEND y152 THSIGWAITINFO z153 THWAITPAGE a254 TIME b255 TIMER ALARM 74 c256 TIMER TIMEOUT 75 d257 TRACE EVENT 01 e2Table 5.6 presents our experimental analysis for hexacopter data set usingour MMTQ framework. It must be noted that Table 5.6 is a short snapshotof our entire mining result. Based on initial observation, we see that count forall matched patterns has reduced substantially. This is due to the presence ofstrict time checks among the system events. The time bounds shown in table5.6 were selected arbitrarily for representation however users can select timebounds of their choice. We see a greater variation in the thread priority of 90.01between THCREATE→THRECEIVE→THCREATE→THRECEIVE. This could be due tothe severity of the thread call. It would require a deeper analysis of the systemimplementation and other factors to identify the root cause for such behav-ior. When a time-bound of [647, 1773] was applied, THREADY→SND_MESSAGEprovided an interesting insight. The said event transition occurred a total of7768 times and maintained a mean priority level of 0.04, which suggests a lowlevel of importance from the system’s perspective. However, it also exhibiteda maximum priority of 24, which is considerably higher than 0.04. This highpriority of 24 occurred approximately 12 times. This could be due to theimmediate need to pass a message from within the system. A similar resultcould be observed for THRUNNING→REC_MESSAGE when a time-bound of [0, 0]was applied. Likewise, many such observations could be made and might beof interest in the eyes of a system administrator.635.1. Experimental AnalysisTable 5.6: Quantitative Specification Analysis using MMTQPatternPreceedingEventFromEventToEventSucceedingEventTime Bound[to,from]Thread PriorityCount Mean Variance Min Maxu0.w1.[0-9]+.c1.u0 MSG RECEIVEV 14 THREPLY REC MESSAGE MSG RECEIVEV 14[0, 0]38 10.00 0.00 10.00 10.00j1.u1.[0-9]+.s0.s0 SND MESSAGE THREADY MSG INFO/19 MSG INFO 19 27 17.26 1.32 17.00 24.00w1.x1.[0-9]+.c1.u0 THREPLY THRUNNING REC MESSAGE MSG RECEIVEV 14 17591 11.52 2.61 10.00 16.00j1.x1.[0-9]+.u1.j1 SND MESSAGE THRUNNING THREADY SND MESSAGE[647,1773]10272 11.44 4.19 10.00 24.00x1.u1.[0-9]+.j1.j1 THRUNNING THREADY SND MESSAGE SND MESSAGE 7768 0.04 0.68 0.00 21.00i1.w1.[0-9]+.x1.c1 SND MESSAGE THREPLY THRUNNING REC MESSAGE 16830 11.51 2.60 10.00 16.00q1.v1.[0-9]+.q1.v1 THCREATE THRECEIVE THCREATE THRECEIVE[0,3000]18 54.00 90.01 10.00 255.00u0.v1.[0-9]+.x1.l1 MSG RECEIVEV 14 THRECEIVE THRUNNING SYNC CONDVAR SIGNAL 83 117 23.79 0.76 21.00 24.00e1.u1.[0-9]+.v0.u0 REPLY MESSAGE THREADY MSG REPLYV/15 MSG RECEIVEV 14 17427 11.40 2.54 10.00 16.00645.1. Experimental Analysis5.1.4 Comparison of Result with Baseline FrameworkIn this section, we use the baseline frameworks to compare the results ob-tained from our framework. All our frameworks, that is QMine, MMTQ, andMINTS are primarily based on 2 baseline frameworks. These are TRE (TimedRegular Expression from [NCJF]) and StreamQRE(Streaming of QuantitativeRegular Expression from [MRA+a]). Our framework does obtain additionalinsights from various other frameworks. For example, MINTS is based onextraction of Timed Automaton in an unsupervised fashion and is motivatedfrom the works of [LLb, Ulu, ACZ+20, WGY] while MMTQ is motivatedfrom the works of [AFR, YEc, LPBa]. However, these motivations are signif-icantly smaller with respect to TRE and StreamQRE and therefore we avoidour framework comparison with these baseline frameworks.QMine and MMTQ perform mining and monitoring of temporal specifica-tion patterns while MINTS extracts a timed automaton that can be used as areference for constructing a mining template. Thus, we divided the compara-tive analysis into 2 parts− Comparison of pattern mining− Comparison of pattern monitoringData set UsedFor this exercise, we used the same Hexacopter data set as defined in Sec-tion 5.1.2. Since, both QMine and MMTQ rely on quantitative measurement,therefore we primarily use thread events and include other events as precedingand succeeding elements.Comparison over pattern miningTable 5.7 presents a brief comparison of the results obtained from theframeworks in consideration. The cells marked as - were omitted due to in-compatibility with the respective framework. Moreover, only a small set ofthe patterns are shown below however our results are similar across all theframeworks, and only the nature of mining operation changes accordingly.655.1. Experimental AnalysisTable 5.7: Comparison of QMine, MMTQ and MINTS with TRE and StreamQREPatternsTime Bounds[-1,-1] if ignoredCountQMine MMTQ MINTS TRE StreamQRETHRECEIVE - THRUNNING[-1, -1]41449 41449 - 41449 41449THRUNNING - THREADY 40157 40157 - 40157 40157THWAITPAGE - THRUNNING 1804 1804 - 1804 1804THRECEIVE - THRUNNING [306, 640] - 9040 9040 9040 -SND MESSAGE - THRUNNING - THREADY[647, 1773]( on THRUNNING - THREADY )- 9012 9012 9012 -REPLY MESSAGE - THREADY - MSG REPLYV/15[647, 1773]( on THREADY - MSG REPLYV/15 )- 5581 5581 5581 -THREADY - MSG REPLYV 15 [371, 1246] - 11069 11069 11069 -665.1. Experimental AnalysisAs is evident, both QMine and MMTQ, are capable of mining all the validspecification patterns. We used TRE to validate all the mined patterns fromQMine by providing a very large time-bound (in the scale of 0 to 109 timeunit). This ensures all the patterns are extracted that satisfy the time-boundrestriction. In our case, we found such a large scale to encompass the maximumtime range and thus this ascertains that TRE does not skip any pattern. Indoing so, we were capable of extracting all the patterns that match patternsextracted using QMine. It must be noted that the presentation of output isdifferent in both frameworks. TRE outputs a success and reset matrix. successmatrix contains the count of all the matching patterns while reset containsthe count of framework reaching a failed (or reset state). QMine extracts allthe matching patterns however the result is spread across the quantitativeproperty. Therefore, the total sum of all the matching instances mined viaQMine must match the count presented in success matrix.We also evaluated our mined patterns with MMTQ by providing a validtime-bound. Similar to QMine, all the mined pattern instances matched thecount present in success matrix. We cross-validated the count evaluated fordominant patterns present in MINTS with those mined using the TRE frame-work. We found the count of patterns to match completely across all theframeworks. Hence, we state that all our framework is complete. TRE per-forms pattern mining however it lacks the capability to present the quanti-tative summary of the matched specification pattern. This deficit is fulfilledusing QMine and MMTQ. We were able to validate our findings with that ofStreamQRE in the absence of time bounds using only event and thread prior-ity if present. In Table 5.7, the cell marked − denote the absence of the result.For example, since QMine does not consider the time of occurrence of eventsthus it cannot be used to mine for system specifications using time-boundconstraints.Comparison of pattern monitoringQMine and MMTQ are capable of pattern monitoring. Therefore, we usedStreamQRE to validate the completeness of both our frameworks. In thisexercise, we demonstrate the results achieved from StreamQRE, QMine andMMTQ over 1 defined mining template. As an operator, we used µ as ouroperator for providing a summary of the quantitative measurement values.Table 5.8 provides a brief comparison for our framework. A static templateof THRUNNING - THRECEIVE was used to perform monitoring. We have onlyshown a brief snapshot of the entire 22662 pattern instances. As evidentboth our frameworks, that is QMine and MMTQ, were capable of trackingevery pattern instance similar to StreamQRE. Hence we claim, both QMineand MMTQ are complete in monitoring all the matching pattern instances.675.1. Experimental AnalysisTable 5.8: Comparison of monitoring capability for QMine, MMTQ w.r.tStreamQREPattern Index QMine MMTQ StreamQREStatistical OperatorMeanTHRUNNING - THRECEIVE1 10 10 10 10.002 17 17 17 13.503 17 17 17 14.674 17 17 17 15.255 10 10 10 14.206 10 10 10 13.507 10 10 10 13.00. . .7456 17 17 17 15.267457 24 24 24 15.267458 17 17 17 15.267459 24 24 24 15.267460 24 24 24 15.267461 21 21 21 15.267462 17 17 17 15.267463 24 24 24 15.267464 17 17 17 15.26. . .8419 0 0 0 15.928420 0 0 0 15.928421 0 0 0 15.928422 0 0 0 15.928423 0 0 0 15.928424 0 0 0 15.928425 0 0 0 15.918426 0 0 0 15.918427 0 0 0 15.91. . .685.2. ConclusionWe did not use TRE and MINTS for comparison since they are not targetedtowards the monitoring of the quantitative property.Consequently, we claim our frameworks are capable of mining and moni-toring all valid temporal specifications. Moreover, our framework provides aquantitative summary along with the capability to induce a time-bound re-striction within the pattern of interest. The formation of the mining templatecan be performed using MINTS that successfully extracts all the dominanttemporal patterns. Since MINTS forms a timed automaton consisting of dom-inant temporal properties, it can be used to detect anomalies in the system ifthe system behavior differs from that of the most prominent behavior.5.2 ConclusionIn this thesis, we introduced the current challenges faced whilst performingspecification mining. We then briefly overviewed a few of these approaches.This leads us to understand the difficulty in forming the specification templateas required by any pattern-based mining framework. Therefore, we presentedour unsupervised temporal specification miner called MINTS to extract timedautomaton (TA) just by using system traces. This enabled us to extract the la-tent temporal and dominant specifications from the system traces. We also usesupport and confidence to understand the coverage of our extracted patterns.Using the extracted specification patterns, a QRE template was formed formining quantitative specification properties using QMine. We used priorityassociated with every thread event. This enabled us to identify the varia-tions among the thread event. We then proceeded with including all systemevents and added time constraints to our QRE template. Using MMTQ, weextracted temporal quantitative properties from the system traces. Therebydemonstrating the applicability of our framework.As stated in Section 4.4, the main contribution of our framework can behighlighted as follow:− QMine provides the capability to mine for all QRE templates along withindividual monitoring− MMTQ extends QMine and provides the capability to mine for all timed-QRE templates along with individual monitoring− MINTS extracts a TA in a semi-supervised fashion, enables mining oftimed temporal patterns, and also provides event prediction capabilityAlthough real-world traces help understand the applicability and useful-ness of a framework, it does not convey any information related to the scala-bility of the framework. Therefore, we created synthetic traces to measure the695.3. Future Workperformance and scalability of all our frameworks and subsequently verifiedtheir theoretical complexity.5.3 Future WorkAs an immediate future work, we aim to build an online monitoring toolfor all our frameworks. This would increase the usability and adoption ofour framework by other researchers. Since we aim to improve our framework,feedback from various researchers is helpful. The second optimization is for theQTrace and QTracetimed used by QMine and MMTQ respectively. Presently,the normalized traces are tightly coupled with the input QRE and QREtimed,thus adding flexibility to the normalization approach would improve the overallexecution time for our frameworks.Moving forward, we aim to provide a simplified representation of theTrietimed. To the best of our knowledge, the merging of two timed automatais not well studied (although Ullman and Hopcroft studied merging of finite-state machines [HMUb]). At present, our approach suffers from event sparsity(when the time between consecutive events varies greatly). With a small tracesize and large time step between two contiguous events, our approach wouldnot be able to learn significant properties. Nevertheless, we believe MINTScan be used in safety-critical applications and by researchers to learn the tem-poral properties of a system. To our knowledge, this is the first attempt todevelop a completely unsupervised approach.70Bibliography[AAGES] Nesreen K. Ahmed, Amir F. Atiya, Neamat El Gayar, and HishamEl-Shishiny. An empirical comparison of machine learning modelsfor time series forecasting. volume 29, pages 594–621. Taylor Fran-cis. → pages 43[ABC] Ce´sar Astudillo, Matthew Bardeen, and Narciso Cerpa. Editorial:Data mining in electronic commerce - support vs. confidence. vol-ume 9, pages I–VII. Facultad de Ingenierıa, Universidad de Talca.→ pages 37[ABL02] Glenn Ammons, Rastislav Bod´ık, and James R. Larus. Mining speci-fications. volume 37, page 4–16, New York, NY, USA, January 2002.Association for Computing Machinery. → pages 7[ACZ+20] Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miao-miao Zhang. Learning one-clock timed automata. In Armin Biereand David Parker, editors, Tools and Algorithms for the Construc-tion and Analysis of Systems, pages 444–462, Cham, 2020. SpringerInternational Publishing. → pages 2, 33, 34, 35, 36, 47, 48, 65[AFR] Rajeev Alur, Dana Fisman, and Mukund Raghothaman. Regularprogramming for quantitative properties of data streams. In Euro-pean Symposium on Programming, pages 15–40. Springer. → pages7, 8, 9, 11, 17, 18, 65[AJU] Fides Aarts, Bengt Jonsson, and Johan Uijen. Generating models ofinfinite-state communication protocols using regular inference withabstraction. In Alexandre Petrenko, Adenilso Sima˜o, and Jose´ Car-los Maldonado, editors, Testing Software and Systems, pages 188–204. Springer Berlin Heidelberg. → pages 34[Ang87] Dana Angluin. Learning regular sets from queries and counterex-amples. volume 75, page 87–106, USA, November 1987. AcademicPress, Inc. → pages 33, 34[AV] Fides Aarts and Frits Vaandrager. Learning i/o automata. In PaulGastin and Franc¸ois Laroussinie, editors, CONCUR 2010 - Concur-71Bibliographyrency Theory, pages 71–85. Springer Berlin Heidelberg. → pages35[BM] C.L. Blake and C.J. Merz. UCI machine learning repository. http://www.ics.uci.edu/mlearn/MLRepository.html. → pages 79[BWC+] T. J. Bunch, J. P. Weiss, Brian G. Crandall, May, and more. Atrialfibrillation is independently associated with senile, vascular, andalzheimer’s dementia. volume 7, pages 433–437. → pages 79[BY] Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Al-gorithms and Tools, pages 87–124. Springer Berlin Heidelberg. →pages 33[CJK] Mihai Christodorescu, Somesh Jha, and Christopher Kruegel. Min-ing specifications of malicious behavior. In Proceedings of the 1stIndia software engineering conference, pages 5–14. ACM. → pages8[DACa] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett.Patterns in property specifications for finite-state verification. InProceedings of the 21st International Conference on Software Engi-neering, ICSE ’99, pages 411–420. Association for Computing Ma-chinery. → pages 2, 19[DACb] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett.Patterns in property specifications for finite-state verification. InProceedings of the 21st International Conference on Software Engi-neering, ICSE ’99, pages 411–420. Association for Computing Ma-chinery. → pages 2[DAC99] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett.Patterns in property specifications for finite-state verification. InProceedings of the 21st International Conference on Software Engi-neering, ICSE ’99, page 411–420, New York, NY, USA, 1999. Asso-ciation for Computing Machinery. → pages 6, 29, 30[DKEB] Rachida Dssouli, Ahmed Khoumsi, Mounia Elqortobi, and JamalBentahar. Chapter three - testing the control-flow, data-flow, andtime aspects of communication systems: A survey. volume 107 ofAdvances in Computers, pages 95–155. Elsevier. → pages 33[DKM+] Valentin Dallmeier, Nikolai Knopp, Christoph Mallon, SebastianHack, and Andreas Zeller. Generating test cases for specificationmining. In Proceedings of the 19th international symposium on Soft-ware testing and analysis, pages 85–96. ACM. 594101. → pages 872Bibliography[DLL+15] Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucˇionis,and Danny Bøgsted Poulsen. Uppaal smc tutorial. volume 17, pages397–415, Aug 2015. → pages 47, 48[dSAdO] Sergio C. de Souza, Nicolas Anquetil, and Ka´thia de Oliveira. Astudy of the documentation essential to software maintenance. pages68–75. ACM. → pages 1[ECH+] Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, andBenjamin Chelf. Bugs as deviant behavior: A general approach toinferring errors in systems code. volume 35, pages 57–72. ACM. →pages 7[ES] Stefan Edelkamp and Stefan Schro¨dl. Chapter 16 - automated sys-tem verification. In Stefan Edelkamp and Stefan Schro¨dl, editors,Heuristic Search, pages 701–736. Morgan Kaufmann. → pages 2, 33[GS] Mark Gabel and Zhendong Su. Online inference and enforcementof temporal properties. In Proceedings of the 32nd ACM/IEEE In-ternational Conference on Software Engineering-Volume 1, pages15–24. ACM. → pages 8[gsd] The future is now: Science for achieving sustainable develop-ment, global sustainable development report 2019. https://sustainabledevelopment.un.org/gsdr2019. → pages 1[HMUa] John E Hopcroft, Rajeev Motwani, and Jeffrey D Ullman. Introduc-tion to Automata Theory, Languages, and Computation. → pages19[HMUb] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. In-troduction to automata theory, languages, and computation, 2ndedition. volume 32, pages 60–65. Association for Computing Ma-chinery. → pages 70[HU] John E. Hopcroft and Jeffrey D. Ullman. Introduction to automatatheory, languages, and computation. Addison-Wesley. → pages 2[Kao20] Johnson Kao. Phone log. https://www.kaggle.com/johnsonkao/phone-log, 2020. → pages 81[KM] A. S. Khan and M. K. Mattsson. Management of documentationand maintainability in the context of software handover. volume 1,pages 238–243. IEEE. → pages 173Bibliography[KP] Zachary Kincaid and Andreas Podelski. Automated Program Veri-fication. In Language and Automata Theory and Applications: 9thInternational Conference, LATA 2015, Nice, France, March 2-6,2015, Proceedings, volume 8977, page 25. Springer. → pages 8[Lama] Leslie Lamport. Time, clocks, and the ordering of events in a dis-tributed system. volume 21, pages 558–565. Association for Com-puting Machinery. → pages 2[Lamb] Leslie Lamport. Time, clocks, and the ordering of events in a dis-tributed system. → pages 6[Lee] J. v. Leeuwen. Handbook of theoretical computer science. Elsevier.→ pages 6[LKHL] David Lo, Siau-Cheng Khoo, Jiawei Han, and Chao Liu. Miningsoftware specifications: methodologies and applications. CRC Press.→ pages 8[LLa] Tien-Duy B Le and David Lo. Beyond support and confidence: Ex-ploring interestingness measures for rule-based specification mining.In 2015 IEEE 22nd International Conference on Software Analysis,Evolution, and Reengineering (SANER), pages 331–340. IEEE. →pages 7[LLb] Tien-Duy B. Le and David Lo. Deep specification mining. In Pro-ceedings of the 27th ACM SIGSOFT International Symposium onSoftware Testing and Analysis, ISSTA 2018, pages 106–117. Associ-ation for Computing Machinery. → pages 1, 2, 6, 33, 34, 65[LMP] Davide Lorenzoli, Leonardo Mariani, and Mauro Pezze`. Automaticgeneration of software behavioral models. In Proceedings of the 30thinternational conference on Software engineering, pages 501–510.ACM. 529080. → pages 7[Lo] David Lo. Specification mining: Methodologies, theories and appli-cations. → pages 2, 33[LPBa] Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. General ltlspecification mining. In Proceedings of the 30th IEEE/ACM Inter-national Conference on Automated Software Engineering, ASE ’15,pages 81–92. IEEE Press. → pages 2, 33, 34, 47, 48, 65[LPBb] Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. GeneralLTL Specification Mining. In Automated Software Engineering74Bibliography(ASE), 2015 30th IEEE/ACM International Conference on, pages81–92. ACM. → pages 8[LSF] T. C. Lethbridge, J. Singer, and A. Forward. How software engineersuse documentation: the state of the practice. volume 20, pages 35–39. → pages 1, 3[Mac] Steve Mackay. Can we get 90% of the globe connected to the internetby 2050? Accessed: 2021-06-01. → pages 1[Mar] Bernard Marr. How much data do we create every day? the mind-blowing stats everyone should read. → pages 6[MN] P. K. Mahato and A. Narayan. Qmine: A framework for miningquantitative regular expressions from system traces. In 2020 IEEE20th International Conference on Software Quality, Reliability andSecurity Companion (QRS-C), pages 370–377. → pages v, 2, 3, 4,25, 33, 35, 47, 48[MN20] Pradeep K. Mahato and Apurva Narayan. Robust supply chainswith gradient boosted trees. In 2020 IEEE Symposium Series onComputational Intelligence (SSCI), pages 2633–2639, 2020.→ pagesv[Mor] Laura Moreno. Summarization of complex software artifacts. pages654–657. ACM. → pages 1[MRA+a] Konstantinos Mamouras, Mukund Raghothaman, Rajeev Alur,Zachary G. Ives, and Sanjeev Khanna. Streamqre: Modular specifi-cation and efficient evaluation of quantitative queries over streamingdata. In Proceedings of the 38th ACM SIGPLAN Conference on Pro-gramming Language Design and Implementation, PLDI 2017, pages693–708. Association for Computing Machinery. → pages 4, 7, 8, 9,10, 11, 17, 18, 25, 33, 65, 89[MRA+b] Konstantinos Mamouras, Mukund Raghothaman, Rajeev Alur,Zachary G. Ives, and Sanjeev Khanna. Streamqre: modular specifi-cation and efficient evaluation of quantitative queries over streamingdata. pages 693–708. ACM. → pages 7, 8, 17, 89[NBF] A. Narayan, N. Benann, and S. Fischmeister. Mining specificationsusing nested words. In 2017 6th International Workshop on SoftwareMining (SoftwareMining), pages 9–16. → pages 875Bibliography[NCJF] Apurva Narayan, Greta Cutulenco, Yogi Joshi, and Sebastian Fis-chmeister. Mining timed regular specifications from system traces.volume 17. Association for Computing Machinery. → pages 2, 8, 25,33, 35, 47, 48, 65, 89[Nor] Christian Nordqvist. What to know about arrhythmia. https://www.medicalnewstoday.com/articles/8887. → pages 79[Pie17] Ann Pietrangelo. The effects of diabetes on your body.https://www.healthline.com/health/diabetes/effects-on-body,2017. [Accessed: 2021-08-18]. → pages 90[PMM17] Fabrizio Pastore, Daniela Micucci, and Leonardo Mariani. Timedk-tail: Automatic inference of timed automata. In 2017 IEEE In-ternational Conference on Software Testing, Verification and Vali-dation (ICST), pages 401–411, 2017. → pages 35[SG] Muzammil Shahbaz and Roland Groz. Inferring mealy machines.In Ana Cavalcanti and Dennis R. Dams, editors, FM 2009: FormalMethods, pages 207–222. Springer Berlin Heidelberg. → pages 34[Sha] Sitaram Sharma. Top google play store statistics 2021. https://www.appventurez.com/blog/google-play-store-statistics/.→ pages 1[Sha19] Ashadullah Shawon. Web log dataset. https://www.kaggle.com/shawon10/web-log-dataset, 2019. → pages 86[SSE] Subanatarajan Subbiah, Christian Schoppmeyer, and Sebastian En-gell. Efficient scheduling of batch plants using reachability treesearch for timed automata with lower bound computations. In E.N.Pistikopoulos, M.C. Georgiadis, and A.C. Kokossis, editors, 21stEuropean Symposium on Computer Aided Process Engineering, vol-ume 29 of Computer Aided Chemical Engineering, pages 930–934.Elsevier. → pages 33[Sta18] By Mayo Clinic Staff. Diabetes - Symptoms and causes- Mayo Clinic. https://www.mayoclinic.org/diseases-conditions/diabetes/symptoms-causes/syc-20371444, 2018. →pages 90[Sur20] U.S. Geological Survey. Earthquake hazard program. https://earthquake.usgs.gov/earthquakes/feed/v1.0/csv.php, 2020.→ pages 8976Bibliography[Thu] A Thurston. Ragel state machine compiler. http://www.colm.net/open-source/ragel/. → pages 11, 13[tre] Timed regular expressions. volume 49, pages 172–206. Associationfor Computing Machinery. → pages 3, 25, 34, 35[UFAMa] Dogan Ulus, Thomas Ferre`re, Eugene Asarin, and Oded Maler. On-line timed pattern matching using derivatives. In Marsha Chechikand Jean-Franc¸ois Raskin, editors, Tools and Algorithms for theConstruction and Analysis of Systems, pages 736–751. SpringerBerlin Heidelberg. → pages 3, 33, 35[UFAMb] Dogan Ulus, Thomas Ferre`re, Eugene Asarin, and Oded Maler.Timed pattern matching. In Axel Legay and Marius Bozga, editors,Formal Modeling and Analysis of Timed Systems, pages 222–236.Springer International Publishing. → pages 33, 34, 35[Ulu] Dogan Ulus. Montre: A tool for monitoring timed regular expres-sions. In Rupak Majumdar and Viktor Kuncˇak, editors, ComputerAided Verification, pages 329–335. Springer International Publish-ing. → pages 3, 33, 35, 47, 48, 65[USG16] USGS. Significant earthquakes. https://www.kaggle.com/usgs/earthquake-database, 1965-2016. → pages 89[Vaa] Frits Vaandrager. Model learning. volume 60, pages 86–95. Associ-ation for Computing Machinery. → pages 34[WGY] Gail Weiss, Yoav Goldberg, and Eran Yahav. Extracting automatafrom recurrent neural networks using queries and counterexamples.In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35thInternational Conference on Machine Learning, volume 80 of Pro-ceedings of Machine Learning Research, pages 5247–5256. PMLR.→ pages 2, 33, 34, 47, 48, 65[WHO20] WHO. Diabetes. https://www.who.int/en/news-room/fact-sheets/detail/diabetes, 2020. → pages 90[Wik] Wikipedia. Temporal logic. https://en.wikipedia.org/wiki/Temporal_logic. → pages 6[Wik20a] Wikipedia. Moment magnitude scale. https://en.wikipedia.org/wiki/Moment_magnitude_scale, 2020. → pages 89[Wik20b] Wikipedia contributors. Lamp (software bundle) — Wikipedia,the free encyclopedia. https://en.wikipedia.org/w/index.php?title=LAMP_(software_bundle), 2020. → pages 8677Bibliography[WN] Westley Weimer and George C. Necula. Mining temporal specifica-tions for error detection. In Nicolas Halbwachs and Lenore D. Zuck,editors, Tools and Algorithms for the Construction and Analysis ofSystems, pages 461–476. Springer Berlin Heidelberg. → pages 33[YEa] Jinlin Yang and David Evans. Automatically inferring temporalproperties for program evolution. In Software Reliability Engineer-ing, 2004. ISSRE 2004. 15th International Symposium on, pages340–351. IEEE. → pages 7[YEb] Jinlin Yang and David Evans. Dynamically Inferring TemporalProperties. In Proceedings of the 5th ACM SIGPLAN-SIGSOFTWorkshop on Program Analysis for Software Tools and Engineer-ing, PASTE ’04, pages 23–28. ACM. → pages 19, 29[YEc] Jinlin Yang and David Evans. Dynamically inferring temporalproperties. In Proceedings of the 5th ACM SIGPLAN-SIGSOFTWorkshop on Program Analysis for Software Tools and Engineering,PASTE ’04, pages 23–28. Association for Computing Machinery. →pages 45, 65[YEB+] Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat,and Manuvir Das. Perracotta: mining temporal API rules fromimperfect traces. In Proceedings of the 28th international conferenceon Software engineering, pages 282–291. ACM. 592060. → pages 778AppendicesAppendix A: Additional Experimental ResultsIn this section, we provide additional experimental analysis performed us-ing real world traces with some of our frameworks.QMineArrhythmia Data setArrhythmia generally occurs with an irregular heartbeat pattern [Nor,BWC+]. This can be due to improper flow of electrical signals by nervesto the heart. Although the majority of arrhythmia cases are harmless, theoccurrence of the same may be a precursor to a major health problem. Theexistence of arrhythmia leads to higher health risks. Therefore it is importantto identify such irregularities before time.For our analysis, we used health records from the UCI Machine LearningRepository [BM]. These are 452 patient records each having 279 attributes.Artery disease is divided into 15 classes with normal class denoted by 1 whileclass 2 refers to coronary artery diseases and class 3-15 exhibits different groupsof arrhythmia. For demonstration purposes, we have only taken 7 attributesnamely Age, Sex, Height, Weight, Heart Rate, and Class. For much detailedanalysis, one could perform the same procedures on a larger data set. Thepoint of interest is the distribution of height, weight, heart rate, and agefor different classes of patients. While such analysis does give insight intothe general trend, it also provides a quick high-level understanding of thedistribution of readings across the data set for rapid medical identification inthe future. We provide our results by finding the mean and variance.Table A.1, we can see detailed breakdown for each age-group and at-tributes. The above analysis was done with QRET = 0M1M2M3M4M5M6,i.e with τ = 7 and Σ = 7 due to only 7 possible events. After our mine map,ξ was created, we were interested in various combinations of the pattern. Forexample, a query of a[4− 9][0− 9]b1c[0− 9] + d[0− 9] + e[0− 9] + f2g woulddenote female patients of Coronary Artery for all age group of range 40− 99and females79Table A.1: Summary of quantitative values on the Arrhythmia Data setAge Sex Count Height (cm) Weight (kg) Heart Rate (bpm) Class0 -Male1-FemaleMean Variance Mean Variance Mean Variance Class0 36 174.194 24.8789 77.8333 124.806 92.0833 69.63191 118 159.356 14.3987 60.8305 131.175 81.4661 52.503110 5 167.2 5.36 58 49.2 98.8 21.361 12 161.333 65.2222 62.1667 270.472 90.5 63.583320 13 168.154 6.74556 69.3846 282.544 95.8462 19.20710-391 28 162.5 42.25 61.6429 244.944 83.2857 108.3473-150 123 171.407 42.5665 76.0569 187.289 89.9024 60.7711 183 160.541 25.9532 68.0383 188.933 80.9071 55.625310 29 169.103 40.9893 80.8276 746.212 94.8621 96.39481 40 158.7 20.61 73.7 172.81 84.45 66.447520 115 170.13 43.7656 76.1043 249.641 96.8174 374.8140-991 77 157.987 21.2596 71.2208 144.432 90.6883 573.9553-15For females of age group 0 − 39, we see that there is variability in heartrate. More specifically usual heart rate is quite low in the normal case whilethose with coronary artery diseases exhibit a bit higher heart rate. Whileour variance is not so significant but the insufficient sample size for femalesin such division could be improved with a larger data set. It must be notedthat our model, as a prerequisite, requires a complete set of traces to mine forinteresting patterns. Although, while data is in itself endless, the frameworkexpects a set of traces that is well balanced and is recorded over a longerduration. Nevertheless, the above quick insight does display a deviation inthe mean heart rate for such patients. Moreover, for males of the age group40− 99, we see a clear distinction in heart rate between a normal person andarrhythmia patients. A normal person would have a heart rate of 89.9 bpmwhile that of a patient would be somewhere around 96.8 bpm. Our resultscorroborate with the details outlined in the data set description.MMTQAndroid application usageAndroid is one of the most popular mobile operating system worldwide. Incontext of smartphones, they use internal batteries to power their operatingsystems, and these batteries have limited capacity. Modern-day apps provideall the visual beauties and capabilities at the expense of high battery usage.Thus the essence of battery management becomes extremely crucial for every80smartphone user. We perform mining, with MMTQ, to understand the effectof application usage on its battery level.For our analysis, we used a real-world android application log [Kao20] thattracks usage by a single user for over 30 applications spanning for a month.The data set is minimal however it includes metrics on various aspects suchas battery level, foreground application, ringer volume, suspend state, signalstrength, wifi connectivity, and more. For demonstration purposes, we usefew features such as foreground applications and battery level, however, itmust be noted that MMTQ is scalable to higher number of features. We alsoselected the top 20 most used foreground applications while grouping the restinto “others”.81Table A.2: Android application usage with transition over 2 applicationBatteryApplication Transition Mean Variance CountWindow Size Interval Time (in sec)From Tojp.naver.line.android com.facebook.katana 82.31 15 72com.frozax.tentsandtrees com.facebook.orca 88.2 14.84 100 – 10com.android.chrome com.netmarbleasia.nikkitw 82.77 10.54 9com.frozax.tentsandtrees com.SuperAwesome.MergeSafari 93 3 2com.frozax.tentsandtrees com.netmarbleasia.nikkitw 77.5 15.5 2App UsageBasedmore than 10com.facebook.orca com.android.chrome 100 0 2jp.naver.line.android com.facebook.katana 82.31 15 72com.sonymobile.home com.facebook.katana 74.88 17.72 560 – 10com.frozax.tentsandtrees jp.naver.line.android 84.88 12.27 26com.google.android.apps.nexuslauncher com.google.android.apps.nexuslauncher 60.73 34.64 11com.google.android.apps.nexuslauncher com.android.chrome 62.5 27.5 2FixedWindow (1 min)more than 10com.android.chrome com.percent.royaldice 24 0 182Table A.2 and A.3 provides our findings for 2 scenarios, one with transitionsbetween 2 applications while the other includes transitions over 3 applications.We used the time to transition from one application to another as our timewindow. The data set was preprocessed and grouped into 2 categories, onewith a fixed window of 1 minute while the other using individual applica-tions as the window size. Samples within each window were averaged amongthemselves. A sample QREtimed is given as 〈0〉[0, 0]M [0, 10000]〈1〉[0, 0] with2 placeholders of the events in the alphabet (the alphabet size is 23, denotingthe presence of 23 distinct foreground labels). The quantitative interval value[0,10000] constraints the miner to accept only those patterns which have appli-cation transition time within 0 to 10 seconds. Similarly, a sample QREtimed as〈0〉[0, 0]M [0, 10000]〈1〉[0, 0] M [0, 10000]〈2〉[0, 0] is expanded to mine for tran-sition over 3 application within the given time frame.83Table A.3: Android application usage with transition over 3 applicationBatteryApplication Transition Mean Variance CountWindow SizeIntervalTime (in sec)Start Intermediate Endcom.facebook.katana jp.naver.line.android com.facebook.katana 79.88 12.20 17less than1 sec com.instagram.android com.facebook.katana com.sonymobile.home 49.50 14.60 4com.facebook.orca jp.naver.line.android com.android.chrome 69.50 15.50 21 - 5 seccom.netmarbleasia.nikkitw com.frozax.tentsandtrees com.sonymobile.home 97.50 1.50 2jp.naver.line.android com.sonymobile.home com.joshua.jptt 28.00 0.00 1App UsageBasedmore than5 sec jp.naver.line.android Others jp.naver.line.android 99.00 0.00 1com.android.chrome com.google.android.apps.nexuslauncher com.netmarbleasia.nikkitw 69.07 19.44 7less than1 sec com.facebook.katana jp.naver.line.android com.facebook.katana 78.56 17.93 17com.facebook.orca jp.naver.line.android com.android.chrome 73.00 12.66 21 - 5 seccom.joshua.jptt com.sonymobile.home com.joshua.jptt 93.50 0.50 2com.frozax.tentsandtrees com.google.android.gm jp.naver.line.android 77.50 5.00 2FixedWindow (1 min)more than5 sec com.google.android.apps.nexuslauncher com.google.android.apps.nexuslauncher com.google.android.apps.nexuslauncher 62.83 28.29 2484A quick analysis of the Table A.2 reveals that the mean battery level ofthe user’s smartphone remained at around 82.31% during transitioning fromLine android application to Facebook under 10 seconds. Although the de-vice maintained a good battery level however with a high variance of 15, itcould suggest that the device could have been recharged during the timeframein few instances. Similarly, when the user switched from TrentsAndTrees(com.frozax.tentsandtrees) to a Role Playing Game (com.netmarbleasia.nikkitw), the battery level stayed at 77.5%. With closer inspection, we foundthat there was an instant when such transition had a battery level of 62%which could indicate an excessive power usage by the Role Playing Game(com.netmarbleasia.nikkitw) possibly due to background activity. Similarly,there was 1 abnormal usage of switching from Chrome (com.android.chrome)to the game Royal Dice (com.percent.royaldice) with a transition time of morethan 10 seconds and battery level of 24%.There were few instances when com.google.android.apps.nexuslauncher(Nexus Launcher), was seen having high usage resulting in a lower batterylevel. A transition from Nexus Launcher to Nexus Launcher with a time in-terval of more than 10 seconds suggests that the device went to sleep duringthe interim. The application came to a resume state from a suspended stateduring device wake-up. In such scenarios as well, Nexus Launcher becamequite resource-intensive thereby suggesting some application issues leading itto behave so erratically. Such insights could be helpful to assist battery man-agement applications to alert the user of such applications.Figure A.1: Battery usage for transition over 2 applications85Table A.3 provides results between transitions of 3 applications. Similarto the findings of battery behavior with the transition between 2 applications,Nexus Launcher exhibits identical battery drain in our 3 application transi-tions test with fewer instances reporting battery level below 40% which couldsuggest a serious issue with the application. Similarly, there was 1 instancewhen the Line (jp.naver.line.android) application was reported to have a lowbattery level of 28%. Meanwhile, a heavy application interaction betweenthe Role-Playing Game (com.netmarbleasia.nikkitw) and TrentsAndTrees re-ported a decent battery level of 97.5% indicating a possibility of continuousdevice charging while playing the games.Likewise, there were 24 instances when the user stayed on the home screen(com.google.android.apps.nexuslauncher) while their battery was at 62%. Fig-ure A.1 displays the monitoring capability of MMTQ for these 24 instances.The possible causes for a dip in battery level could be due to heavy applicationusage. Such insights help understand application behavior and could be usefulfor proper troubleshooting.Although, the data set does not contain many abnormalities however itcould be interesting to find some if it so happens. Following the mining ofinteresting templates, one can perform monitoring for specific template forricher insights. Fig A.1 demonstrates a basic monitoring result for a templates.Webserver Server logWebservers are a vital component for the entire internet community. Theinformation system over the internet is served by web servers across the globe.For every request made by a user, a specific web server would provide a re-sponse to user’s query. More formally, for every request, the quality of responsealong with the swiftness of the information plays a major role in server’s re-sponse. A slow responding server is often frowned upon and criticized forconsuming vital user time. In present times, the responsiveness of a serverplays an important role in the growth of an industry. Moreover, the securityof such servers and databases is of prime importance. A user might be willingto accept a slow response provided their data are not breached and affected.We attempt to understand server behavior using its system traces.For our analysis, we used a real-world server log [Sha19] from a LAMPserver [Wik20b]. The data set is small however it can be used as a reference tobuild an understanding of the usage of MMTQ. The server logged the requestsand responses for a span of about 6 hours. Initially, we categorized this timeseries data set into intervals of HTTP methods, i.e GET and POST, requests.We used the variable interval size to find suitable patterns for deeper min-ing. Table A.4 shows the transition counts in the HTTP methods with variablewindow, α, and δ. The average response time between GET to POST HTTP86Table A.4: Server Call analysis with varying window intervalTemplate <0>[0,0] M[0,alpha] <1>[0,0] M[0,delta] <2>[0,0]Transitionalpha(in ms)delta(in ms)Count Min MaxAverageResponseTime (in ms)GET to POST 100 100 307 1 179 753.99500 500 411 1 8871000 1000 437 1 8875000 5000 489 1 221910000 10000 489 1 2219POST to GET 100 100 316 1 3 671.28500 500 422 1 31000 1000 447 1 35000 5000 491 1 310000 10000 491 1 3calls was around 753.99 milliseconds with a transition time of 500 millisec-onds being the most prominent one while the average response time betweenPOST calls to GET HTTP calls were around 671.28 milliseconds. Althoughthe number of GET HTTP calls were significantly higher than those of POSTHTTP calls. We then used a fixed window to aggregate the number of GETand POST HTTP calls within the window frame followed by varying the in-terval duration among the windows. The intuition behind such activity is tounderstand the relationship of GET and POST HTTP calls for the concernedapp using this webserver and detect anomaly if exists.Table A.5 demonstrates our findings. The ratio of GET to POST callsremained proportional for different window sizes across the server log to about10:1. Fig A.2 represents the monitoring result for theQREtimed = 〈0〉[0, 0]M [0, 15000]〈1〉[0, 0]M [0, 15000]〈2〉[0, 0] (1)where the alphabet size is 2. There was an instant when the GET and POSTcalls to the server peaked however the ratio between the GET and POST callremained with an acceptable limit thereby not suggesting any anomaly at thetime. The data set we used did not contain any anomaly however during asuspicious network breach attempt, the ratio of HTTP method calls changesdrastically. MMTQ provides such capability to mine and monitor for suchsuspiciousWhile our framework MMTQ is successful in detecting the major pat-terns, developers and analysts can always examine using more complex andinteresting patterns. It must be noted that our experiments demonstrate the87Table A.5: Server Call analysis with fixed window frame and varying windowtransitionsFixedWindowInterval Time(in sec)Get PostMean Variance Count Mean Variance Count50 sec0 – 30 31.31 93.62 180 2.18 8.12 180more than 30 10 0 1 0 0 0100 sec0 – 30 49.26 152.77 111 3.42 13.99 111more than 30 51 43 2 4.5 4.5 2Figure A.2: Server usage analysis88Table A.6: Richter magnitude of simultaneous earthquakesIntervalWindow( sec )ProminentSequences( Richter Unit )CountMagnitudeSeverityMean Variance0 - 600Mww - ML 70 5.48 0.58 ModerateMb - Mb 43 4.5 0.3 LightMb - ML 425 4.43 0.34 Light601 - 1200Mb - ML 27 4.47 0.31 LightMb - Md 7 4.39 0.54 LightMd - ML 107 1.48 0.82 Minor1201 - 6000Mb - ML 3 4.6 0.3 LightMd - ML 15 1.62 1.06 MinorML - Md 13 1.47 0.45 Minorapplicability of our tool using real data set. Moreover, the data set used byAlur et.al [MRA+a, MRA+b] is more suitable for streaming exercise while theauthor in [NCJF] focuses solely on event patterns and mining such patterns.Comparison with various deep learning models is also not feasible due to theunique nature of our application, for the detection of anomalies and its magni-tude within a given time interval. Such an effort, to the best of our knowledge,has not been attempted prior to our work.Earthquake Data setIt is well-established that Earth’s crust is formed of tectonic plates [Wik20a].These tectonic plates are often under extreme duress that results in continuousshifting and sliding of these slabs among themselves. A minor displacement ofsuch sheets consequences bears significant energy to cause massive destructionover the surface. Such displacement could occur at the bottom of the earthor in the depth of the sea. Richter scale, developed in 1935 by Charles.F.Richter [Wik20a], is a metric used to measure the intensity of such activity. In2005, the International Association of Seismology and Physics of the Earth’sInterior (IASPEI) had standardized a few metrics89 used alongside the tradi-tional Richter scale.For our analysis, we used a data set ( [Sur20, USG16] ) containing earth-quake information since 1995 maintained by the National Earthquake Infor-mation Center (NEIC). This time-series data set contains several important8https://en.wikipedia.org/wiki/Seismic_magnitude_scales9https://www.usgs.gov/natural-hazards/earthquake-hazards/science/magnitude-types89features such as location and depth of seismic origin, type, and magnitude ofthe earthquake, and more of approximately 12000 such activities. However,for demonstration, we selected the time-series subset comprising of type ofquake along with its magnitude. Table A.6 shows the most prominent patternfor 2 simultaneous earthquakes occurring at different intervals.Diabetes Data setInsulin, a hormone present in the body, helps in controlling the amountof glucose in our blood system [Sta18, Pie17, WHO20]. Glucose is generatedfrom food and is the prime source of energy packets for our bodies. But anexcessive amount of glucose is harmful and could lead to a stroke and numeroushealth complications. When the body fails to effectively break down glucose,it leads to diabetes, a disease that has plagued humans for many centuries.While various studies are in place around the world to overcome such disease,it is important to extract vital information during its treatment. We performa very basic and quick analysis of glucose levels in multiple diabetes patientsusing our QRETtimed.For our analysis, we used records of 70 Diabetes patients from UCI Ma-chine Learning Repository [? ]. The readings were taken for 70 patients witheach record spanning approximately around a month. After an administrationof insulin to a patient, the patient’s body becomes more reliant on externalfactors in order to maintain a reasonable glucose level. In general, a pre-mealglucose reading should be around 80 − 120mg/dl while a post-meal shouldhover around 80 − 140mg/dl. The data set contains glucose reading for 20events ranging from regular insulin dose and NPH insulin dose to glucosereading for Hypoglycemic symptoms. For demonstration purposes, we haverecorded readings for a single patient along with that of all patients. Sincethere would be no control group for our experiment thus we rely on the recom-mended glucose level. We measured reading with a time-bound of fewer than6 hours and that of within 6−8 hours. While such an experiment does providepreliminary quick analysis, we can for certain modify the mining pattern toaccomplish more complex tasks. These mined properties and procedures, oncefinalized, can be used in real-time operations such as that of monitoring ortaking actions based on results.Table A.7 shows a detailed breakdown of glucose reading taken for dif-ferent events with varying time-frames. The above analysis with done withQTracetimed as < 0 > [0, 0]M [0, 0] < 1 > [0, 0]M [0, 0] < 2 > [0, 0]M [22000,32000] < 3 > [0, 0]M [0, 0] < 4 > [0, 0]M [0, 0] < 5 > [0, 0] which has 6 TREand with a time-bound of 6− 8 hours. Since a single event was used for eachinstance, thus there was no necessity of time-bound within the event-space.Since we had 20 classes thus our alphabet size was 20. We recorded the mean90Table A.7: Summary of quantitative values mined on the Diabetes Data setMean Variance Count Mean Variance CountPatient 1 All Patients (70)Less than 6 hoursPre-Breakfast 150.125 61.848148.667 58.44479Regular Insulin 8.375 0.7 8.11111 0.993808NPH Insulin 15 0.71 15.1111 0.737028Pre-Breakfast 213.375 80.61 206 78.8134Pre-Breakfast 170.333 75.1524174.398 66.0269904Regular Insulin 9 1.29 6.80973 3.58236NPH Insulin 15.6667 0.62 21.9513 7.45606Post-Lunch 143.208 73.75 142.007 61.5554NPH Insulin 14.85 1.0142015.4091 2.2086422Regular Insulin 3.95 1.024 3.90909 1.08331Pre-Supper 166.35 57.2125 166.045 56.0774Pre-Breakfast 174.1 73.9 179.455 74.6207Within 6-8hrsRegular Insulin 3.25 0.82915645.33333 4.384326Regular Insulin 6.5 0.5 8 3.60555Unspecified 151.25 73.0458 196 112.091Pre-Breakfast 136.75 51.0802 167.167 61.9097Pre-Breakfast 161.8 78.33625161.8 78.33625Regular Insulin 9.4 1.0198 9.4 1.0198NPH Insulin 14.6 1.2 14.6 1.2Pre-Supper 118 16.4924 118 16.4924Pre-Breakfast 297 01130.429 78.78527Regular Insulin 10 0 5.28571 3.05728NPH Insulin 14 0 15.5714 9.16292Post-Lunch 148 0 193.143 90.9151and variance along with the total match for such patterns. It must be notedthat while the first 3 events, for example, Pre-Breakfast, Regular Insulin, andNPH Insulin must be administered immediately but the 4th event, for example,Post-Lunch was recorded within the time-bound.With a quick analysis, we find that in general patient’s pre-breakfast glu-cose levels are significantly higher than the recommended level while if lunchis taken within 6 hours after the NPH insulin administration the glucose levelstays within a moderate level of 143.208 mg/dl while if lunch is delayed by2 hours then glucose reading rises to that of 193.143 mg/dl which is quitehigh. Though only 7 such events occurred but nevertheless it does have thepotential of adverse effect. We also notice for patients having breakfast within6 hours after NPH Insulin tends to have a higher reading than normal whilefew instances occurred within there was a relatively lower reading if breakfast91was consumed after 6 hours of performing an unspecified event. This could bean interesting finding in determining that particular unspecified event whichcould help in medical research.Our findings suggest an Mww ( estimated based on radiated energy ) quakeis usually followed by ML ( estimated based on local readings ) in under 10mins. Mww provides a more precise and early estimation of the true magnitudeof an earthquake as compared to that of local reading ( ML). Moreover, Mb (estimated based on reading from first primary wave ) reading is often followedby ML reading. Such findings are aligned with their theoretical applicationthus implying the use of a more traditional approach in comparison to olderread ( ML based ). Furthermore, Mb Richter readings provide an alert almost10 minutes before the actual impact. Although such short notice might notbe significant, however, in terms of relief and disaster management, an earlywarning system always plays a vital role. The above analysis is performedusing QRETtimed as 〈0〉[0, 0]M [0, 600] 〈1〉[0, 0] with alphabet size as 10 andtimeframe of under 10 minutes.92
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NonCommercial-ShareAlike 4.0 International
Graduate
Narayan, Apurva
Specification mining frameworks for complex software systems
Text