peer reviewed

As modern software systems grow in complexity and operate in dynamic environments, the need for runtime analysis techniques becomes a more critical part of the verification and validation process. Runtime verification monitors the runtime system behaviour by checking whether an execution trace— a sequence of recorded events—satisfies a given specification, yielding a Boolean or quantitative verdict. However, when a specification is violated, such a verdict is often insufficient to understand why the violation happened. To fill this gap,diagnosticsapproaches aim to produce more informative verdicts. In this paper, we address the problem of generating informative verdicts for violated Inter-procedural Control-Flow Temporal Logic (iCFTL) specifications that express constraints over program variable values. We propose a diagnostic approach based on backward data-flow analysis to statically determine the relevant statements contributing to the specification violation. Using this analysis, we instrument the program to produce enriched execution traces. Using the enriched execution traces, we perform the runtime analysis and identify the statements whose execution led to the specification violation. We implemented our approach in a prototype tool,iCFTLdiagnostics, and evaluated it on 112 specifications across 10 software projects. Our tool achieves 90% precision in identifying relevant statements for 100 of the 112 specifications. It reduces the number of lines that have to be inspected for diagnosing a violation by at least 90%. In terms of computational cost, our experiments show thatiCFTLdiagnosticsgenerates a diagnosis within 7 min, and requires no more than 25MB of memory. The instrumentation required to support diagnostics incurs an execution time overhead of less than 30% and a memory overhead below 20%.

Ensuring the safety and reliability of Cyber-Physical Systems (CPS) is critical, particularly in safety-critical domains such as automotive and aerospace. Fault Injection (FI) is a well-established technique for testing system resilience, but current FI tools often face challenges when applied to Simulink-based CPS models. In this paper, we analyze the shortcomings of existing FI methods, and reflect on the key challenges of FI for Simulink-based CPS models. By offering insights into these challenges and proposing research pathways, we aim to inspire further advances in FI methodologies, enabling more robust testing of CPS in real-world applications.

Modern software systems increasingly rely on personal data. Despite the enforcement of the European General Data Protection Regulation (GDPR) and the growing awareness about privacy and data protection, many individuals’ rights remain unsatisfactorily implemented in software systems. This is partially due to the knowledge gap between legal interpretation and software development.In this paper, we address this gap first by extracting, in close collaboration with legal experts, a list of 108 requirements pertinent to the right of access (ACC) and the right to portability (PRT), two fundamental rights under the GDPR. We further propose the XTRAREG approach, which utilizes large language models (LLMs) and retrieval augmented generation (RAG) to provide automated assistance in extracting privacy requirements from predefined legal sources.Compared to the manually extracted requirements, XTRAREG can automatically generate requirements with an accuracy of 81.8% for ACC and 85.7% for PRT. Our empirical evaluation reveals two notable observations: (i) A skewed performance in terms of coverage in the favor of ACC, indicating the significant impact of abundant training data of the LLM, (ii) despite explicit exposure of legal references through RAG, the LLM generates requirements predominantly from the GDPR.

Mobile apps are ubiquitous in our lives as they provide numerous services to support our daily activities. Personalizing such services entail collecting (possibly sensitive) personal information. Mobile apps must therefore comply with privacy regulations like the General Data Protection Regulation (GDPR) enforced in the European Union (EU). To achieve compliance, an app should implement the legal requirements pertinent to data collection and processing according to the GDPR. Privacy policies associated with apps can serve as intermediary instruments connecting between source code and regulations. They explain to app users how activities involving personal data are implemented and provide a detailed view on how legal requirements are operationalized in the app. Incomplete policies can indicate non-compliant apps.This paper sheds light on the state-of-practice of GDPR compliance in two mainstream app markets: the Apple App Store and the Google Play Store. We conducted a study to assess the completeness of 470 apps privacy policies in these stores according to the GDPR. Our analysis shows that, irrespective of the app store, fundamental GDPR requirements (e.g., information pertinent to individuals’ rights and details of data transfer outside EU) are missing in ≈92% of the analyzed policies, revealing potential breaches in the respective apps.

