Simulink has emerged as the fundamental infrastructure that supports modeling, simulation, verification, and code generation for embedded software development. To improve the performance of the code generated from Simulink models, state-of-the-art code generators employ various optimization techniques, such as expression folding, variable reuse, and parallelism. However, they overlook the presence of redundant calculations within data-intensive models widely used to perform substantial data processing in embedded scenarios, which can significantly degrade the performance and introduce additional memory usage. This paper proposes MFRODO, an efficient and memory-sensitive code generator for data-intensive Simulink models through redundancy elimination. MFRODO begins by conducting model analysis to construct the dataflow graph and derive the I/O mapping of each block. Then, for each block within the dataflow graph, MFRODO recursively determines its calculation range by leveraging the I/O mapping of its subsequent blocks and marks optimization blocks whose calculation range is eliminated. For optimizable blocks, MFRODO eliminates the redundant calculations and reduces the memory space associated with these calculations. Finally, MFRODO rebuilds the I/O mappings of these optimizable blocks to ensure code correctness and synthesizes the embedded code for deployment. We implemented and evaluated MFRODO on benchmark Simulink models, in terms of execution duration, memory usage, and code generation overhead across different compilers and architectures. The results show that, compared with the Simulink Embedded Coder, DFSynth, and HCG, MFRODO achieves performance improvements ranging from 1.17× - 8.55×, while reducing BSS segment usage by 12.00% - 52.71%. Besides, MFRODO reduces compile time by 91.8% - 98.7% and code synthesis time by 94.3% - 99.6% compared with Simulink Embedded Coder, while incurring comparable overhead to DFSynth and HCG.

Simulink has become a pivotal infrastructure in embedded scenarios, including automotive systems and aerospace designs. To improve the performance of the code generated from Simulink models, state-of-the-art code generators employ various optimization techniques, such as expression folding, variable reuse, and parallelism. However, they struggle to generate efficient code for loop-semantic models which are crucial in substantial data processing tasks. This inefficiency manifests in numerous redundant calculations, such as array calculations and conditional statements. As a result, the performance of the generated code is limited. This article proposes Knight, an efficient code generator for loop-semantic Simulink models with loop reshaping. Knight first parses the Simulink model to extract essential content, such as block functionalities and connections. Knight then identifies blocks with internal states and implements the specific interaction rules to discern those that are state-dependent. For state-dependent blocks, Knight conducts forward inference to obtain their preceding blocks, which influence the internal state calculations. Subsequently, Knight isolates blocks that are optimizable and irrelevant to the internal states. These blocks are strategically relocated outside the loop semantics while preserving critical semantics related to code generation. We implemented and evaluated Knight on benchmark Simulink models across different compilers and architectures. Compared with the state-of-the-art code generators Simulink Embedded Coder, DFSynth, and HCG, the code generated by Knight is$16.58 \times $faster,$16.89 \times $faster, and$15.38 \times $faster in terms of execution duration on average, without incurring additional overhead of memory usage.

Fuzzing, as an effective method for software system defect testing and bug mining, utilizes random data generated by mutation to execute programs to trigger potential bugs in the tested program. However, due to the strict syntax and semantic checks in DBMSs, existing mutation-based testing methods are difficult to generate test cases with correct syntax and semantics. To ensure the syntax and semantic correctness of the test case generated by mutation, this paper proposes the concepts of weak semantic correlation nodes and semantic relationship tables. At the same time, a set of mutation operators for weak semantic correlation nodes in the syntax tree is designed, and each time the “optimal” mutation operator is selected to replace, delete, and insert the target node subtree in the test case syntax tree. In response to semantic errors during the mutation, this paper checks and corrects them through a pre-extracted semantic relationship table, further ensuring the correctness of the semantics of the test cases generated by the mutation. This paper utilizes this semantic effective fuzzing method for DBMSs to implement a new fuzzing framework for DBMSs, SQLPass. We evaluated SQLPass on four popular DBMSs: SQLite3, MySQL, MariaDB and PostgreSQL. In our experiment, SQLPass achieves 5.7%-94.2% higher semantic correctness than state-of-the-art tools, and explores 1.3%-52% more code coverage than other tools. Notably, it discovered four unknown bugs on SQLite3 and MariaDB and has submitted them to the vendor for confirmation.

