Logs are vital to understanding a software system’s behavior, often being the only evidence available to investigate failures. Selecting a Log Severity Level (LSL) can be challenging for the following reasons: (i) the absence of knowledge about how logs are used in production, (ii) the lack of understanding of how critical an event is, and (iii) the lack of practical guidelines. This leads to frequent LSL adjustments during software development and evolution. Our goal is to investigate the LSL adjustments between system releases and explore methods to improve LSL classification. We analyzed the log statements from different releases of open-source systems, focusing on their LSL adjustments and examining the commit comments to understand the reasons for the adjustments. Our results show that most adjustments occur at the intersection of development and production environment logs. Furthermore, the main guiding factors for the adjustments are the experience and logging theory. Our contributions are (i) a description of trends and patterns in LSL adjustments and (ii) a set of 24 heuristics to guide the choice, review, and adjustments of LSL. We advise developers to adhere to the LSL purposes, routinely review LSL settings, and remain adaptable to their mutability. • The severity level of log statements can change as the software evolves. • Severity level adjustments occurring between system releases tend to be more experience-oriented rather than based on logging theories. • Avoiding the overproduction of log data is one of the main reasons for adjusting severity levels in the systems investigated. • There is a tendency towards one-degree adjustments with an emphasis on adjustments between the Debug and Info levels. • From our research, we have derived a set of 24 heuristics designed to guide the choice, review, and adjustment of log severity levels.

The integrity of sensor datasets used in smart home applications is crucial for tasks like activity recognition and automation. We identify common validity issues such as event ordering errors, lifecycle inconsistencies, and data corruption, which are often overlooked but can significantly affect the reliability of analyses. We present a toolbox based on the BeepBeep stream processing library that enables efficient verification of 19 sanity checks on data streams. Our analysis of 15 publicly available smart home datasets collected by five different research teams reveals that most of them violate key assumptions about sensor behavior, emphasizing the need for pre-validation.

Lineage is the process of keeping track of the relationship between the inputs of a data processing task and the parts of the output they contribute to produce. Depending on its precise definition, lineage can be seen as a form of database provenance, a means of tracking information flow in computer programs, or be used to express causality and provide counter-examples for the falsity of a logical statement. In this paper, we establish the formal foundations of a notion of lineage for arbitrary abstract functions manipulating objects that are “composite” –that is, can be made of multiple other objects. Three definitions of lineage over functions are formally defined, respectively called explanation, participation and extraction; we then establish explanation relationships for a set of elementary functions , and for compositions thereof. A fully functional implementation of these concepts is finally presented and experimentally evaluated.

This paper presents a flexible and modular approach to dynamic program analysis for JVM-based languages, aiming to address the limitations of existing tools, in particular their limited expressivity and tight coupling between instrumentation and analysis. The proposed solution decouples these two processes using BISM, a lightweight instrumentation language, and BeepBeep, a complex event processing engine. This novel combination enhances expressiveness, promotes reusability, and integrates seamlessly into JVM-based projects. Various analyses such as monitoring, profiling, coverage measurement, and complex event generation are demonstrated, showcasing the approach’s flexibility.

Event stream processing (ESP) is the application of a computation to a set of input sequences of arbitrary data objects, called “events”, in order to produce other sequences of data objects. In recent years, a large number of ESP systems have been developed; however, none of them is easily amenable to a formal verification of properties on their execution. In this paper, we show how stream processing pipelines built with an existing ESP library called BeepBeep 3 can be exported as a Kripke structure for the NuXmv model checker. This makes it possible to formally verify properties on these pipelines, and opens the way to the use of such pipelines directly within a model checker as an extension of its specification language.

Summary Combinatorial test generation, also called ‐way testing, is the process of generating sets of input parameters for a system under test, by considering interactions between values of multiple parameters. In order to decrease total testing time, there is an interest in techniques that generate smaller test suites. In our previous work, we used graph techniques to produce high‐quality test suites. However, these techniques require a lot of computing power and memory, which is why this paper investigates distributed computing for ‐way testing. We first introduce our distributed graph colouring method, with new algorithms for building the graph and for colouring it. Second, we present our distributed hypergraph vertex covering method and a new heuristic. Third, we show how to build a distributed IPOG algorithm by leveraging either graph colouring or hypergraph vertex covering as vertical growth algorithms. Finally, we test these new methods on a computer cluster and compare them to existing ‐way testing tools.