Growth in system complexity increases the need for automated techniques dedicated to different log analysis tasks such as Log-based Anomaly Detection (LAD). The latter has been widely addressed in the literature, mostly by means of a variety of deep learning techniques. However, despite their many advantages, that focus on deep learning techniques is somewhat arbitrary as traditional Machine Learning (ML) techniques may perform well in many cases, depending on the context and datasets. In the same vein, semi-supervised techniques deserve the same attention as supervised techniques since the former have clear practical advantages. Further, current evaluations mostly rely on the assessment of detection accuracy. However, this is not enough to decide whether or not a specific ML technique is suitable to address the LAD problem in a given context. Other aspects to consider include training and prediction times as well as the sensitivity to hyperparameter tuning, which in practice matters to engineers. In this paper, we present a comprehensive empirical study, in which we evaluate a wide array of supervised and semi-supervised, traditional and deep ML techniques w.r.t. four evaluation criteria: detection accuracy, time performance, sensitivity of detection accuracy and time performance to hyperparameter tuning. Our goal is to provide much stronger and comprehensive evidence regarding the relative advantages and drawbacks of alternative techniques for LAD. The experimental results show that supervised traditional and deep ML techniques fare similarly in terms of their detection accuracy and prediction time on most of the benchmark datasets considered in our study. Moreover, overall, sensitivity analysis to hyperparameter tuning with respect to detection accuracy shows that supervised traditional ML techniques are less sensitive than deep learning techniques. Further, semi-supervised techniques yield significantly worse detection accuracy than supervised techniques.

Abstract The completeness (in terms of content) of financial documents is a fundamental requirement for investment funds. To ensure completeness, financial regulators have to spend significant time carefully checking every financial document based on relevant content requirements, which prescribe the information types to be included in financial documents (e.g., the fund name, the description of shares’ issue conditions and procedures). Although several techniques have been proposed to automatically detect certain types of information in documents across application domains, they provide limited support to help regulators automatically identify the text chunks related to financial information types, due to the complexity of financial documents and the diversity of the sentences typically characterizing an information type. In this paper, we propose FITI to trace content requirements in financial documents with multi-granularity text analysis. Given a new financial document, FITI first selects a set of candidate sentences for efficient information type identification. Then, to rank candidate sentences, FITI uses a combination of rule-based and data-centric approaches, by leveraging information retrieval (IR) and machine learning (ML) techniques that analyze the words, sentences, and contexts related to an information type. Finally, using a list of domain-specific indicator phrases related to each information type, a heuristic-based selector, which considers both the sentence ranking and domain-specific phrases, determines a list of sentences corresponding to each information type. We evaluated FITI by assessing its effectiveness in tracing financial content requirements in 100 real-world financial documents. Experimental results show that FITI is able to provide accurate identification with average precision, recall, and $$\hbox {F}_1$$ F 1 -score values of 0.824, 0.646, and 0.716, respectively. The overall accuracy of FITI significantly outperforms the best baseline (based on a transformer language model) by 0.266 in terms of $$\hbox {F}_1$$ F 1 -score. Furthermore, FITI can help regulators detect about 80% of missing information types in financial documents.

This article represents the Replicated Computational Results (RCR) related to our TOSEM paper “A Machine Learning Approach for Automated Filling of Categorical Fields in Data Entry Forms,” where we proposed LAFF, an approach to automatically suggest possible values of categorical fields in data entry forms, which is a common user interface feature in many software systems. In this RCR report, we provide details about our replication package. We make available the different scripts needed to fully replicate the results obtained in our paper.

This is the Replicated Computational Results (RCR) Report for the article ‘ Stress Testing Control Loops in Cyber-Physical Systems ’. The article proposes a novel approach for testing Cyber-Physical Systems (CPS) based on the integration of the guarantees that can be provided with the control theoretical models into the software testing practices. This RCR report describes how to reproduce the empirical results of the article. We make available the different scripts needed to fully replicate the results obtained in our article.

Cyber-Physical Systems (CPSs) software is used to enforce desired behaviours on physical systems. To test the interaction between the CPS software and the system’s physics, engineers provide traces of desired physical states and observe traces of the actual physical states. CPS requirements describe how closely the actual physical traces should track the desired traces. These requirements are typically defined for specific, simple input traces such as step or ramp sequences, and thus are not applicable to arbitrary inputs. This limits the availability of oracles for CPSs. Our recent work proposes an approach to testing CPSs using control-theoretical design assumptions instead of requirements. This approach circumvents the oracle problem by leveraging the control-theoretical guarantees that are provided when the design assumptions are satisfied. To address the test case generation and oracle problems, researchers have proposed metamorphic testing, which is based on the study of relations across tests, i.e., metamorphic relations (MRs).In this work, we define MRs based on the design assumptions and explore combinations of these MRs using genetic programming to generate CPS test cases. This enables the generation of CPS input traces with potentially arbitrary shapes, together with associated expected output traces. We use the deviation from the expected output traces to guide the generation of input traces that falsify the MRs. Our experiment results show that the MR-falsification provides engineers with new information, helping them identify passed and failed test cases. Furthermore, we show that the generation of traces that falsify the MRs is a non-trivial problem, which cannot be addressed with a random generation approach but is successfully addressed by our approach based on genetic search.