Simulink is extensively utilized in system design for its ability to facilitate modeling and synthesis of embedded controllers. It provides automatic test case generation to assist testers in inspecting the model. However, with the continuous increase in the model's scale, the control logic and internal states of the model are becoming more and more complex. Mainstream test case generation methods based on constraint solving and model simulation face challenges in achieving high coverage metrics.

Simulink has emerged as the fundamental infrastructure that supports modeling, simulation, verification, and code generation for embedded software development. To improve the performance of the code generated from Simulink models, state-of-the-art code generators employ various optimization techniques, such as expression folding, variable reuse, and parallelism. However, they overlook the presence of redundant calculations within data-intensive models widely used to perform substantial data processing in embedded scenarios, which can significantly undermine the efficiency and performance of the generated code.

Simulink has gained widespread recognition as a valuable tool for system design. As systems grow increasingly complex, particularly in terms of their internal states, this complexity poses new challenges for existing model testing methodologies. Traditional techniques such as constraint solving and random search encounter difficulties when attempting to explore the intricate logic embedded within these models. In this paper, we introduceHSTCG, a state-aware test case generation method for Simulink models with heuristic strategy.HSTCGsolves only one iteration of the model each time to get the test input that can cover a target branch, then executes the model once to obtain and update the new model state based on the solved input dynamically. Then, it solves the remaining branches based on the new model state iteratively until all the coverage requirements are satisfied. To improve the efficiency of test case generation, we also designed a heuristic strategy containing heuristic branch searching, repeated state filter and unreached branch filter to minimize the times of constraint solving. We implementedHSTCGand evaluated it on several benchmark Simulink models. Compared to the built-in Simulink Design Verifier and state-of-the-art academic work SimCoTest,HSTCGachieves an average improvement of 55% and 103% on Decision Coverage, 53% and 62% on Condition Coverage and 192% and 201% on Modified Condition Decision Coverage, respectively. We also validated the significant improvement of the heuristic strategy, which can improve the efficiency of test case generation by 62.2% on average.

Simulink has been widely used in system design, which supports the efficient modeling and synthesis of embedded controllers, with automatic test case generation to simulate and validate the correctness of the constructed Simulink model. However, the increasing complexity of the model, especially the internal states, brings extra challenges to existing model testing techniques such as constraint solving and random search, which results in difficulties when trying to reach the deeper logic of the model effectively.In this paper, we propose STCG, a state-aware test case generation method for Simulink models. STCG solves only one iteration of the model each time to get the test input that can cover a target branch, then executes the model once to obtain and update the novel model state based on the solved input dynamically. Then, it solves the remaining branches based on the new model state iteratively until all the coverage requirements are satisfied. We implemented STCG and evaluated it on several benchmark Simulink models. Compared to the built-in Simulink Design Verifier and state-of-the-art academic work SimCoTest, STCG achieves an average improvement of 58% and 132% on Decision Coverage, 52% and 70% on Condition Coverage and 239% and 237% on Modified Condition Decision Coverage, respectively.

Simulink is widely used for the model-driven design of embedded systems. It is able to generate optimized embedded control software code through expression folding, variable reuse, etc. However, for some commonly used computing-sensitive models, such as the models for signal processing applications, the efficiency of the generated code is still limited. In this article, we propose PHCG, an optimized code generator for the Simulink model with single-instruction–multiple-data (SIMD) instruction synthesis. It will select the optimal implementations for intensive computing actors based on adaptively precalculation of the input scales, and synthesize the appropriate SIMD instructions for batch computing actors based on the iterative dataflow graph mapping. In addition, actors of the same type that can be executed in parallel can be combined into batch computing actors as much as possible by merging isomorphic subgraphs. We implemented and evaluated its performance on benchmark Simulink models. Compared to the built-in Simulink Coder and the most recent DFSynth, the code generated by PHCG achieves an improvement of 38.9%–92.9% and 41.2%–76.8% in terms of execution time across different architectures and compilers, respectively.

