For embedded systems, verifying both real-time properties and logical validity are important. The embedded system is not only required to the accurate operation but also required to strictly real-time properties. To verify real-time properties is a key problem in model checking. In order to verify real-time properties of assembly program, we develop the simulator to propose the model checking method for verifying assembly programs. Simultaneously, we propose a timed Kripke structure and implement the simulator of the robot's processor to be verified. We propose the timed Kripke structure including the execution time which extends Kripke structure. For the input assembly program, the simulator generates timed Kripke structure by dynamic program analysis. Also, we implement model checker after generating timed Kripke structure in order to verify whether timed Kripke structure satisfies RTCTL formulas. Finally, to evaluate a proposed method, we conduct experiments with the implementation of the verification system. To solve the real problem, we have experimented with real microcontroller software.

Embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.). Therefore, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our study aims at enabling a formal verification with Satisfiability Modulo Theories-Based Bounded Model Checking (SMT-Based BMC) of safety for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts, and the size of the models is reduced using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method of safety properties of embedded assembly program by combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions. Moreover, we show the evaluation of our method by experiments using prototype model checker.

In recent years, reinforcement learning (RL) has received a lot of attention because we can automatically learn optimal behavioral policies. However, since RL acquires the policy by repeatedly interacting with the environment, it is difficult to learn about realistic tasks. In recent years, there has been a lot of research on offline RL (batch RL), which does not need to interact with the environment, but learns from the accumulated experience prepared in advance. Learning does not work by applying common RL methods directly to offline RL because of a problem called distributional shift. Methods to suppress distributional shift have been actively studied in offline RL. In this study, we propose a new offline RL algorithm that adds constraints from discriminators used in Generative Adversarial Networks to the offline RL method called TD3+BC. We compare and validate the proposed method with existing methods using a benchmark for 3D robot control simulation. In TD3+BC, the constraint was tightened to suppress distribution shift, but a challenge arose when the quality of the dataset was poor, leading to difficulties in successful learning. The proposed approach addresses this issue by incorporating features to mitigate distribution shift while introducing new constraints to enable learning that is not solely dependent on the dataset’s quality. This innovative strategy aims to improve accuracy even in cases where the dataset exhibits poor characteristics.

It is important to verify both the correctness and real-time properties of embedded systems. However, as practical computer programs are represented by infinite state transition systems, specifying and verifying a computer program is difficult. Real-time properties are also important for embedded programs, but verifying the real-time properties of an embedded program is difficult. In this paper, we focus on verifying an embedded assembly program, in order to verify the real-time safety properties. We propose a deductive verification method to verify real-time safety properties, based on discrete time, as follows: (1) First, we construct a timed computational model including the execution time from the assembly program. We can specify an infinite state transition system including the execution time of the timed computational model. (2) Next, we verify whether a timed computational model satisfies RTLTL (Real-Time Linear Temporal Logic) formulas by deductive verification. We can specify real-time properties by RTLTL. By our proposed methods, we are able to achieve verification of the real-time safety properties of an embedded program.