Context: New scientific evidence continuously arises with advances in Software Engineering (SE) research. Conventionally, Systematic Literature Reviews (SLRs) are not updated or updated intermittently, leaving gaps between updates, during which time the SLR may be missing crucial new evidence. Goal: We propose and evaluate a concept and process called Continuous Systematic Literature Review (CSLR) in SE. Method: To elaborate on the CSLR concept and process, we performed a synthesis of evidence by conducting a meta-ethnography, addressing knowledge from varied research areas. Furthermore, we conducted a case study to evaluate the CSLR process. Results: We describe the resulting CSLR process in BPMN format. The case study results provide indications on the importance and preliminary feasibility of applying CSLR in practice to continuously update SLR evidence in SE. Conclusion: The CSLR concept and process provide a feasible and systematic way to continuously incorporate new evidence into SLRs, supporting trustworthy and up-to-date evidence for SLRs in SE.

Context: There are several initiatives to semi-automate the initial selection of studies task for Systematic Literature Reviews (SLR) to reduce effort and potential bias. Objective: We propose a strategy called SCAS-AI to semi-automate the initial selection task. This strategy improves the original SCAS strategy with Artificial Intelligence (AI) resources (fuzzy logic and genetic algorithm) for studies selection. Method: We evaluated the SCAS-AI strategy through a quasi-experiment with SLRs in Software Engineering (SE). Results: In general, the SCAS-AI strategy improved the results achieved using the original SCAS strategy in reducing the effort of the initial selection task. The effort reduction applying SCAS-AI was 39.1%. In addition, the errors percentage was 0.3% for studies automatically excluded (false negative – loss of evidence) and 3.3% for studies automatically included (false positive – evidence later excluded during the full-text reading). Conclusion: The results show the potential of the investigated AI techniques to support the initial selection task for SLRs in SE.

Abstract Explainability is the process of linking part of the inputs given to a calculation to its output, in such a way that the selected inputs somehow “cause” the result. We establish the formal foundations of a notion of explainability for arbitrary abstract functions manipulating nested data structures. We then establish explanation relationships for a set of elementary functions, and for compositions thereof. A fully functional implementation of these concepts is finally presented and experimentally evaluated.

Context: A tertiary study can be performed to identify related reviews on a topic of interest. However, the elaboration of an appropriate and effective search string to detect secondary studies is challenging for Software Engineering (SE) researchers. Objective: The main goal of this study is to propose a suitable search string to detect secondary studies in SE, addressing issues such as the quantity of applied terms, relevance, recall and precision. Method: We analyzed seven tertiary studies under two perspectives: (1) structure – strings’ terms to detect secondary studies; and (2) field: where searching – titles alone or abstracts alone or titles and abstracts together, among others. We validate our string by performing a twostep validation process. Firstly, we evaluated the capability to retrieve secondary studies over a set of 1537 secondary studies included in 24 tertiary studies in SE. Secondly, we evaluated the general capacity of retrieving secondary studies over an automated search using the Scopus digital library. Results: Our string was capable to retrieve an optimum value of over 90% of the included secondary studies (recall) with a high general precision of almost 60%. Conclusion: The suitable search string for finding secondary studies in SE contains the terms “systematic review”, “literature review”, “systematic mapping”, “mapping study” and “systematic map”.

Context: Searching and selecting relevant evidence is crucial to answer research questions from secondary studies in Software Engineering (SE). The activities of search and selection of studies are labour-intensive, time-consuming and demand automation support. Objective: Our goal is to identify and summarize the state-of-the-art on automation support for searching and selecting evidence for secondary studies in SE. Method: We performed a systematic mapping on existing automating support to search and select evidence for secondary studies in SE, expanding our investigation in a cross-domain study addressing advancements from the medical field. Results: Our results show that the SE field has a variety of tools and Text Classification (TC) approaches to automate the search and selection activities. However, medicine has more well-established tools with a larger adoption than SE. Cross-validation and experiment are the most adopted methods to assess TC approaches. Furthermore, recall and precision are the most adopted assessment metrics. Conclusion: Automated approaches for searching and selecting studies in SE have not been applied in practice by SE researchers. Integrated and easy-to-use automated approaches addressing consolidated TC techniques can bring relevant advantages on workload and time saving for SE researchers who conduct secondary studies.

