The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Pour les systèmes embarqués, la vérification des propriétés en temps réel et de la validité logique est importante. Le système embarqué est non seulement nécessaire au fonctionnement précis, mais également aux propriétés strictement en temps réel. La vérification des propriétés en temps réel est un problème clé dans la vérification de modèles. Afin de vérifier les propriétés en temps réel du programme d'assemblage, nous développons le simulateur pour proposer la méthode de vérification de modèle pour vérifier les programmes d'assemblage. Simultanément, nous proposons une structure de Kripke temporisée et implémentons le simulateur du processeur du robot à vérifier. Nous proposons la structure de Kripke chronométrée incluant le temps d'exécution qui étend la structure de Kripke. Pour le programme d'assemblage d'entrée, le simulateur génère une structure de Kripke chronométrée par analyse de programme dynamique. De plus, nous implémentons un vérificateur de modèle après avoir généré une structure Kripke temporisée afin de vérifier si la structure Kripke temporisée satisfait aux formules RTCTL. Enfin, pour évaluer une méthode proposée, nous menons des expériences avec la mise en œuvre du système de vérification. Pour résoudre le vrai problème, nous avons expérimenté un vrai logiciel de microcontrôleur.
Yajun WU
Kanazawa University
Satoshi YAMANE
Kanazawa University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Yajun WU, Satoshi YAMANE, "Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software" in IEICE TRANSACTIONS on Information,
vol. E103-D, no. 4, pp. 800-812, April 2020, doi: 10.1587/transinf.2019EDP7172.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2019EDP7172/_p
Copier
@ARTICLE{e103-d_4_800,
author={Yajun WU, Satoshi YAMANE, },
journal={IEICE TRANSACTIONS on Information},
title={Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software},
year={2020},
volume={E103-D},
number={4},
pages={800-812},
abstract={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.},
keywords={},
doi={10.1587/transinf.2019EDP7172},
ISSN={1745-1361},
month={April},}
Copier
TY - JOUR
TI - Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software
T2 - IEICE TRANSACTIONS on Information
SP - 800
EP - 812
AU - Yajun WU
AU - Satoshi YAMANE
PY - 2020
DO - 10.1587/transinf.2019EDP7172
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E103-D
IS - 4
JA - IEICE TRANSACTIONS on Information
Y1 - April 2020
AB - 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.
ER -