We propose RDC-SAT, a novel approach to optimize splitting heuristics in Divide-and-Conquer SAT solvers using deep reinforcement learning. Our method dynamically extracts features from the current solving state whenever a split is required. These features, such as learned clauses, variable activity scores, and clause LBD (Literal Block Distance) values, are represented as a graph. A GNN integrated with an Actor-Critic model processes this graph to determine the optimal split variable. Unlike traditional linear state transitions characterized by Markov processes, divide-and-conquer challenges involve tree-like state transitions. To address this, we developed a reinforcement learning environment based on the Painless framework that efficiently handles these transitions. Additionally, we designed different discounted reward functions for satisfiable and unsatisfiable SAT problems, capable of handling tree-like state transitions. We trained our model using the Decentralized Proximal Policy Optimization (DPPO) algorithm on phase transition random 3-SAT problems and implemented the RDC-SAT solver, which operates in both GPU-accelerated and non-GPU modes. Evaluations show that RDC-SAT significantly improves the performance of D\&C solvers on phase transition random 3-SAT datasets and generalizes well to the SAT Competition 2023 dataset, substantially outperforming traditional splitting heuristics.

Model-driven development (MDD) is a mainstream approach in safety-critical domains, providing standardized modeling languages like SysML.SysML behavior models describe system dynamics and are widely used in aerospace, manufacturing, and IoT.However, manual modeling is inefficient and prone to quality issues, restricting MDD's practical adoption.The potential of LLMs in SysML behavior model generation and its challenges remain unclear, making it a key research topic.This empirical study evaluates LLMs in generating three types of SysML behavior models, focusing on performance and hallucinations.Our contributions are twofold:(1) constructing and publishing a dataset of 107 SysML behavior models spanning various domains; (2) analyzing hallucinations in LLM-assisted SysML behavior model generation from syntactic and semantic perspectives and proposing model-checking rules to mitigate them and enhance model quality.We analyze hallucinations in SysML behavior model generation, classifying them and exploring their possible causes.The evaluation results show that while the models generally meet syntactic requirements, they consistently lack semantic accuracy.Across both phases, LLMs achieve over 90% grammar accuracy.For semantic accuracy, the average F1-score for ACT reaches 95%, while SD drops to just 50%.These results demonstrate that while our model-checking rules effectively correct format and syntax, they are insufficient for addressing deeper semantic gaps.Overcoming these challenges requires advanced strategies, such as counterexamples and simulation traces, to provide optimal feedback.Additionally, model-checking in LLM-based generation is costly, and reducing this cost is another critical issue to address in the future.

With the booming development of Internet of Things (IoT), the LoRaWAN protocol, a crucial technology in Low Power Wide Area Network (LPWAN), has attracted academic attention. Numerous studies on the security of LoRaWAN have been proposed, and some of these studies have been rigorously verified. However, there is a lack of a unified verification framework for the LoRaWAN protocol. In this paper, we present a unified, comprehensive, and systematic security verification framework for the LoRaWAN protocol. The framework facilitates the construction of CSP model for the LoRaWAN protocol and enables the implementation of these CSP models in PAT with C#. Additionally, it supports the formal verification of the models. By integrating C# into PAT, our framework gains extensibility, flexibility, and broad applicability. Simultaneously, we introduce intruders in our CSP model to simulate five different types of attacks (Replay attacks, DoS attacks, ACK Spoofing attacks, Bit Flipping attacks, and MITM attacks) to evaluate LoRaWAN’s performance in vulnerable environments. To demonstrate the applicability of our framework, we extend it to higher versions of LoRaWAN and apply it in the manufacturing industry. We not only verify the fundamental properties but also validate the security properties by simulating attacks in PAT. Our work would help to diversely analyze the security aspects related to the LoRaWAN protocol, and provide the foundation for the analysis of enhancing its security and robustness.

A smart legal contract is a legally binding contract in which some or all of the contractual obligations are defined and performed automatically by a computer program. As its software requirement, the legal contract is composed of legal clauses expressing the execution logic and time constraints between events in natural language. When formally verifying a smart legal contract to ensure the requirements’ conformance, it is necessary to translate the time-constrained functional requirements (TFRs) into property specifications like Metric temporal logic (MTL) as the input of a model checker. Instead of costly and error-prone manual writing, this work automates the TFR detection and the specification generation using deep learning, named AutoMTL-Spec. We separate the MTL specification generation approach into four tasks: TFR detection, intermediate representation structure extraction, event sequence/time point extraction, and MTL generation, respectively. We construct a dataset including 43 contracts of four categories, 4608 terms, and 277 TFRs. The experimental results showed that all three models significantly outperform the baselines. Most of the indicators of the three learning tasks reached near to or more than 90%.