Event stream processing (ESP) is the application of a computation to a set of input sequences of arbitrary data objects, called "events", in order to produce other sequences of data objects. In recent years, a large number of ESP systems have been developed; however, none of them is easily amenable to a formal verification of properties on their execution. In this paper, we show how stream processing pipelines built with an existing ESP library called BeepBeep 3 can be exported as a Kripke structure for the NuXmv model checker. This makes it possible to formally verify properties on these pipelines, and opens the way to the use of such pipelines directly within a model checker as an extension of its specification language.

The paper reports results on an empirical study of the structural properties of HTML markup in websites. A first large-scale survey is made on 708 contemporary (2019–2020) websites, in order to measure various features related to their size and structure: DOM tree size, maximum degree, depth, diversity of element types and CSS classes, among others. The second part of the study leverages archived pages from the Internet Archive, in order to retrace the evolution of these features over a span of 25 years. The goal of this research is to serve as a reference point for studies that include an empirical evaluation on samples of web pages.

Added value can be extracted from event logs generated by business processes in various ways. However, although complex computations can be performed over event logs, the result of such computations is often difficult to explain; in particular, it is hard to determine what parts of an input log actually matters in the production of that result. This paper describes a framework to provide explainable results for queries executed over sequences of events, where individual output values can be precisely traced back to the data elements of the log that contribute to (i.e. "explain") the result. This framework has been implemented into the BeepBeep event processing engine and empirically evaluated on various queries.

Open Source Software (OSS) has been recognized by the software development community as an effective way to deliver software. Unlike traditional software development, OSS development is driven by collaboration among developers spread geographically and motivated by common goals and interests. Besides this fact, it is recognized by the OSS community the need to understand OSS development process and its activities. Our goal is to investigate the state-of-art about OSS process through conducting a systematic literature review providing an overview of how the OSS community has been investigating OSS process over past years. We identified and summarized OSS process activities and their characteristics and translated them into an OSS macro process using BPMN notation. As a result, we systematically analyzed 33 studies presenting an overview of the OSS process research and a generalized OSS development macro process represented by BPMN notation with a detailed description of each OSS process activity and roles in OSS environment. We conclude that OSS process can be in practice further investigated by researchers. In addition, the presented OSS process can be used as a guide for OSS projects and be adapted according to each OSS project reality. It provides insights to managers and developers who want to improve their development process even in OSS and traditional environments. Finally, recommendations for OSS community regarding OSS process activities are provided.

Context: Systematic Literature Reviews (SLRs) are important instruments for both Software Engineering (SE) practitioners and scientific community. Their value directly depends on their quality and up-to-date results. However, most of the SLRs are outdated and the current scenario on how SLRs are documented does not favor their updating process. Goal: In this scenario, the main goal of this paper is to present an experience report on how to transfer the know-how of SLRs to facilitate their updates. Method: To address this issue, we used a Knowledge Management (KM) model, known as Nonaka-Takeuchi model, and described how we instantiated the Model for SLR update. We use two SLRs updates conducted by us to illustrate some of the knowledge sharing issues. Results: Our examples showed that the introduction of the concept of KM in the SLR update is in fact valuable, especially for sharing tacit knowledge (decisions) taken throughout the review process. Conclusions: We conclude that KM principles can be applied to manage the knowledge generated during the update of SLR.

Historical data contained in event logs can reveal important insights about the execution of a business process. In particular, the trends computed by processing and analyzing the sequence of events generated by multiple instances of the same process serve as the basis to produce forecasts about current executions of the process. In this paper, we join the concepts of event stream processing and machine learning to create a framework that allows the computation of various kinds of predictions on event logs. The proposed framework is generic: by providing different definitions to a handful of event functions, multiple different types of predictions can be computed using the same basic workflow. The approach has been implemented and experimentally evaluated by extending an existing event stream processing engine.