editorial reviewed

Statutory law is subject to change as legislation develops over time – new regulation can be introduced, while existing regulation can be amended, or repealed. From a requirements engineering (RE) perspective, such change must be dealt with to ensure the compliance of software systems at all times. Understanding the implications of regulatory change on compliance of software requirements requires navigating hundreds of legal provisions. Analyzing instances of regulatory change entirely manually is not only time-consuming, but also risky, since missing a change may result in non-compliant software which can in turn lead to hefty fines. In this paper, we propose MURCIA, an automated approach that leverages recent language models to assist human analysts in analyzing regulatory changes. To build MURCIA, we define a taxonomy that characterizes the regulatory changes at the textual level as well as the changes in the text's meaning and legal interpretation. We evaluate MURCIA on four regulations from the financial domain. Over our evaluation set, MURCIA can identify textual changes with F1 score of 90.5%, and it can provide, according to our taxonomy, the text meaning and legal interpretation with an F1 score of 90.8% and 83.7%, respectively.

This paper reports on the experience of building a content model in collaboration with a national financial supervisory authority, with the goal of automating the compliance checking activity performed by the agents of the supervisory authority on fund documentation. The work is focused on modelling content requirements found in the law, i.e., deontic rules prescribing that some information is contained in an official document. For such requirements, the main modelling effort revolves around the required content and its information types. We therefore designed a process to build a content model, elaborating design criteria for the model which partly depend on the use case encompassing compliance checking. We built the content model through iterative interactions between a knowledge engineer and domain experts designed to ensure that the model is not limited to representing only the letter of the law, but rather represents the relevant distinctions in the practice of compliance checking. We drew lessons learned regarding the need for setting up classification criteria for information types and handling the trade-off between expressivity and maintainability of the model.

Abstract With the increasing complexity and scope of software systems, their dependability is crucial. The analysis of log data recorded during system execution can enable engineers to automatically predict failures at run time. Several Machine Learning (ML) techniques, including traditional ML and Deep Learning (DL), have been proposed to automate such tasks. However, current empirical studies are limited in terms of covering all main DL types—Recurrent Neural Network (RNN), Convolutional Neural Network (CNN), and transformer—as well as examining them on a wide range of diverse datasets. In this paper, we aim to address these issues by systematically investigating the combination of log data embedding strategies and DL types for failure prediction. To that end, we propose a modular architecture to accommodate various configurations of embedding strategies and DL-based encoders. To further investigate how dataset characteristics such as dataset size and failure percentage affect model accuracy, we synthesised 360 datasets, with varying characteristics, for three distinct system behavioural models, based on a systematic and automated generation approach. Using the F1 score metric, our results show that the best overall performing configuration is a CNN-based encoder with Logkey2vec. Additionally, we provide specific dataset conditions, namely a dataset size $$>350$$ > 350 or a failure percentage $$>7.5\%$$ > 7.5 % , under which this configuration demonstrates high accuracy for failure prediction.

Software systems log massive amounts of data, recording important runtime information. Such logs are used, for example, for log-based anomaly detection, which aims to automatically detect abnormal behaviors of the system under analysis by processing the information recorded in its logs. Many log-based anomaly detection techniques based on deep learning models include a pre-processing step called log parsing. However, understanding the impact of log parsing on the accuracy of anomaly detection techniques has received surprisingly little attention so far. Investigating what are the key properties log parsing techniques should ideally have to help anomaly detection is therefore warranted. In this paper, we report on a comprehensive empirical study on the impact of log parsing on anomaly detection accuracy, using 13 log parsing techniques, seven anomly detection techniques (five based on deep learning and two based on traditional machine learning) on three publicly available log datasets. Our empirical results show that, despite what is widely assumed, there is no strong correlation between log parsing accuracy and anomaly detection accuracy, regardless of the metric used for measuring log parsing accuracy. Moreover, we experimentally confirm existing theoretical results showing that it is a property that we refer to as distinguishability in log parsing results-as opposed to their accuracy-that plays an essential role in achieving accurate anomaly detection.