Action Recognition is a fundamental task in computer vision field, with a wide range of applications in autonomous driving, security monitoring, etc. However, previous action recognition approaches usually suffer from the inappropriate spatio-temporal modeling or high computational consumption (e.g., 3D CNN). In this paper, we propose a novel Spatio-Temporal Adaptive Network (STANet) with bidirectional temporal difference, consisting of a Temporal Adaptive module (TA) and a Spatial Adaptive (SA) module, to sufficiently extract the crucial motion information and model the spatial pivotal appearance information from both forward and backward perspectives, respectively. Specifically, the Temporal Adaptive module uses bidirectional temporal differences to learn valuable motion trends and balance the static semantics and dynamic motion for a certain action during information fusion; while the Spatial Adaptive module uses the bidirectional temporal difference to obtain the spatio-channel attention to stress the discriminative position-relevant and semantic-relevant appearance features. Extensive experiments conducted on widely-used action recognition benchmarks UCF-101, HMDB-51, Something-Something V1, and Kinetics-400 prove the effectiveness of the proposed methods compared to other state-of-the-art approaches.

Intelligent robots are a current application in Industrial Internet of Things (IIoT), with their trustworthiness being a topic of considerable research interest. Vulnerabilities in robot software may affect the trustworthiness of robotics. To detect these vulnerabilities in robot software, this study proposes a differential fuzz testing method. The main idea is to continuously execute test cases for different versions of software packages to detect inconsistencies among outputs and eventually discover vulnerabilities. First, test cases are generated, combining seed generation and mutation, after which the measured model of the packages in the robot visualization tool (RVIZ) is built and the generated seeds are executed. The differences among inconsistent outputs are calculated and the causes of the differences analyzed. Two evaluation metrics for the inconsistencies and seeds are presented. This method is applied to the crucial package in ROS-MoveIt!. The results show that thearm.go()ofmoveit_commanderhas joint angle overflow.

Simulink is widely used for the model-driven design of embedded systems. It is able to generate optimized embedded control software code through expression folding, variable reuse, etc. However, for some commonly used computing-sensitive models, such as the models for signal processing applications, the efficiency of the generated code is still limited.

Simulink is a widely used model-driven design environment for supporting the simulation and code generation of embedded applications. To improve the quality of the code generated from Simulink models, state-of-the-art code generators employ various high-level optimizations, like eliminating local variables. However, they overlook the compatibility between code and the low-level processor architecture, especially the instruction pipeline. Consequently, instruction pipeline stalls occur frequently, leading to additional delays in instruction execution, as well as limited efficiency for deployed the embedded software. In this article, we propose Mercury, an instruction pipeline aware code generator for Simulink models which utilizes data dependencies between actors to decrease the instruction pipeline stalls of the generated code. First, Mercury collects data dependencies through model dataflow traversal and records the property of each actor. Then, Mercury approximately estimates the execution latency of required instructions fetched from corresponding actors and uses a topology-based method to obtain candidate actors for code synthesis. Finally, Mercury adopts the least penalty priority to iteratively select the most suitable actor for code synthesis and releases data dependencies with its subsequent actors. We implemented and evaluated Mercury on benchmark Simulink models (Su et al., 2021) as well as a real industrial model. Compared to the official tool Simulink Embedded Coder and the state-of-the-art academic tool DFSynth, Mercury outperformed them by 9.7%–33.4% and 9.2%–59.4% in terms of the execution time of the generated code across different architectures, respectively. The statistics also demonstrate that the generated code of Mercury increases utilization of pipeline slots by 11.0%–37.1% and 10.6%–50.0%, respectively.

