Behavioral model diagrams, e.g., sequence diagrams, are an essential form of documentation that are typically designed by system engineers from requirements documentation, either fully manually or assisted by design tools. With the growing use of Large Language Models (LLM) as AI modeling assistants, more automation will be involved in generating diagrams. This necessitates the advancement of automatic model correctness evaluation tools. Such a tool can be used to evaluate both manually and AI automatically generated models; to provide feedback to system engineers, and enable AI assistants to self-evaluate and self-enhance their generated models. In this paper, we propose MCeT, the first fully automated tool to evaluate the correctness of a behavioral model, sequence diagrams in particular, against its corresponding requirements text and produce a list of issues that the model has. We utilize LLMs for the correctness evaluation tasks as they have shown outstanding natural language understanding ability. However, we show that directly asking an LLM to compare a diagram to requirements finds less than 35% of issues that experienced engineers can find. We propose to supplement the direct check with a fine-grained, multi-perspective approach; we split the diagram into atomic, non-divisible interactions, and split the requirements text into atomic, self-contained items. We compare the diagram with atomic requirements and each diagramatom with the requirements. We also propose a self-consistency checking approach that combines perspectives to mitigate LLM hallucinated issues. Our combined approach improves upon the precision of the direct approach from 0.58 to 0.81 in a dataset of real requirements. Moreover, the approach finds 90% more issues that the experienced engineers found than the direct approach, and reports an average of 6 new issues per diagram.

Graph model generation from natural language description is an important task with many applications in software engineering. With the rise of large language models (LLMs), there is a growing interest in using LLMs for graph model generation. Nevertheless, LLM-based graph model generation typically produces partially correct models that suffer from three main issues: (1) syntax violations: the generated model may not adhere to the syntax defined by its metamodel, (2) constraint inconsistencies: the structure of the model might not conform to some domain-specific constraints, and (3) inaccuracy: due to the inherent uncertainty in LLMs, the models can include inaccurate, hallucinated elements. While the first issue is often addressed through techniques such as constraint decoding or filtering, the latter two remain largely unaddressed. Motivated by recent self-consistency approaches in LLMs, we propose a novel abstraction-concretization framework that enhances the consistency and quality of generated graph models by considering multiple outputs from an LLM. Our approach first constructs a probabilistic partial model that aggregates all candidate outputs and then refines this partial model into the most appropriate concrete model that satisfies all constraints. We evaluate our framework on several popular open-source and closed-source LLMs using diverse datasets for model generation tasks. The results demonstrate that our approach significantly improves both the consistency and quality of the generated graph models.

Prime compilation aims to generate all prime implicates/implicants of a Boolean formula. Recently, prime compilation of non-clausal formulae has received great attention. Since it is hard for$\Sigma_{2}^{P}$, existing methods have performance issues. We argue that the main performance bottleneck stems from enlarging the search space using dual rail (DR) encoding, and computing a minimal clausal formula as a by-product. To deal with the issue, we propose a two-phase approach, namely CoAPI, for prime compilation of non-clausal formulae. Thanks to the two-phase framework, we construct a clausal formula without using DR encoding. In addition, to improve performance, the key in our work is a novel bounded prime extraction (BPE) method that, interleaving extracting prime implicates with extracting small implicates, enables constructing a succinct clausal formula rather than a minimal one. Following the assessment way of the state-of-the-art (SOTA) work, we show that CoAPI achieves SOTA performance. Particularly, for generating all prime implicates, CoAPI is up to about one order of magnitude faster. Moreover, we evaluate CoAPI on a benchmark sourcing from real-world industries. The results also confirm the outperformance of CoAPI11Our code and benchmarks are publicly available at https://github.com/LuoWeiLinWillam/CoAPI.