Data entry forms use completeness requirements to specify the fields that are required or optional to fill for collecting necessary information from different types of users. However, because of the evolving nature of software, some required fields may not be applicable for certain types of users anymore. Nevertheless, they may still be incorrectly marked as required in the form; we call such fields obsolete required fields. Since obsolete required fields usually have “not-null” validation checks before submitting the form, users have to enter meaningless values in such fields to complete the form submission. These meaningless values threaten the quality of the filled data and could negatively affect stakeholders or learning-based tools that use the data. To avoid users filling meaningless values, existing techniques usually rely on manually written rules to identify the obsolete required fields and relax their completeness requirements. However, these techniques are ineffective and costly. In this article, we propose LACQUER, a learning-based automated approach for relaxing the completeness requirements of data entry forms. LACQUER builds Bayesian Network models to automatically learn conditions under which users had to fill meaningless values. To improve its learning ability, LACQUER identifies the cases where a required field is only applicable for a small group of users and uses SMOTE, an oversampling technique, to generate more instances on such fields for effectively mining dependencies on them. During the data entry session, LACQUER predicts the completeness requirement of a target based on the already filled fields and their conditional dependencies in the trained model. Our experimental results show that LACQUER can accurately relax the completeness requirements of required fields in data entry forms with precision values ranging between 0.76 and 0.90 on different datasets. LACQUER can prevent users from filling 20% to 64% of meaningless values, with negative predictive values (i.e., the ability to correctly predict a field as “optional”) between 0.72 and 0.91. Furthermore, LACQUER is efficient; it takes at most 839 ms to predict the completeness requirement of an instance.

Models such as finite state automata are widely used to abstract the behavior of software systems by capturing the sequences of events observable during their execution. Nevertheless, models rarely exist in practice and, when they do, get easily outdated; moreover, manually building and maintaining models is costly and error-prone. As a result, a variety of model inference methods that automatically construct models from execution traces have been proposed to address these issues. However, performing a systematic and reliable accuracy assessment of inferred models remains an open problem. Even when a reference model is given, most existing model accuracy assessment methods may return misleading and biased results. This is mainly due to their reliance on statistical estimators over a finite number of randomly generated traces, introducing avoidable uncertainty about the estimation and being sensitive to the parameters of the random trace generative process. This article addresses this problem by developing a systematic approach based on analytic combinatorics that minimizes bias and uncertainty in model accuracy assessment by replacing statistical estimation with deterministic accuracy measures. We experimentally demonstrate the consistency and applicability of our approach by assessing the accuracy of models inferred by state-of-the-art inference tools against reference models from established specification mining benchmarks.

Cyber-physical Systems (CPSs) are often safety-critical and deployed in uncertain environments. Identifying scenarios where CPSs do not comply with requirements is fundamental but difficult due to the multidisciplinary nature of CPSs. We investigate the testing of control-based CPSs, where control and software engineers develop the software collaboratively. Control engineers make design assumptions during system development to leverage control theory and obtain guarantees on CPS behaviour. In the implemented system, however, such assumptions are not always satisfied, and their falsification can lead the loss of guarantees. We define stress testing of control-based CPSs as generating tests to falsify such design assumptions. We highlight different types of assumptions, focusing on the use of linearised physics models. To generate stress tests falsifying such assumptions, we leverage control theory to qualitatively characterise the input space of a control-based CPS. We propose a novel test parametrisation for control-based CPSs and use it with the input space characterisation to develop a stress testing approach. We evaluate our approach on three case study systems, including a drone, a continuous-current motor (in five configurations), and an aircraft. Our results show the effectiveness of the proposed testing approach in falsifying the design assumptions and highlighting the causes of assumption violations.

Advances in Artificial Intelligence (AI), and in particular in Machine Learning (ML), are introducing profound changes to scholarly submissions across publication venues, affecting in particular the contributions that are being submitted to Software Engineering (SE) conferences and journals. In this context, it is not always clear whether manuscripts submitted to SE venues under the umbrella term SE for AI are indeed relevant to SE, in the sense that they explicitly contain contributions to the SE body of knowledge. This leads to recurring discussions on whether certain AI-related submissions are appropriate to SE venues, or should instead be submitted to other journals and conferences, including AI or ML-specific ones. In this editorial, we discuss the kinds of AI-related contributions that are a better fit-and a less good fit-for publication in the IEEE Transactions on Software Engineering.