The robot has attracted much attention to anticipate improved quality of human life. Real-time obstacle avoidance is one of hot spots of the research. Runtime verification is a real-time and lightweight verification technology to verify the properties in many fields. In this case study, we use the JavaMOP, a runtime verification tool to verify the implementations' correctness of the safety strategies for avoiding collision as a complement to the design. The design of the safety strategies can be classified as the pre-contact safety strategy and the post-contact safety strategy. The former can avoid obstacles and the latter can reduce the physical damage after a collision. Additionally, this case study also proposes a new method of dynamic parameter selection. It can automatically update the parameters during the operation of the robot without having to get familiar with and to modify robot programs. Because some special parameters may change as mutative factors or be updated by engineers' experience in the uncertain environment, they cannot be fixed. We follow the JavaMOP specification to describe informal requirements using the FSM and ptLTL languages. Finally, the experimental results verify the correctness of the safety strategies and the effectiveness of dynamic parameter selection.

Robot Operating System(ROS) is widely used in the development of various service robots, which have high requirements in safety and reliability. Data distribution service(DDS) is deployed in ROS2 to implement the control of nodes and data distribution, which is very important for the operation of application on ROS2. In this paper, we focus on model abstraction, formal modeling and automatic verification for DDS in ROS2. A distributed model with interface parameters was established in PRISM. Properties such as security, liveness and priority of DDS in ROS2 were verified. The results show that the design satisfies these properties and high-priority messages can be sent and transmitted preferentially by the system. Due to the experiment result, we come up with a suggestion that the system will be better if its buffer can store six messages or more.

Robot systems have been widely used in industry and also play an important role in human social life. Safety critical applications usually demand rigorously formal verification to ensure correctness. But for the increasing complexity of dynamic environments and applications, it is not easy to build a comprehensive model for the traditional offline verification. In this paper, we propose RobotRV, the first data-centered real-time verification approach for the robot system. Within this approach, a domain-specific language named RoboticSpec is designed to specify the complex application scenario of the robot system, the data packets transmitted in the robot system, and the safety critical temporal properties. Then, we develop an engine to automatically translate the RoboticSpec model into a real-time verifier. The generated verifier serves as an independent plug-in component for the runtime verification of concerned temporal properties. We applied the proposed approach to a real robot system. As presented in experiment results, our method detected potential failures, and improved the safety of robot system.

In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.

Robot control systems are complex cyber-physical systems which are difficult to develop. In this paper, we present a formal model-based automatic code synthesis method which can generate executable C++ code running on the world-wide used Robot Operating System (ROS). The internal interaction behaviors of robot systems are modeled as a network of timed automata. The safety requirements and specifications related to the model are formalized as CTL formulas and verified by Uppaal. We design a code synthesis method to generate the executable C++ code from the verified model. Compared to existing code generators based on timed automata, our method supports more complex structures and advanced features such as timer and committed location, and provides the important abstraction and mapping of ROS instructions, which realize the seamless connection between the generated code and ROS. A case study of grasping a cup by a robot with seven degrees of freedom manipulator is conducted and the generated codes are successfully applied to a ROS development environment.

Wireless medical cyber-physical systems are widely adopted in the daily practices of medicine, where huge amounts of data are sampled by the wireless medical devices and sensors, and is passed to the decision support systems (DSSs). Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care based on those collected data. But for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties encoded in those data, which brings new challenges to current simulation-based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios and have applied the proposed technique to assist existing wireless medical cyber-physical system. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital.

Automatic hardware/software partitioning relies on characterization, estimation and design space exploration of the system performance and cost metrics. In real world situations, such estimates are complicated and cannot be 100 percent accurate. Furthermore, hardware/software co-design is so complicated nowadays that simply considering the bipartitioning between hardware and software is not sufficient. It is important to consider some of the other key design parameters and resource sharing together with the hardware/software partitioning problem. Under variable requirements of smart systems, more flexibility on the resource usage should be incorporated in system modelling. This paper considers uncertainty modeling for system partitioning with an enhanced set of parameters for hardware/software resource sharing. We harness state-of-the-art uncertainty theory for linear uncertain distribution and normal uncertain distribution. Our derivations convert the uncertainty model back to a regular constraint optimization problem. Experimental results show the effectiveness of our approach.

