arXiv subjects

Takashi Tomita

Publications and source records attributed to Takashi Tomita.

6 recordsLinked to original sources

arXiv2026

Bit-Precise Conformance Testing of Simulink Model Checkers

MATLAB/Simulink provides a practical modeling language and a simulation engine for the development of cyber-physical systems. To ensure the quality of the developed models, there are formal verification tools available, such as Simulink Design Verifier (SLDV) and third-party SMT-based model checkers (SmtMC). However, due to the absence of a semantics of Simulink that covers every element of models and the details of its numerical behavior, the reliability of the model checkers themselves is often doubtful, potentially analyzing models differently from the simulator. This work aims to verify the quality of the Simulink model checkers by addressing the following items. 1) Formalization of the basic block types of Simulink. It involves defining block type feature sets and the bit-precise behavior of the blocks. 2) A method for testing bit-precise conformance relations among the tools for each block type. The pass rate of our test suite measures (i) conformance of model checking results with simulation results by Simulink and (ii) conformance between the results of SmtMC and SLDV. 3) Experiment to perform tests on 10 block types. We confirmed that SmtMC efficiently passed all test cases, while SLDV achieved pass rates of only 94-96% and 80-90% for conformance (i) and (ii), respectively. We analyzed the causes of failed tests, such as errors, corner cases, and timeouts.

cs.SE↗

arXiv2025

Modeling Language for Scenario Development of Autonomous Driving Systems

Autonomous driving systems are typically verified based on scenarios. To represent the positions and movements of cars in these scenarios, diagrams that utilize icons are typically employed. However, the interpretation of such diagrams is typically ambiguous, which can lead to misunderstandings among users, making them unsuitable for the development of high-reliability systems. To address this issue, this study introduces a notation called the car position diagram (CPD). The CPD allows for the concise representation of numerous scenarios and is particularly suitable for scenario analysis and design. In addition, we propose a method for converting CPD-based models into propositional logic formulas and enumerating all scenarios using a SAT solver. A tool for scenario enumeration is implemented, and experiments are conducted on both typical car behaviors and international standards. The results demonstrate that the CPD enables the concise description of numerous scenarios, thereby confirming the effectiveness of our scenario analysis method.

cs.SE↗

arXiv2022

SMT-Based Model Checking of Industrial Simulink Models

The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numerically accurate analysis of models, and (3) demonstrating the analysis of Simulink models using an SMT solver (we use Z3). It first encodes a target model into a predicate logic formula in the domain of mathematical arithmetic and bit vectors. We explore how to encode various Simulink blocks exactly. Then, the method verifies a given invariance property using the k-induction-based algorithm that extracts a subsystem involving the target block and unrolls the execution paths incrementally. In the experiment, we applied the proposed method and other tools to a set of models and properties. Our method successfully verified most of the properties including those unverified with other tools.

cs.LO↗

arXiv2021

Compositional Test Generation of Industrial Synchronous Systems

Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexity issue. We regard a test case as a counterexample in safety verification, and represent a test generation process as a deductive proof tree built with dedicated inference rules; we conduct both spatial- and temporal-compositional reasoning along with a modular system structure. A proof tree is generated using our semi-automated scheme involving manual effort on contract generation and automatic processes for counterexample search with SMT solvers. As case studies, the proposed method is applied to four industrial examples involving such features as enabled/triggered subsystems, multiple execution rates, filter components, and nested counters. In the experiments, we successfully generated test cases for target systems that were difficult to deal with using the existing tools.

cs.SE↗

arXiv2021

Approximate Translation from Floating-Point to Real-Interval Arithmetic

Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes advantage of the efficiency of RA solving. The proposed method abstracts FP numbers as rational intervals and FPA expressions as interval arithmetic (IA) expressions; then, we solve IA formulas to check the satisfiability of an FPA formula using an off-the-shelf RA solver (we use CVC4 and Z3). In exchange for the efficiency gained by abstraction, the solving process becomes quasi-complete; we allow to output unknown when the satisfiability is affected by possible numerical errors. Furthermore, our IA is meticulously formalized to handle the special value NaN. We implemented the proposed method and compared it to four existing SMT solvers in the experiments. As a result, we confirmed that our solver was efficient for instances where rounding modes were parameterized.

cs.LO↗

arXiv2011

A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking

Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively. In PCTL and CSL, the possibility of executions satisfying some temporal properties can be quantitatively represented by the probabilistic extension of the path quantifiers in their basic Computation Tree Logic (CTL), however, path formulae of them are expressed via the same operators in CTL. For this reason, both of them cannot represent formulae with quantitative temporal properties, such as those of the form "some properties hold to more than 80% of time points (in a certain bounded interval) on the path." In this paper, we introduce a new temporal operator which expressed the notion of frequency of events, and define probabilistic frequency temporal logic (PFTL) based on CTL\star. As a result, we can easily represent the temporal properties of behavior in probabilistic systems. However, it is difficult to develop a model checker for the full PFTL, due to rich expressiveness. Accordingly, we develop a model-checking algorithm for the CTL-like fragment of PFTL against finite-state Markov chains, and an approximate model-checking algorithm for the bounded Linear Temporal Logic (LTL) -like fragment of PFTL against countable-state Markov chains.

cs.LO↗