Fault tree analysis (FTA) is a prominent reliability analysis method, which is widely used in safety-critical industries. Computing the minimal cut sets (MCSs) of a fault tree, i.e., finding all the smallest combinations of the basic events that cause system failures, is a fundamental step in FTA. Since coherent fault trees are the most common in industrial systems in practice, they are the focus of this article. Computing MCSs is a computationally hard problem. Classical methods have been proposed based on manipulation of Boolean expressions and binary decision diagrams. However, given the inherent intractability of computing MCSs in practice, there are still limitations on time and memory in these methods. Therefore, developing new methods over different paradigms remains to be an interesting research direction. In this article, motivated by recent progress on modern Boolean satisfiability problem (SAT) solvers, we present a new method for computing MCSs based on SAT, namely SATMCS. Specifically, given a fault tree, we iteratively search for a cut set based on the conflict-driven clause learning framework. By exploiting local propagation graph, which characterizes the partial failure propagation based on the cut set, we provide efficient algorithms for extracting an MCS. The new MCS is learned as a block clause for SAT solving, and the conflict clauses in iterations are incrementally recorded, which helps to prune search space and ensures completeness of the results. Moreover, we adopt a jump-chronological backtracking strategy to prepare the next iteration, which allows for reusing the same search steps in SAT solving. We compare SATMCS with state-of-the-art commercial tools on practical fault trees. Although SATMCS is only a prototype, it shows comparable performance in time consumption with one tool (XFTA), and in various cases, it outperforms the others (FaultTree+ and Commander). Besides, SATMCS exhibits much better performance on memory usage than these tools. Specifically, SATMCS consumes about one order of magnitude less memory usage in most instances.

Fault tree analysis (FTA) is a prominent reliability analysis method widely used in safety-critical industries. Computing minimal cut sets (MCSs), i.e., finding all the smallest combination of basic events that result in the top level event, plays a fundamental role in FTA. Classical methods have been proposed based on manipulation of boolean expressions of fault trees and Binary Decision Diagrams. However, given the inherent intractability of computing MCSs, developing new methods over different paradigms remains to be an interesting research direction. In this paper, motivated by recent progress on modern SAT solver, we present a new method for computing MCSs based on SAT solving. Specifically, given a fault tree, we iteratively search for a cut set based on the DPLL framework. By exploiting local failure propagation paths in the fault tree, we provide efficient algorithms for extracting an MCS from the cut set. The information of a new MCS is learned as a blocking clause for SAT solving, which helps to prune search space and ensures completeness of the results. We compare our method with a popular commercial FTA tool on practical fault trees. Preliminary results show that our method exhibits better performance on time and memory usage.

A context-sensitive probabilistic Boolean network with perturbation (CS-PBNp) closely models gene regulatory networks under external controls that alter the evolution of the networks in a desirable way over a finite time horizon. In this paper, we consider optimal control for a CS-PBNp, proposing an approach, based on a formal verification technique - probabilistic model checking, for finding optimal control policy that minimizes the expected cost over the entire control horizon. To this end, we first present a detailed procedure of modeling a CS-PBNp using the modeling language of a widely used probabilistic model checker PRISM. Furthermore, by analyzing computation of reward-based temporal properties, we provide a reduction approach allowing us to formulate the optimal control problem as minimum reachability reward properties. Based on this result, we incorporate control and state cost information into the PRISM code of a CS-PBNp such that automated model checking a minimum reachability reward property on the code gives the solution to the optimal control problem. Experiment results on an apoptosis network demonstrate the feasibility and effectiveness of our approach.

Runtime monitoring can be used to verify, enforce and control the dynamic execution of a target program at runtime to detect property violations, enforce desired properties and actively correct the execution, respectively. However, the state-of-the-art study lacks an appropriate formal program semantics of runtime monitoring. In this paper, we propose a theory of runtime control at an appropriate level of formalization to provide a formal program semantics of instrumented target programs under the control of controlling programs. Our theory provides a complete formal semantics for real implementations of runtime monitoring and control, but still retains a good balance between implementation and generality. Indeed, the theory encompasses the formalization of key implementation techniques, such as program instrumentation, synchronization on passively monitored actions, and synthesis of controlling programs from specifications. On the other hand, the theory is so generic and expressive that many existing formalisms about runtime monitoring can be considered as special cases of our theory.

Multi-valued models, with additional logic values to capture the degree of uncertainty, support modeling and reasoning about systems with partial and inconsistent information. A mixed simulation, often used in abstract model checking, describes the connection between behaviors of two models and defines a precision order. In this paper, we derive a new notion of mixed simulation of multi-valued models such that the precision order is logically characterized by multi-valued semantics of propositional μ-calculus, it generalizes previous notion of mixed simulation for any multi-valued logic. Our work is based on bilattices, consisting of both a truth ordering and an information ordering. We first define the mixed simulation of multi-valued models over world-based bilattices using a model reduction approach, show the logical characterization result, and discuss three stronger variants of our notion. We then extend the result for any multi-valued logic through lattice embedding.