We present an extension of first-order logic that includes a counting quantifier, allowing one to express assertions about the number n of elements in a set that satisfy a given property. We show how this logic can be used to express problems such as node degree distribution in computer networks, various graph problems and entity relationships with cardinality constraints found in UML diagrams. We then present a translation of this counting logic back into classical first-order logic; this translation is linear in the number of quantifiers and independent of n. This translation makes it possible to use existing first-order model finders to efficiently generate test data following a specific distribution.

Information systems produce different types of event logs; in many situations, it may be desirable to look for trends inside these logs. We show how trends of various kinds can be computed over such logs in real time, using a generic framework called the trend distance workflow. Many common computations on event streams turn out to be special cases of this workflow, depending on how a handful of workflow parameters are defined. This process has been implemented and tested in a real-world event stream processing tool, called BeepBeep. Experimental results show that deviations from a reference trend can be detected in realtime for streams producing up to thousands of events per second.

LabPal is a Java library designed to easily create and run experiments on a computer. It provides a user-friendly web console, support for automated plotting, a pause-resume facility, a mechanism for handling data traceability and linking, and the possibility of saving all experiment input and output data in an open format. These functionalities greatly reduce the amount of boilerplate scripting needed to run experiments on a computer, and simplify their re-execution by independent parties.

SealTest is a Java library for generating test sequences based on a formal specification. It allows a user to easily define a wide range of coverage metrics using multiple specification languages. Its simple and generic architecture makes it a useful testing tool for dynamic software systems, as well as an appropriate research testbed for implementing and experimentally comparing test sequence generation algorithms.

This paper describes the design and implementation of an SQL-like language for performing complex queries on event streams. The Event Stream Query Language (eSQL) aims at providing a simple, intuitive and fully non-procedural syntax, while still preserving backwards compatibility with traditional SQL. More importantly, eSQL's core syntax is designed to be extended by user-defined grammatical constrcts. These new constructs can form domain-specific sub-languages, with eSQL being used as the “glue” to form very expressive queries. These concepts have been implemented in BeepBeep 3, an open source event stream query engine.

Artifact-centric workflows describe possible executions of a business process through constraints expressed from the point of view of the documents exchanged between principals. A sequence of manipulations is deemed valid as long as every document in the workflow follows its prescribed lifecycle at all steps of the process. So far, establishing that a given workflow complies with artifact lifecycles has mostly been done through static verification, or by assuming a centralized access to all artifacts where these constraints can be monitored and enforced. We present in this paper an alternate method of enforcing document lifecycles that requires neither static verification nor single-point access. Rather, the document itself is designed to carry fragments of its history, protected from tampering using hashing and public-key encryption. Any principal involved in the process can verify at any time that a document's history complies with a given lifecycle. Moreover, the proposed system also enforces access permissions: not all actions are visible to all principals, and one can only modify and verify what one is allowed to observe.

The paper focuses on bugs in web applications that can be detected by analyzing the contents and layout of page elements inside a browser's window. Based on an empirical analysis of 35 real-world web sites and applications (such as Facebook, Dropbox, and Moodle), it provides a survey and classification of more than 90 instances of layout-based bugs. It then introduces Cornipickle, an automated testing tool that provides a declarative language to express desirable properties of a web application as a set of human-readable assertions on the page's HTML and CSS data. Such properties can be verified on-the-fly as a user interacts with an application.

The management of the configuration of network devices is a complex process, due to both the number of devices and parameters to take into consideration, and most importantly to the widely varying ways in which such parameters can be queried and modified on each device. Each equipment vendor provides its own command-line interface or management protocol where parameters are structured in a different way, and even multiple equipments from the same vendor may need to be interacted with differently. In this paper, we present a generic data model for configuration information of network devices that takes into account vendor and version heterogeneity. Ultimately, a configuration query engine will allow a user to pinpoint a specific, abstract configuration parameter, and be given the proper sequence of commands to query that parameter on a device of given vendor and operating system version.

Information systems in general, and business processes in particular, generate a wealth of information in the form of event traces or logs. The analysis of these logs, either offline or in real-time, can be put to numerous uses: computation of various statistics, detection of anomalous patterns or compliance violations of some form of contract. However, current solutions for Complex Event Processing (CEP) generally offer only a restricted set of predefined queries on traces, and otherwise require a user to write procedural code to compute custom queries. In this paper, we present a formal and declarative language for the manipulation of event traces.

