Search Results 1-20 of 145

  • A symbolic Zone-based reachability analysis for dense-timed pushdown automata with freezing clocks  [in Japanese]

    結縁 祥治 , 平岡 祥

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 117(477), 7-12, 2018-03-06

  • Model Checking Application to the Railway Crossing Problem for STAMP/STPA using Timed Automaton  [in Japanese]

    岡野 浩三 , 小形 真平 , 楊 盼 , 岡本 圭史

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 117(477), 1-6, 2018-03-06

  • Dense-timed Pushdown Automata with Multiple Local Clocks  [in Japanese]

    上里 友弥

    … 本論文では,Abdullaらによって導入されたDense-timed pushdown automata(TPDA)を拡張し,複数の局所クロックを持つTPDAを考え,この拡張が言語クラスを拡大しないことを示す.TPDAは,時間オートマトンとプッシュダウン・オートマトンの両方の性質を持つ計算モデルであり,従来のプッシュダウン・オートマトンにおけるスタックとは異なり,時間付きスタック(クロック付きスタック)を考える.時間付 …

    情報処理学会論文誌プログラミング(PRO) 11(1), 10-28, 2018-02-08

    IPSJ

  • Configuration Reachability Analysis of Synchronized Recursive Timed Automata  [in Japanese]

    UEZATO Yuya , MINAMIDE Yasuhiko

    … We present synchronized recursive timed automata (SRTA) that extend timed automata with a stack in which each frame contains multiple real valued clocks. … SRTA are an extension of dense-timed pushdown automata (TPDA) of Abdulla et al. … As with TPDA, timed transitions of an SRTA synchronously increase the values of all the clocks within its stack at the same rate. …

    Computer Software 35(1), 1_140-1_168, 2018

    J-STAGE

  • Dense-timed Pushdown Automata with Multiple Local Clocks  [in Japanese]

    上里 友弥

    … 本発表では,Abdullaらによって導入されたDense-timed pushdown automata(TPDA)を拡張し,複数の局所クロックを持つTPDAを考え,この拡張が言語クラスを拡大しないことを示す.TPDAは,時間オートマトンとプッシュダウン・オートマトンの両方の性質を持つ計算モデルであり,従来のプッシュダウン・オートマトンにおけるスタックとは異なり,クロック付きスタックを考える.クロック付きスタックでは, …

    情報処理学会論文誌プログラミング(PRO) 10(5), 3-3, 2017-11-14

    IPSJ

  • A Symbolic Simulation of Dense-Timed Pushdown Automata with Clock Freezing  [in Japanese]

    平岡 祥 , 結縁 祥治

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(512), 1-6, 2017-03-09

  • Cutting a Parameter Space for a Multi-Legged Robot Based on Model Checking

    NOMURA Keisuke , INAGAKI Shinkichi

    … The robot behavior is modelled by timed-automata, and specifications for the robot to successfully walk are described in a computational tree logic (CTL). …

    SICE Journal of Control, Measurement, and System Integration 10(4), 317-323, 2017

    J-STAGE

  • Towards a Zone-based Verification for DTPDA with Clock Freezing  [in Japanese]

    平岡 祥 , 結縁 祥治

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(278), 43-48, 2016-10-27

  • Towards a Zone-based Verification for DTPDA with Clock Freezing  [in Japanese]

    平岡 祥 , 結縁 祥治

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(277), 43-48, 2016-10-27

  • The Representation and Verification of Business Process Using UML  [in Japanese]

    Kajimura Kengo , Shinkawa Yoshiyuki

    スピードが要求される近年のビジネスプロセス(BP)では、時間制約が重要な要因となる。BPの表記法には様々なものがあるが、情報システムとの適合性を考慮すると、UMLも有力な選択肢となる。UMLには13種類の図(ダイアグラム)があり、このうち時間制約の記述が可能なものはシーケンス図とタイミング図となる。前者がシステムの大域的動作のモデル化に向いているのに対し、後者は局所的動作に適していると考えられる。 …

    Abstracts of Annual Conference of Japan Society for Management Information 2016f(0), 147-150, 2016

    J-STAGE

  • New Extension of Updatable Timed Automata  [in Japanese]

    上里 友弥 , 南出 靖彦

    日本ソフトウェア科学会大会論文集 32, 13p, 2015-09-09

  • An Implementation of Computing Optimal Mean-payoff Values for Non-terminating Scheduling by Double Priced Timed Automata  [in Japanese]

    平岡 祥 , 結縁 祥治

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 115(20), 11-16, 2015-05-11

  • Scheduling analysis based on behavior of timed automata  [in Japanese]

    結縁 祥治

    ウィンターワークショップ2015・イン・宜野湾 論文集 2015, 81-82, 2015-01-15

    IPSJ

  • Code Synthesis for LEGO Mindstorms EV3 Using UPPAAL  [in Japanese]

    ARAKAWA Mitsuru , YUEN Shoji

    本研究は,UPPAALを用いて記述した時間オートマトンによる振舞い仕様からLEGO Mindstorm EV3システムを制御するC言語プログラムを合成する手法を提案する.UPPAALは複数の時間オートマトンがネットワークで同期しながら計算が進行する振舞いを記述し,制限されたCTLによって記述された性質に対するモデル検査を行うツールである.LEGO Mindstorm EV3の振舞いをモジュール毎に …

    Technical report of IEICE. SS 114(271), 41-46, 2014-10-23

  • Validation of UML Timing Diagrams Using Timed Automata  [in Japanese]

    KAJIMURA Kengo , SHINKAWA Yoshiyuki

    従来,UMLは業務系システムのモデリングに適したモデル記述言語として,情報システムの分析・設計・製作・評価の各工程で幅広く用いられてきた.しかし,組込システムの発展により,UMLも,よりハードウエアに近い領域でのソフトウェア設計にも利用できることが求められ,UML2.0よりタイミング図が利用可能となっている.タイミング図はステートマシン図によるオブジェクトの状態遷移と,シーケンス図によるオブジェク …

    IEICE technical report 114(188), 17-21, 2014-08-21

  • A cost-aware scheduling for real-time tasks based on the priced task automta  [in Japanese]

    YUEN Shoji , KAMEI Tatsuro

    本研究では、Fersmanらによって提案されたタスク生成とスケジュール可能性を時間オートマトンにもとづいて拡張したタスクオートマトンにコストの概念を導入する。スケジューリング可能な場合に、タスクをスケジュールするための時間あたり最適なコストを求める手法について提案する。タスクオートマトンで起動されるタスクタイプにコスト情報を付加し、タスクインスタンスの実行に対してコストを加算し、実行時間に対する平 …

    Technical report of IEICE. KBSE 114(128), 37-42, 2014-07-02

  • A cost-aware scheduling for real-time tasks based on the priced task automta  [in Japanese]

    YUEN Shoji , KAMEI Tatsuro

    本研究では、Fersmanらによって提案されたタスク生成とスケジュール可能性を時間オートマトンにもとづいて拡張したタスクオートマトンにコストの概念を導入する。スケジューリング可能な場合に、タスクをスケジュールするための時間あたり最適なコストを求める手法について提案する。タスクオートマトンで起動されるタスクタイプにコスト情報を付加し、タスクインスタンスの実行に対してコストを加算し、実行時間に対する平 …

    Technical report of IEICE. SS 114(127), 37-42, 2014-07-02

  • A cost-aware scheduling for real-time tasks based on the priced task automta  [in Japanese]

    Shoji Yuen , Tatsuro Kamei

    … This report presents a technique to give the optimal cost with respect to time passage when a set of tasks are schedulable in the model of task automata proposed by Fersman et.al. … When a task automata is schedulable, the optimal cost is shown to be computable according to the given scheduling strategy using double priced timed automata. …

    IPSJ SIG Notes 2014-SE-185(6), 1-6, 2014-07-02

    IPSJ

  • Well-Structured Pushdown System: Case of Dense Timed Pushdown Automata

    Cai Xiaojuan , Ogawa Mizuhito

    … As an instance, an alternative proof of the decidability of the reachability for dense-timed pushdown system (in P.A.Abdulla, M.F. … Stenman, Dense-Timed Pushdown Automata, IEEE LICS 2012) is presented. …

    Lecture Notes in Computer Science 8475, 336-352, 2014-06

    IR DOI

  • Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets

    TOYOSHIMA Ichiro , NAKANO Shota , YAMAGUCHI Shingo

    … In this paper, we proposed reduction operators of timed Petri net for efficient model checking. … Timed Petri nets are used widely for modeling and analyzing systems which include time concept. … Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. … In this paper, first, we have defined a concept of timed behavioral inheritance. …

    IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E97.A(2), 484-489, 2014

    J-STAGE

Page Top