Model checking can automatically verify behavioral properties like deadlock-absence and linear temporal logic (LTL) specifications against a design model. When a model violates a property, a model checker can provide counterexamples. How-ever, it requires a lot of effort to identify the root cause. Model fault localization is widely recognized to be an expensive activity. What information in the counterexample can be used, and how to use this information to locate the root cause is still an open issue. We are the first to investigate the learning-based fault localization problem in model checking and propose an approach to locating the root cause in Petri net violating deadlock or LTL properties, called MC-FLoc. MC-FLoc learns fault location from the traces in the state graph of counterexamples. We present effective searching strategies to select faulty and correct traces and design a trace sorting algorithm so that similar traces are gathered to effectively learn the relationship between the nearby units. We construct five learning models and evaluate MC- Floc on a set of cases. The evaluation results show an average EXAM score of less than 13% on the deadlock benchmark and an average EXAM score of less than 20% on the LTL benchmark. This work is useful to practitioners of model checkers for providing a fault localization approach as well as establishing a benchmark for faulty software models. Our prototype and benchmark are publicly available at: https://github.com/MC-Floc/Floc.git.

A software architectural tactic is a design decision for realizing quality goals at the architectural level. With the evolution of code, the designed architectural tactics might be degraded over time. In practice, the existing systems provide limited support for checking the consistency between an architectural tactic and its implementation. Kim et al. specified the generic structure and interaction behavior for a subset of architectural tactics in Role-Based Meta-modeling Language (RBML) to facilitate the design of tactics. Based on Kim et al.'s work, this paper first presents a machine learning-based method to assist users in detecting the behavior methods of the tactic structure in code, then proposes a runtime verification (RV) method for checking the behavioral consistency between the tactic specification in RBML and its implementation. We conducted experiments for the behavioral methods detection approach by comparing five machine learning models on a dataset with seventy-four open-source projects containing ten types of tactics. For each tactic, we selected an open-source project to show the effectiveness of the RV approach. Finally, we design and implement a prototype tool named ArchTacRV to help developers efficiently maintain the architectural tactics.

There are various uncertain disturbances in the actual manufacturing environment, which makes dynamic multiobjective flexible scheduling problem of flexible job shop (MDFJSP) become the research focus in the field of optimal scheduling. In this paper, MDFJSP in the environment of temporary order insertion uncertainty is studied, and a multiobjective dynamic scheduling scheme based on rescheduling index and adaptive nondominated sorting genetic algorithm (NSGA-II) is proposed. First, based on the actual manufacturing environment, the mathematical model of the traditional flexible job shop scheduling problem is improved, and the multiobjective dynamic rescheduling model of flexible work center is established. Then, the existing rescheduling mechanisms are summarized, and a rescheduling hybrid driving mechanism based on the rescheduling index is proposed to enable it to reschedule and drive according to the actual situation. Finally, the shortcomings of the traditional multiobjective scheduling algorithm NSGA-II are analyzed, the adaptive cross mutation strategy and the simplified harmonic normalized distance measure method are proposed to improve it, and an adaptive multiobjective dynamic scheduling algorithm NSGA-II (MDSA-NSGA-II) is formed. To analyze the performance of this algorithm, the performance of this algorithm is compared with five classical flexible job shop multiobjective scheduling algorithms in international general examples, and the effectiveness is verified by real aircraft production examples. The experimental results fully show that MDSA-NSGA-II has good performance in solving MDFJSP.

The timing requirements of real-time systems can be guaranteed by the well-designed scheduling.The analysis of such scheduling inputs an abstract task model of the system and outputs a diagnostic regarding the practicability of the timing requirements.Task models have evolved from periodic models to more sophisticated graph-based ones, among which the digraph real-time (DRT) task model is the most applicable because of its good expressiveness and analysis efficiency.However, the DRT model can't support the precedence constraints within or between tasks.In this paper, we propose a new task model, called the DRTPC model, that extends the DRT model to support the precedence constraint.Further, based on our model, we present a uniprocessor schedulability analysis algorithm for the static priority scheduling, and introduce an optimization technique to improve the analysis efficiency.Our experiments show that, despite the high computational complexity of the problem, our approach scales very well for large sets of tasks with precedence constraints.