Web crawling is the process of exhaustively exploring the contents of a web site or application through automated means. While the results of such a crawling can be put through numerous uses ranging from a simple backup to comprehensive testing and analysis, features of modern-day applications prevent crawlers from properly exploring applications. We provide an in-depth analysis of 15 such features, and report on their presence in a study of 16 real-world web sites. Based on that study, we develop a configurable web application where the presence of each such feature can be turned on or off, aimed as a test bench where existing crawlers can be compared in a uniform way. Our results, which are the first exhaustive comparison of available crawlers, indicates areas where future work should be aimed.

Configuration validation is the process of automatically assessing whether the various configuration parameters of a network's devices are set to appropriate values according to a set of formal constraints given beforehand. Virtually all automated validation solutions presented to date assume a centralized and complete knowledge of the network's configuration to perform their analysis. We present an algorithm that automatically performs this evaluation, while still requiring the need for a centralized point of verification, this algorithm can analyze the constraints to evaluate, and reduce the amount of data that needs to be transferred to that central location, pushing as much of the evaluation of each constraint locally on each device.

Runtime verification is the process of observing a sequence of events generated by a running system and comparing it to some formal specification for potential violations. We show how the use of a runtime monitor can greatly speed up the testing phase of a video game under development, by automating the detection of bugs when the game is being played. We take advantage of the fact that a video game, contrarily to generic software, follows a special structure that contains a "game loop", this game loop can be used to centralize the instrumentation and generate events based on the game's internal state. We report on experiments made on a sample of five real-world video games of various genres and sizes, by successfully incrementing and efficiently monitoring various temporal properties over their execution-including actual bugs reported in the games' bug tracking database in the course of their development.

A runtime monitor is a tool that takes as input a model of some system, and observes in real time that the sequence of events produced by a run of that system follows the specification. While existing monitoring solutions generally use finite-state machines and temporal logic as their model language, the specification is ultimately tangled with hand-written, implementation-specific details which severely limit their range of application. We present a runtime monitoring platform that clearly separates the extraction of events in the running program from the specification and monitoring process. This separation allows one to cleanly monitor first-order properties involving arbitrarily complex native program objects, while still incurring reasonable overhead.

Configuration information in network devices is stored in an internal data structure that can be accessed through various means. However, the exact organization of the parameters, and therefore the actual way of reaching them, does not necessarily reflect a semantically sound view of the configuration operations in all situations. In this paper, we propose the use of configuration dependency rules to provide a semantic virtualization of the parameters. We show how this virtualization can be superimposed with minimal interference over current configuration protocols, taking Netconf as an example.

Configuration Logic (CL) is a formal language that allows a network engineer to express constraints in terms of the actual parameters found in the configuration of network devices. There exists an efficient algorithm that can automatically check a pool of devices for conformance to a set of CL constraints; moreover, this algorithm can point to the part of the configuration responsible for the error when a constraint is violated. A CL validation engine has been integrated into a network management tool called ValidMaker. We show on a simple use case scenario based on Virtual Local Area Networks how representative formal constraints can be expressed with CL and efficiently validated with ValidMaker.

An anomaly in a firewall is a relationship between two of its rules that may hint at a possible misconfiguration of its filter. One notable limitation of existing solutions for firewall analysis is that they provide algorithms tailored for the verification of specific anomalies. We introduce a modal logic, called Visibility Logic (VL), which can be used to express arbitrary patterns between rules inside a firewall. A model checker allows one to verify any formula expressed in visibility logic, of which traditional anomalies are merely particular instances, with running times of under one second for 1,500 rules.

An increasing number of popular SOAP web services exhibit a stateful behavior, where a successful interaction is determined as much by the correct format of messages as by the sequence in which they are exchanged with a client. The set of such constraints forms a "message contract” that needs to be enforced on both sides of the transaction; it often includes constraints referring to actual data elements inside messages. We present an algorithm for the runtime monitoring of such message contracts with data parameterization. Their properties are expressed in {\rm LTL}\hbox{-}{\rm FO}^+, an extension of Linear Temporal Logic that allows first-order quantification over the data inside a trace of XML messages. An implementation of this algorithm can transparently enforce an {\rm LTL}\hbox{-}{\rm FO}^+ specification using a small and invisible Java applet. Violations of the specification are reported on-the-fly and prevent erroneous or out-of-sequence XML messages from being exchanged. Experiments on commercial web services from Amazon.com and Google indicate that {\rm LTL}\hbox{-}{\rm FO}^+ is an appropriate language for expressing their message contracts, and that its processing overhead on sample traces is acceptable both for client-side and server-side enforcement architectures.

