8 citations · 8 across the 6 of their papers we have counts for
6 papers
Bit-Precise Conformance Testing of Simulink Model Checkers
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki +1
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 a…
Modeling Language for Scenario Development of Autonomous Driving Systems
Toshiaki Aoki, Takashi Tomita, Tatsuji Kawai +2
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…
SMT-Based Model Checking of Industrial Simulink Models
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki +3
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 a…
Compositional Test Generation of Industrial Synchronous Systems
Daisuke Ishii, Takashi Tomita, Kenji Onishi +1
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 i…
Approximate Translation from Floating-Point to Real-Interval Arithmetic
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties ca…
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki
Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and contin…