Currently, more and more application-specific operating systems (ASOS) are applied in real-time embedded systems.With the development of microkernel technique, the ASOS is usually customized based on the microkernel using the configurable policy, which has various alternatives.In the design of the real-time embedded system (RTES) based on such ASOS, evaluating its timing performance at the early design stage is helpful to guide the designer towards choosing the most appropriate policy.However, the existing works lack a uniform approach to support analyzing the various alternatives of the configured policy.To solve this problem, this paper presents a general-purpose timing analysis approach for the ASOS-based RTES.In the analysis, a timing analysis tree is proposed to characterize the tasks and the ASOS in the RTES.Then, each of the alternative policies in the ASOS is refined by the uniform execution rules in the tree.Finally, the task's response time under the various alternative policies is analyzed by a traversal of the timing analysis tree using a uniform way.In the case study, we take the scheduling policy as an example to show the use of our approach on a real-life robot controller system.

The timing requirements of real-time systems can be guaranteed by well-designed scheduling policies. The analysis of such scheduling uses an abstract task model of the system to diagnose the practicability of timing requirements. The task models have evolved from periodic models to more sophisticated graph-based ones, among which digraph real-time (DRT) task model is the most applicable because of its good expressiveness and analysis efficiency. However, the DRT model cannot support the commonly used precedence constraints within or between tasks. In this paper, we propose a new task model that extends the DRT model to support precedence constraints. Based on our model, we present two methods of uniprocessor schedulability analysis for static priority scheduling policy and earliest deadline first (EDF) scheduling policy. We also introduce an optimization technique to improve the efficiency of model analysis. Our experiments show that, despite a high computational complexity of the problem, our approach scales very well for large sets of tasks with precedence constraints.

Abstract Event‐B is a formal notation and method for the systems development. The key feature of this method is to produce correct‐by‐construction system designs. Once the correct design is established, the remaining work is to generate or implement correct code from the design. Two main problems remain in the process from the correct‐by‐construction design to the correct software. First, the Event‐B design is “quasi‐correct” due to some technical limitations. For instance, it is still difficult to prove the liveness properties by the Rodin platform; it is not possible to construct the Event‐B design with floating‐point arithmetic, and sometimes, the Event‐B model is incomplete and must rely on the third‐party libraries. Therefore, a method is needed to complement these modeling and proof gaps. Secondly, proving the correctness of an automatic code generator is very difficult; therefore, a method is needed to guarantee the correctness of the produced code without proving the code generator. In this article, we address the above 2 problems by introducing an intermediate formal language called High‐Level Language (HLL) between the Event‐B models and the C code. The Event‐B model is translated to HLL with an additional schedule configuration, where Event‐B invariants and system invariants (here, deadlock‐freeness and liveness properties) are proved using a SAT‐based model checker called S3. This proof guarantees the correctness of the HLL model with respect to the Event‐B model. The C code is then automatically generated from the HLL model for most functions and is manually implemented for the third‐party ones according to the function contracts defined in Event‐B. The correctness of the generated C code is guaranteed using the equivalence proof, and the correctness of the implemented C code is guaranteed using the conformance proof. Through the article, we use a traffic light controller to illustrate the proposed method; then, we apply the method to an automatic protection function of a 3‐wheeled robot to evaluate its feasibility.

This paper presents a formal development process for safety-critical embedded Human-Machine Interface (HMI) systems. This formal approach is centered on the LIDL formal language and the S3 verification toolset. It is aimed at blurring the boundaries between modeling, design, verification and implementation for the development of HMI. From textual requirements to software, the development process integrates the following formal activities: modeling the behavioral aspect of user interfaces (UIs) using LIDL; translating LIDL to Lustre, with which we combine the functional library in Lustre; translating the Lustre design models into the HLL verification models; verifying formal properties expressed in HLL against the HLL model using the S3 toolset, and diagnosing design errors with the help of counterexample scenarios and debug tools. This formal development process is illustrated on a simple use case — part of the display component of an alert management system used in a three-wheeled robot.

To ease the expression of real-time requirements, Dwyer, and then Konrad, studied a large collection of existing systems in order to identify a set of real-time property patterns covering most of the useful use cases. The goal was to provide a set of reusable patterns that system designers can instantiate to express requirements instead of using complex temporal logic formulas. A limitation of this approach is that the choice of patterns is more oriented towards expressiveness than efficiency; meaning that it does not take into account the computational complexity of checking patterns. For this purpose, we define a set of verification-dedicated, atomic property patterns for qualitative and quantitative real-time requirements. End-user requirements can then be expressed as a composition of these patterns using a predefined meta-model and a mapping library. These properties can be checked efficiently using a set of elementary observers and a model checking approach.