Ticketing system is an example of a Service System (SS) which is responsible for handling huge volumes of tickets generated by large enterprise IT (Information Technology) infrastructure components, and ensuring smooth operation. An issue is captured as summary on the ticket and once a ticket is resolved, the solution is also noted down on the ticket as resolution. Further the system maintains the provision of recording the time when a ticket is opened, acknowledged to user, resolved and/or closed, from which different QoS parameters could be obtained. For example, Resolution Time can be computed as the difference of resolution date and opening date of the ticket. QoS parameters are used to measure the performance of different aspects of a service. In case of impreciseness of observations of these parameters fuzzy sets seems to be an optimal tool to model them. To ensure better operation for services based on these QoS values we propose a two-stage analysis framework for QoS prediction of incoming tickets which includes fuzzy clustering of incident tickets based on QoS values and building a fuzzy regression model using this categorization and the textual contents of tickets. Further we carry out a fuzzy correlation analysis of different categories (clusters) of QoS parameters. Lastly we report on our experimental results.

Time-triggered architectures form an important component of many distributed computing platforms for safety-critical real-time applications such as avionics and automotive control systems. TTA, FlexRay, and TTCAN are examples of such time-triggered architectures that have been popular in recent times. These architectures involve a number of algorithms for synchronizing a set of distributed computing nodes for meaningful exchange of data among them. The algorithms include a startup algorithm whose job is to integrate one or more nodes into the group of communicating nodes. The startup algorithm runs on every node when the system is powered up, and again after a failure occurs. Some critical issues need to be considered in the design of the startup algorithms, for example, the algorithms should be robust under reasonable assumptions of failures of nodes and channels. The safety-critical nature of the applications where these algorithms are used demands rigorous verification of these algorithms, and there have been numerous attempts to use formal verification techniques for this purpose. This paper focuses on various formal verification efforts carried out for ensuring the correctness of the startup algorithms. In particular, the verification of different startup algorithms used in three time-triggered architectures, TTA, FlexRay, and TTCAN, is studied, compared, and contrasted. Besides presenting the various verification approaches for these algorithms, the gaps and possible improvements on the verification efforts are also indicated.

Summary We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verifysafetyinvariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verifylivenessfor real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd.

Business processes play an important role in organizations; however, not enough attention is given to analyzing and modeling errors in them. In this paper, we study syntactic and control flow error frequencies in business processes from real industry projects. Our samples come from a number of application domains such as Banking and Capital Markets, Insurance and Healthcare, and Retail. We consider industrial business processes modeled in Business Process Modeling Notation (BPMN) and use graph-theoretic techniques and Petri net-based analyses to detect syntactic and control flow-related errors, respectively. We then use a set of metrics that capture different network characteristics of the models and study the empirical relations between the metrics and process errors. The major results of the empirical investigation are: 1) multiple edges to or from tasks as well as hanging nodes are the predominant forms of syntactic errors, 2) syntactic errors occur frequently in Retail & Logistics domain and significantly less in the Insurance and Healthcare domain, and 3) the probability of error occurrence can be modeled as a function of node size and coefficient of connectivity through a logistic regression model which correctly classified 97.6 percent of the cases.

In this paper, we tackle the problem of conformance checking which verifies if the event logs (observed) match/fit the reference (arbitrary) process. We use concepts from Communicating Sequential Processes (CSP), which facilitates automated analysis using PAT toolkit. By this technique one can identify all the logs which cannot be properly replayed on the process. We illustrate our approach with an example. Finally, we introduce some metrics based on conformance checking. They are related to fitness, closeness, and appropriateness of the event logs vis-a-vis reference process models.

We chalk out a procedure for automatically analyzing BPM processes modeled using an in-house Infosys requirements modeling tool, called InFlux. By this analysis, we are able to check the processes for syntactical errors as well as errors due lack of soundness. In the first step of the analysis these processes are checked for syntactical errors using simple graph-search techniques. If these processes do not contain any such error, they are subjected to soundness analysis ( i.e., checking for absence of deadlock and lack of synchronization) using two different approaches with the business process verification tool Woflan and the Petri net model checker LoLA. Depending on the existence of a cycle the models are either fed into Woflan or LoLA. We report our experience with the occurrence of errors in InFlux processes.

We describe the modeling and verification of TTCAN startup protocol using SAL model checker. For the modeling purposes we propose a new modeling framework called Synchronous Calendar which can be seen as an adaptation of Calendar based models introduced by Duterte and Sorea. A Synchronous Calendar can express dense time systems without relying on continuously varying clocks and supports synchronous message transmission. We capture both fault-free and fault-tolerant aspects of startup algorithm of TTCAN in two different models and verify the safety and liveness properties for them. Our verification technique relies on induction and abstraction methods which are supported by SAL model checker. To our knowledge this is the first work towards a formal analysis of TTCAN startup protocol.

Interval-based temporal logics are natural frameworks for modeling a number of problems from various areas of computer science such as artificial intelligence, natural language processing, temporal databases and formal specification. Quite a few interval-based temporal logics became popular in recent years, such as Venema's CDT logic, Halpern and Shoham's HS logic, Moszkowski's ITL and its prepositional version, and Goranko, Montanari, and Sciavicco 's PNL. In this work we introduce a new prepositional interval-based temporal logic called CW, which can be considered an extension of the prepositional fragment of Moszkowski's ITL evaluated over different (parallel) lines, and which is particularly adapt for expressing natural language sentences. We study the logic CW and develop a (non-terminating) sound and complete deduction system based on tableaux for it.

This paper presents a completeness result for a first-order interval temporal logic, called Neighbourhood Logic (NL) which has two neighbourhood modalities. NL can support the specification of liveness and fairness properties of computing systems as well as formalisation of many concepts of real analysis. These two modalities are also adequate in the sense that they can derive other important unary and binary modalities of interval temporal logic. We prove the completeness result for NL by giving a Kripke model semantics and then mapping the Kripke models to the interval models for NL.