Interface contracts are sets of constraints specifying valid exchanges of messages between two or more peers. A contract violation occurs when one of the peers fails to fulfil one of these constraints and emits a message that is not a valid continuation of a message "trace". In some cases, the message that directly exposes the violation turns out to be the last of a succession of forced moves, while the "root cause" of the violation resides earlier in the trace and may emanate from a different peer. We formally define the notion of causality for interface contracts expressed in a first-order extension of Linear Temporal Logic. In particular, we show how the detection of root causes reduces to satisfiability solving of a precise set of formulae. An experimental setup shows how causality can be analyzed automatically on a pre-recorded message trace.

This paper presents a methodology for generating a web service "stub" that simulates the behaviour of a real-world SOAP web service. The simulation is driven by a formal description of the original service's input and output parameters, messages, and ordering constraints between messages, using an extension of Linear Temporal Logic called LTL-FO+. This logic is rich enough to express complex behaviours taken from real-world web services, where the structure of future messages and valid parameter values are interdependent. Given a history of previous interactions, a sound, symbolic algorithm is described that generates on-the-fly a new message that is a valid continuation of that history with respect to the LTLFO + specification. By providing a faithful placeholder for an actual third-party web service, this algorithm can be used as a development and testing tool. Empirical evaluation shows how such an approach outperforms a previous attempt that relied on a model checker to produce each new message.

Requirements on message-based interactions can be formalized as an interface contract that specifies constraints on the sequence of possible messages that can be exchanged by multiple parties. At runtime, each peer can monitor incoming messages and check that the contract is correctly being followed by their respective senders. We introduce cooperative runtime monitoring, where a recipient "delegates" its monitoring task to the sender, which is required to provide evidence that the message it sends complies with the contract. In turn, this evidence can be quickly checked by the recipient, which is then guaranteed of the sender's compliance to the contract without doing the monitoring computation by itself. A particular application of this concept is shown on web services, where service providers can monitor and enforce contract compliance of third-party clients at a small cost on the server side, while avoiding to certify or digitally sign them.

The enforcement of navigation constraints in web applications is challenging and error prone due to the unrestricted use ofnavigation functions inweb browsers. This often leads to navigation errors, producing cryptic messages and exposinginformation thatcanbeexploitedbymalicious users. We propose a runtime enforcement mechanism that restricts the control flow of a web application to a state machine model specified by the developer, and use model checking to verify temporal properties on these state machines. Our experiments, performed on three real-world applications, show that 1) our runtime enforcement mechanism incurs negligible overhead under normal circumstances, and can even reduceserverprocessingtimeinhandlingunexpectedrequests; 2) by combining runtime enforcement with model checking, navigation correctness can be efficiently guaranteed in large web applications.

The global interaction behavior in message-based systems can be specified as a finite-state machine defining acceptable sequences of messages exchanged by a group of peers. Realizability analysis determines if there exist local implementations for each peer, such that their composition produces exactly the intended global behavior. Although there are existing sufficient conditions for realizability, we show that these earlier results all fail for a particular class of specifications called arbitrary-initiator protocols. We present a novel algorithm for deciding realizability by computing a finite-state model that keeps track of the information about the global state of a conversation protocol that each peer can deduce from the messages it sends and receives. By searching for disagreements between each peer’s deduced states, we provide a sound analysis for realizability that correctly classifies realizability of arbitrary-initiator protocols.

Rule-based filters are sequences of rules formed of a condition and a decision. Rules are applied sequentially up to the first fulfilled condition, whose matching decision determines the outcome. Such filters are particularly useful in network management, where they filter packets allowed to flow in or out of an interface. Properties of filters which either reveal or hint to misconfiguration (anomalies) have been largely studied in the network management community. We show that in fact such properties are of a spatial and temporal nature. Accordingly we introduce a spatio-temporal language appropriate for filter properties, use it to describe major filter anomalies and finally prove that verifying a property in this language can be done in time polynomial in the number of filter rules.

