The Doctoral School in Science and Engineering is happy to invite you to Luiz Matheus DE ALENCAR CARVALHO’s defence entitled
Enhancing LTL Specifications and Solver Reliability through Search Techniques
Supervisor: Assoc. Prof Mike PAPADAKIS
Linear temporal logic (LTL) is a powerful logical formalism that includes descriptive operators for future events that deal with concurrent behaviors. LTL has a general set of operators that impose high expressiveness and complexity. The formalism includes safety, liveness, and fairness properties. LTL is commonly used as a specification language for distributed, concurrent, and hardware systems. Moreover, LTL is a common formalism in Goal-Oriented Requirements Engineering (GORE). The requirement methodology has taken advantage of the analysis techniques associated with LTL. In this manner, we present ACoRe, an automated approach to resolve goal-conflicts in requirements specifications expressed in LTL. ACoRe explores syntactic modifications of the specifications to remove all the previously identified conflicts while preserving consistency. Moreover, ACoRe also computes the syntactic and semantic similarity, in which the syntactic similarity refers to the distance between the text representations of the original specification and the candidate repair, while the semantic similarity refers to the behavior of the system shared by the original specification and the candidate repair. We evaluated ACoRe on formal specifications collected from the literature and benchmarks. In summary, the empirical results present a reasonable number of repairs in the Pareto-optimal set. Also, we show that ACoRe obtains better results when genetic algorithms are used, as opposed to other search algorithms, measured in terms of quality indicators, while at the same time, it produces more repairs that do not introduce new conflicts.
On the basis of the high level of expressiveness provided by LTL, tools have been created to mine LTL properties based on trace artifacts. A trace describes the relevant events that occur or the behavior changes of concurrent systems. The LTL mining tools analyze patterns or constraints in these traces and propose LTL properties that are valid in the provided traces.
However, there is a gap in the evaluation of the capability of mining tools. For instance, if the tools are able to propose correct properties or reach a soundness set of LTL properties. Therefore, we propose an evaluation of LTL mining tools. First, we assess them based on the capability to find a ground truth set of LTL specifications. Second, we observe the capability to cover the ground truth set of LTL specifications. Our evaluation shows that the mining tools do not find LTL properties in a ground truth composed of formal specifications. Moreover, the experiment also indicates that the mining tools have low precision in the semantic coverage of the ground truth. The empirical results suggest that enriching or completing existing specifications by mining additional LTL traces is still an open research area, and the current tools are useless for improving existing specifications.
Furthermore, LTL solvers have been proposed to address the LTL satisfiability problem. In an effort to answer the satisfiability problem, the LTL solvers were designed around several algorithms. Among the additional efforts made, developments have also been made in terms of improving performance gains. Among the applications are complex contexts such as program analysis, software verification, symbolic execution, program synthesis, model checking, and artificial intelligence reasoning. These application domains generally require high-quality standards.
Our work also presents a new fuzzing technique for LTL solvers based on a search-based approach called SpecBCFuzz. Among the fitness functions, the boundary conditions are extensively evaluated during the search process, which progressively resolves the boundary conditions in the LTL specifications that were provided as seeds. Thus, the evolved specifications are valid repairs for the previously identified diverges. We claim that the search process for resolving boundary conditions efficiently produces failure-inducing input. Moreover, additional fitness, such as semantic and syntactic similarities, can constrain the search space and maintain the seeds given by the specifications as representative of realistic LTL specifications.
Our empirical evaluation relies on differential fuzzing testing and inconsistency patterns. The result suggests that SpecBCFuzz is significantly more efficient than a baseline approach (e.g., LTL probabilistic grammar fuzzing). In addition, the empirical study points out a more significant size effect of the inconsistency patterns identified during the execution of the empirical study. Furthermore, our empirical evaluation presents 16 bugs in the evaluated LTL solvers, detecting bugs in 18 out of the 21 solvers’ configurations we study. In addition, we present performance warning patterns. The set of warning patterns has the potential to indicate improvements in a particular solver for releases, heuristics set, or theoretical guidelines for a specific type of LTL satisfiability algorithm.
Moreover, we modify portfolio decisions to incorporate a confirmation answer. In other words, the portfolio does not provide the fastest answer. The portfolio replicates the answer when at least two solvers agree on a given input. It was formulated based on our previous study that identified bugs in LTL solvers and demonstrated that a considerable number of these bugs are not inherent to a single input across different solvers. Our empirical results present bugs in the pure portfolio, whereas a search-based fuzzing approach does not find a single bug for the reliable portfolio. Furthermore, we also evaluated the reliable portfolio in terms of performance. The empirical results present the lowest runtime for the reliable portfolio compared to a single robust LTL solver (NuSMV). In summary, a reliable portfolio is capable of increasing soundness in LTL solvers and is also associated with a gain in performance compared to an individual LTL solver that contains a high level of soundness.