Abstract This short paper takes initial steps towards developing a novel approach, called log slicing, that aims to answer a practical question in the field of log analysis: Can we automatically identify log messages related to a specific message (e.g., an error message)? The basic idea behind log slicing is that we can consider how different log messages are “computationally related” to each other by looking at the corresponding logging statements in the source code. These logging statements are identified by 1) computing a backwards program slice, using as criterion the logging statement that generated a problematic log message; and 2) extending that slice to include relevant logging statements. The paper presents a problem definition of log slicing, describes an initial approach for log slicing, and discusses a key open issue that can lead towards new research directions.

Users frequently interact with software systems through data entry forms. However, form filling is time-consuming and error-prone. Although several techniques have been proposed to auto-complete or pre-fill fields in the forms, they provide limited support to help users fill categorical fields, i.e., fields that require users to choose the right value among a large set of options. In this article, we propose LAFF, a learning-based automated approach for filling categorical fields in data entry forms. LAFF first builds Bayesian Network models by learning field dependencies from a set of historical input instances, representing the values of the fields that have been filled in the past. To improve its learning ability, LAFF uses local modeling to effectively mine the local dependencies of fields in a cluster of input instances. During the form filling phase, LAFF uses such models to predict possible values of a target field, based on the values in the already-filled fields of the form and their dependencies; the predicted values (endorsed based on field dependencies and prediction confidence) are then provided to the end-user as a list of suggestions. We evaluated LAFF by assessing its effectiveness and efficiency in form filling on two datasets, one of them proprietary from the banking domain. Experimental results show that LAFF is able to provide accurate suggestions with a Mean Reciprocal Rank value above 0.73. Furthermore, LAFF is efficient, requiring at most 317 ms per suggestion.

Trace checking is a verification technique widely used in Cyber-physical system (CPS) development, to verify whether execution traces satisfy or violate properties expressing system requirements. Often these properties characterize complex signal behaviors and are defined using domain-specific languages, such as SB-TemPsy-DSL, a pattern-based specification language for signal-based temporal properties. Most of the trace-checking tools only yield a Boolean verdict. However, when a property is violated by a trace, engineers usually inspect the trace to understand the cause of the violation; such manual diagnostic is time-consuming and error-prone. Existing approaches that complement trace-checking tools with diagnostic capabilities either produce low-level explanations that are hardly comprehensible by engineers or do not support complex signal-based temporal properties. In this paper, we proposeTD-SB-TemPsy, a trace-diagnostic approach for properties expressed using SB-TemPsy-DSL. Given a property and a trace that violates the property,TD-SB-TemPsydetermines the root cause of the property violation.TD-SB-TemPsyrelies on the concepts ofviolation cause, which characterizes one of the behaviors of the system that may lead to a property violation, anddiagnoses, which are associated with violation causes and provide additional information to help engineers understand the violation cause. As part ofTD-SB-TemPsy, we propose a language-agnostic methodology to define violation causes and diagnoses. In our context, its application resulted in a catalog of 34 violation causes, each associated with one diagnosis, tailored to properties expressed in SB-TemPsy-DSL. We assessed the applicability ofTD-SB-TemPsyon two datasets, including one based on a complex industrial case study. The results show thatTD-SB-TemPsycould finish within a timeout of 1 min for$\approx 83.66\%$of the trace-property combinations in the industrial dataset, yielding a diagnosis in$\approx 99.84\%$of these cases; moreover, it also yielded a diagnosis for all the trace-property combinations in the other dataset. These results suggest that our tool is applicable and efficient in most cases.

Log message template identification aims to convert raw logs containing free-formed log messages into structured logs to be processed by automated log-based analysis, such as anomaly detection and model inference. While many techniques have been proposed in the literature, only two recent studies provide a comprehensive evaluation and comparison of the techniques using an established benchmark composed of real-world logs. Nevertheless, we argue that both studies have the following issues: (1) they used different accuracy metrics without comparison between them, (2) some ground-truth (oracle) templates are incorrect, and (3) the accuracy evaluation results do not provide any information regarding incorrectly identified templates.