Most works that extend workflow validation beyond syntactical checking consider constraints on the sequence of messages exchanged between services. These constraints are expressed only in terms of message names and abstract away their actual data content. We provide examples of real-world “data-aware” Web service constraints where the sequence of messages and their content are interdependent. To this end, we present {\rm CTL}\hbox{-}{\rm FO}^+, an extension over Computation Tree Logic that includes first-order quantification on message content in addition to temporal operators. We show how {\rm CTL}\hbox{-}{\rm FO}^+ is adequate for expressing data-aware constraints, give a sound and complete model checking algorithm for {\rm CTL}\hbox{-}{\rm FO}^+, and establish its complexity to be PSPACE-complete. A “naive” translation of {\rm CTL}\hbox{-}{\rm FO}^+ into CTL leads to a serious exponential blowup of the problem that prevents existing validation tools to be used. We provide an alternate translation of {\rm CTL}\hbox{-}{\rm FO}^+ into CTL, where the construction of the workflow model depends on the property to validate. We show experimentally how this translation is significantly more efficient for complex formulas and makes model checking of data-aware temporal properties on real-world Web service workflows tractable using off-the-shelf tools.

We present an algorithm for the runtime monitoring of business process properties with data parameterization. The properties are expressed in LTL-FO+, an extension to traditional Linear Temporal Logic that includes full first-order quantification over the data inside a trace of XML messages. The algorithm works "on-the-fly": it keeps in memory only the states that are necessary at each step. Initial results indicate that LTL-FO+ is an appropriate language for expressing data dependencies on message traces and that its processing overhead on sample traces is acceptable.

Configuration Logic (CL) is a fragment of XQuery that allows first-order quantification over node labels. In this paper, we study CL satisfiability and seek a deterministic decision procedure to build models of satisfiable CL formulae. To this end, we show how to revert CL satisfiability into an equivalent CTL satisfiability problem in order to leverage existing model construction algorithms for CTL formulae.

Most works that extend workflow validation beyond syntactical checking consider constraints on the sequence of messages exchanged between services. However, these constraints are expressed only in terms of message names and abstract away their actual data content. Using the context of the User-controlled Lightpath initiative (UCLP) hosted by the CANARIE consortium, we provide examples of real- world "data-aware" web service constraints where the sequence of messages and their content are interdependent. We present CTL-FO+, an extension over Computation Tree Logic that includes first-order quantification on state variables in addition to temporal operators. We show how CTL- FO+is adequate for expressing data-aware constraints, give a complete model checking algorithm for CTL-FO+and establish its complexity to be PSPACE-complete. This makes using CTL-FO+for validating workflow properties no harder than using the Linear Temporal Logic (LTL) already used by some web service tools. Finally, we show how the modelling of data-aware properties is an increase in expressiveness that cannot be efficiently simulated by these tools.

The accuracy of the rules produced by a concept learning system can be hindered by the presence of errors in the data, such as "ill-defined" attributes that are too general or too specific for the concept to learn. In this paper, we devise a method that uses the Boolean differences computed by a program called Newton to identify multiple ill-defined attributes in a dataset in a single pass. The method is based on a compound heuristic that assigns a real-valued rank to each possible hypothesis based on its key characteristics. We show by extensive empirical testing on randomly generated classifiers that the hypothesis with the highest rank is the correct one with an observed probability quickly converging to 100%. Moreover, the monotonicity of the function enables us to use it as a rough estimator of its own likelihood

Querying and efficiently validating properties on labelled tree structures has become an important part of research in numerous domains. In this paper, we show how a fragment of XPath called configuration logic (CL) can be embedded into computation tree logic. This framework embeds into CTL a larger subset of XPath than previous work and in particular allows universally and existentially quantified variables in formulas. Finally, we show how the variable binding mechanism of CL can be seen as a branching-time equivalent of the "freeze" quantifier

We introduce a logical formalism for describing properties of configurations of computing systems. This logic of trees allows quantification on node labels, which are modalities containing variables. We explain the motivation behind our formalism and give both a classical semantics and a new equivalent one based on partial functions on variables.