Embedded systems are becoming increasingly popular due to their widespread applications. Hardware/software partitioning with reliability in consideration is becoming one of the most crucial steps in the design of complex embedded systems, especially for safety critical applications. In this paper, a reliability-centric approach is proposed to increase the reliability and decrease the potential errors of the embedded system during the partition stage. We use task graph to model the system function blocks, and treat reliability as the first-class metric during the mathematical formalization and optimization procedure. Experimental evaluations demonstrate that the proposed approach obtains a better solution with the trade off of time, cost and reliability compared to existing partitioning methods, with higher and more accurate reliability characterization for safety-critical systems.

Motion planning is an important problem with many applications in robotics. In this paper, we focus on motion planning with rectangular obstacles parallel to the X, Y or Z axis. We formulate motion planning using Satisfiability Modulo Theories (SMT) and use SMT solvers to find a feasible path from the source to the goal. Our formulation decompose the robotic path into N path segments where the two ends of each path segment can be constrained using difference logic. Our SMT approach will find a solution if and only if a feasible path exists for the given constraints. We present extensive experimental results to demonstrate the scalability of our approach.

In designing robot control systems, simulation is still the primary approach to verifying the functions of circuit descriptions written in hardware design language. The validity of the verification depends on the coverage metric. But not all state spaces can be specified in a simulation. Model checking can overcome the shortcomings of simulation, because all of the state spaces can be traversed. Robot control system is an important part of the robot, used in the control of the manipulator to perform specific tasks. Therefore, in this paper a verification framework is presented for design correctness of robotic manipulator, which combines simulation and model checking. The framework is also applied to other control system or control hardware. Model checking guides the generating of test vectors, and makes the functional coverage reach 100% quickly. In this paper, a manipulator designed with six degrees of freedom is verified. The results of the verification of the manipulator show that the verification framework is effective for checking the design correctness of robotic manipulator.

Sambot is a module robot system, with the advantages of self-assembly. A target robotic configuration can be organized by a group of Sambots. A novel motion planning method for Sambot configuration using model checking is presented in this paper. This hierarchical method contains two layers. The abstract logic layer is responsible for the discrete planning of Sambots configuration. The robot and the environment are all modeled as timed automata. System requirements are formalized as Computational Tree Logic (CTL) formulas. Model checking is applied on the system model. The verification result gives the optimal discrete plans for the configuration of Sambot. In physical layer, a sample-based planner generates the trajectory trace considering the dynamics of Sambot and the suggested high level plans. The experiment results illustrate the effectiveness of our approach.

Programable logic controllers (PLCs) are complex embedded systems which are widely used in industry. The formal modeling of PLC system for verification is a rough task. Good verification model should be faithful with the system, and also should have suitable scale because of the state explosion problem of verification. This paper proposes an automatic framework for the construction of verification model of PLC systems. BIP (Behavior, Interaction, Priority) separates behavioral and architectural aspects in modelling. Specifical PLC features and system architecture are modelled by BIP framework. They are universal for all PLC applications. We define the operational semantics of PLC instruction and present an automatic translation based modeling method for PLC software. A small example is demonstrated for our approach.

Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper shows the modeling and validation work of a typical PLC control system using the Behavior-Interaction-Priority(BIP) component framework. The gate control system based on PLC is a real industry application. We design general system architecture for this kind of device control system. The control software and hardware of environment are all modeled as BIP components. Their interactions are described by BIP connectors. System requirements are formalized as monitors. Simulation is applied on the system model. We found a couple of design errors in simulation, which help us to improve the dependability of the original systems.

Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper presents a robust approach to design and implement PLC-based embedded systems. Timed automata are used to model the controller and its environment. We validate the design model with resort to model checking techniques. We propose an algorithm to generate PLC code from timed automata and implement this algorithm with a prototype tool. This method can condense the developing process and guarantee the correctness of PLC programs. A case study demonstrates the effectiveness of our method.