Abstract Behavioral software models play a key role in many software engineering tasks; unfortunately, these models either are not available during software development or, if available, quickly become outdated as implementations evolve. Model inference techniques have been proposed as a viable solution to extract finite state models from execution logs. However, existing techniques do not scale well when processing very large logs that can be commonly found in practice. In this paper, we address the scalability problem of inferring the model of a component-based system from large system logs, without requiring any extra information. Our model inference technique, called PRINS, follows a divide-and-conquer approach. The idea is to first infer a model of each system component from the corresponding logs; then, the individual component models are merged together taking into account the flow of events across components, as reflected in the logs. We evaluated PRINS in terms of scalability and accuracy, using nine datasets composed of logs extracted from publicly available benchmarks and a personal computer running desktop business applications. The results show that PRINS can process large logs much faster than a publicly available and well-known state-of-the-art tool, without significantly compromising the accuracy of inferred models.

Cyber-physical systems combine software and physical components. Specification-driven trace-checking tools for CPS usually provide users with a specification language to express the requirements of interest, and an automatic procedure to check whether these requirements hold on the execution traces of a CPS. Although there exist several specification languages for CPS, they are often not sufficiently expressive to allow the specification of complex CPS properties related to the software and the physical components and their interactions. In this paper, we propose (i) the Hybrid Logic of Signals (HLS), a logic-based language that allows the specification of complex CPS requirements, and (ii) ThEodorE, an efficient SMT-based trace-checking procedure. This procedure reduces the problem of checking a CPS requirement over an execution trace, to checking the satisfiability of an SMT formula. We evaluated our contributions by using a representative industrial case study in the satellite domain. We assessed the expressiveness of HLS by considering 212 requirements of our case study. HLS could express all the 212 requirements. We also assessed the applicability of ThEodorE by running the trace-checking procedure for 747 trace-requirement combinations. ThEodorE was able to produce a verdict in 74.5% of the cases. Finally, we compared HLS and ThEodorE with other specification languages and trace-checking tools from the literature. Our results show that, from a practical standpoint, our approach offers a better trade-off between expressiveness and performance.

Regression testing is arguably one of the most important activities in software testing. However, its cost-effectiveness and usefulness can be largely impaired by complex system test cases that are poorly designed (e.g., test cases containing multiple test scenarios combined into a single test case) and that require a large amount of time and resources to run. One way to mitigate this issue is decomposing such system test cases into smaller, separate test cases---each of them with only one test scenario and with its corresponding assertions---so that the execution time of the decomposed test cases is lower than the original test cases, while the test effectiveness of the original test cases is preserved. This decomposition can be achieved with program slicing techniques, since test cases are software programs too. However, existing static and dynamic slicing techniques exhibit limitations when (1) the test cases use external resources, (2) code instrumentation is not a viable option, and (3) test execution is expensive.

Signal-based temporal properties (SBTPs) characterize the behavior of a system when its inputs and outputs are signals over time; they are very common for the requirements specification of cyber-physical systems. Although there exist several specification languages for expressing SBTPs, such languages either do not easily allow the specification of important types of properties (such as spike or oscillatory behaviors), or are not supported by (efficient) trace-checking procedures.

Malicious users can attack Web applications by exploiting injection vulnerabilities in the source code. This work addresses the challenge of detecting injection vulnerabilities in the server-side code of Java Web applications in a scalable and effective way. We propose an integrated approach that seamlessly combines security slicing with hybrid constraint solving; the latter orchestrates automata-based solving with meta-heuristic search. We use static analysis to extract minimal program slices relevant to security from Web programs and to generate attack conditions. We then apply hybrid constraint solving to determine the satisfiability of attack conditions and thus detect vulnerabilities. The experimental results, using a benchmark comprising a set of diverse and representative Web applications/services as well as security benchmark applications, show that our approach (implemented in the JOACO tool) is significantly more effective at detecting injection vulnerabilities than state-of-the-art approaches, achieving 98 percent recall, without producing any false alarm. We also compared the constraint solving module of our approach with state-of-the-art constraint solvers, using six different benchmark suites; our approach correctly solved the highest number of constraints (665 out of 672), without producing any incorrect result, and was the one with the least number of time-out/failing cases. In both scenarios, the execution time was practically acceptable, given the offline nature of vulnerability detection.

Abstract Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

Many software engineering activities process the events contained in log files. However, before performing any processing activity, it is necessary to parse the entries in a log file, to retrieve the actual events recorded in the log. Each event is denoted by a log message, which is composed of a fixed part---called (event) template---that is the same for all occurrences of the same event type, and a variable part, which may vary with each event occurrence. The formats of log messages, in complex and evolving systems, have numerous variations, are typically not entirely known, and change on a frequent basis; therefore, they need to be identified automatically.

A Role-based Access Control (RBAC) mechanism prevents unauthorized users to perform an operation, according to authorization policies which are defined on the user’s role within an enterprise. Several models have been proposed to specify complex RBAC policies. However, existing approaches for policy enforcement do not fully support all the types of policies that can be expressed in these models, which hinders their adoption among practitioners. In this paper we propose a model-driven enforcement framework for complex policies captured by GemRBAC+CTX, a comprehensive RBAC model proposed in the literature. We reduce the problem of making an access decision to checking whether a system state (from an RBAC point of view), expressed as an instance of the GemRBAC+CTX model, satisfies the constraints corresponding to the RBAC policies to be enforced at run time. We provide enforcement algorithms for various types of access requests and events, and a prototype tool (MORRO) implementing them. We also show how to integrate MORRO into an industrial Web application. The evaluation results show the applicability of our approach on a industrial system and its scalability with respect to the various parameters characterizing an AC configuration.

Offline trace checking tools check whether a specification holds on a log of events recorded at run time; they yield a verification verdict (typically a boolean value) when the checking process ends. When the verdict is false, a software engineer needs to diagnose the property violations found in the trace in order to understand their cause and, if needed, decide for corrective actions to be performed on the system. However, a boolean verdict may not be informative enough to perform trace diagnostics, since it does not provide any useful information about the cause of the violation and because a property can be violated for multiple reasons.

Constraint solving is an essential technique for detecting vulnerabilities in programs, since it can reason about input sanitization and validation operations performed on user inputs. However, real-world programs typically contain complex string operations that challenge vulnerability detection. State-of-the-art string constraint solvers support only a limited set of string operations and fail when they encounter an unsupported one, this leads to limited effectiveness in finding vulnerabilities. In this paper we propose a search-driven constraint solving technique that complements the support for complex string operations provided by any existing string constraint solver. Our technique uses a hybrid constraint solving procedure based on the Ant Colony Optimization meta-heuristic. The idea is to execute it as a fallback mechanism, only when a solver encounters a constraint containing an operation that it does not support. We have implemented the proposed search-driven constraint solving technique in the ACO-Solver tool, which we have evaluated in the context of injection and XSS vulnerability detection for Java Web applications. We have assessed the benefits and costs of combining the proposed technique with two state-of-the-art constraint solvers (Z3-str2 and CVC4). The experimental results, based on a benchmark with 104 constraints derived from nine realistic Web applications, show that our approach, when combined in a state-of-the-art solver, significantly improves the number of detected vulnerabilities (from 4.7% to 71.9% for Z3-str2, from 85.9% to 100.0% for CVC4), and solves several cases on which the solver fails when used stand-alone (46 more solved cases for Z3-str2, and 11 more for CVC4), while still keeping the execution time affordable in practice.

Trace checking is a procedure for evaluating requirements over a log of events produced by a system. This paper deals with the problem of performing trace checking of temporal properties expressed in TemPsy, a pattern-based specification language. The goal of the paper is to present a scalable and practical solution for trace checking, which can be used in contexts where relying on model-driven engineering standards and tools for property checking is a fundamental prerequisite.The main contributions of the paper are: a model-driven trace checking procedure, which relies on the efficient mapping of temporal requirements written in TemPsy into OCL constraints on a conceptual model of execution traces; the implementation of this trace checking procedure in the TEMPSY-CHECK tool; the evaluation of the scalability of TEMPSY-CHECK, applied to the verification of real properties derived from a case study of our industrial partner, including a comparison with a state-of-the-art alternative technology based on temporal logic. The results of the evaluation show the feasibility of applying our model-driven approach for trace checking in realistic settings: TEMPSY-CHECK scales linearly with respect to the length of the input trace and can analyze traces with one million events in about two seconds.

JoanAudit is a static analysis tool to assist security auditors in auditing Web applications and Web services for common injection vulnerabilities during software development. It automatically identifies parts of the program code that are relevant for security and generates an HTML report to guide security auditors audit the source code in a scalable way. JoanAudit is configured with various security-sensitive input sources and sinks relevant to injection vulnerabilities and standard sanitization procedures that prevent these vulnerabilities. It can also automatically fix some cases of vulnerabilities in source code — cases where inputs are directly used in sinks without any form of sanitization — by using standard sanitization procedures. Our evaluation shows that by using JoanAudit, security auditors are required to inspect only 1% of the total code for auditing common injection vulnerabilities. The screen-cast demo is available at https://github.com/julianthome/joanaudit.

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval of the formula to be checked. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches.

A role-based access control (RBAC) policy restricts a user to perform operations based on her role within an organization. Several RBAC models have been proposed to represent different types of RBAC policies. However, the expressiveness of these models has not been matched by specification languages for RBAC policies. Indeed, existing policy specification languages do not support all the types of RBAC policies defined in the literature.

PESOS 2013 is a forum that brings together software engineering researchers from academia and industry, as well as practitioners working in the areas of service-oriented systems to discuss research challenges, recent developments, novel application scenarios, as well as methods, techniques, experiences, and tools to support engineering, evolution and adaptation of service-oriented systems. The special theme of the 5th edition of PESOS is “Service Engineering for the Cloud” The goal is to explore approaches to better engineer service-oriented systems, to either take advantage of the qualities offered by cloud infrastructures or to account for lack of full control over important quality attributes. PESOS 2013 also continues to be the key forum for collecting case studies and artifacts for educators and researchers in this area.

Specification patterns have proven to help developers to state precise system requirements, as well as formalize them by means of dedicated specification languages. Most of the past work has focused its applicability area to the specification of concurrent and real-time systems, and has been limited to a research setting. In this paper we present the results of our study on specification patterns for service-based applications (SBAs). The study focuses on industrial SBAs in the banking domain. We started by performing an extensive analysis of the usage of specification patterns in published research case studies - representing almost ten years of research in the area of specification, verification, and validation of SBAs. We then compared these patterns with a large body of specifications written by our industrial partner over a similar time period. The paper discusses the outcome of this comparison, indicating that some needs of the industry, especially in the area of requirements specification languages, are not fully met by current software engineering research.

Service-based applications can be realized by composing existing services into new, added-value composite services. The external services with which a service composition interacts are usually known by means of their syntactical interface. However, an interface providing more information, such as a behavioral specification, could be more useful to a service integrator for assessing that a certain external service can contribute to fulfill the functional requirements of the composite application.

SOABench is a framework for the automatic generation, execution and analysis of testbeds for evaluating the performance of service-oriented middleware. Testbeds can be characterized in terms of the composite services to execute, the workload to generate, the deployment configuration to use, the performance metrics to gather, the data analyses to perform on them, and the reports to produce.

Middleware for Web service compositions, such as BPEL engines, provides the execution environment for services as well as additional functionalities, such as monitoring and self-tuning. Given its role in service provisioning, it is very important to assess the performance of middleware in the context of a SOA. This paper presents SOABench, a framework for the automatic generation and execution of testbeds for benchmarking middleware for composite Web services and for assessing the performance of existing SOA infrastructures. SOABench defines a testbed model characterized by the composite services to execute, the workload to generate, the deployment configuration to use, the performance metrics to gather, the data analyses to perform on them, and the reports to produce. We have validated SOABench by benchmarking the performance of different BPEL engines.

REMAN is a reputation management infrastructure for composite Web services. It supports the aggregation of client feedback on the perceived QoS of external services, using reputation mechanisms to build service rankings. Changes in rankings are pro-actively notified to composite service clients to enable self-tuning properties in their execution.

The dependability of composite services is largely affected by their constituent Web services. Composite services have to operate in an open and dynamically changing environment in order to leverage the best performing services available at the moment. Hence, there is the need for an efficient mechanism to provide reliable service rankings. In this paper we present a novel, generic, and customizable reputation infrastructure to automatically and transparently monitor the execution of composite services, taking both functional and non-functional properties into account. The experienced Web service quality-of-service is communicated to a configurable reputation mechanism that publishes service rankings. Our reputation infrastructure supports notifications upon changes in service reputation, enabling self-tuning and self-healing properties in the execution of composite services. We implemented our architecture using standard technologies, such as BPEL and JavaEE. Performance measurements show that our infrastructure causes only moderate overhead.

Web service based applications are expected to live in dynamically evolving settings. At run-time, services may undergo changes that could modify their expected behavior. Because of such intrinsic dynamic nature, applications should be designed by adhering to the principles of design- by-contract. Run-time monitoring is needed to check that the contract between service providers and service users is fulfilled while the collaboration is in place. We describe a language to specify the expected functional and non-functional requirements that a service provider should fulfill. The language (timed WSCoL) is a temporal extension of a previous proposal (WSCoL). We also illustrate the architecture of a run-time analyzer that checks timed WSCoL properties. Should such properties be disproved during execution, appropriate recovery and reconfiguration actions may be put in place.