‹ Dependable Systems Lab.
Japanese

Toshifusa Sekizawa

Home Publication Lectures

Books

  • Toshifusa Sekizawa, and Koichi Takahashi:
    "System Verification by Model Checking,"
    Reliability Engineering Associate of Japan (REAJ) 'Reliability Handbook', Chapter V, Section D-4, July 2014.
  • Kozo Okano, and Toshifusa Sekizawa (Eds.):
    "ソフトウェア工学の基礎 XX FOSE2013,"
    Kindai kagaku sha Co., Ltd., December 2013. (in Japanese)
  • Toshifusa Sekizawa and Koichi Takahashi:
    "Model Checking (general statement)"
    IEICE handbook 「知識ベース」 7群1編2章4, pp.28-34, 2010 (in Japanese)
  • Koichi Takahashi and Toshifusa Sekizawa:
    "Abstraction"
    IEICE handbook 「知識ベース」 7群1編3章1, pp.3-9, 2010 (in Japanese)

Journals

  • Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto:
    "Parallel Multiple Counter-Examples Guided Abstraction Loop - Applying to Timed Automaton -,"
    International Journal of Informatics Society (IJIS), Vol. 8, No. 2, pp.103-116, September 2016.
  • Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto:
    "Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects,"
    International Journal of Informatics Society (IJIS), Vol. 6, No.2, pp. 79-87, November 2014.
  • Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto:
    "Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model,"
    Special Issue of the International Journal of Informatics Society (IJIS), Vol. 5, No. 3, pp.147-155, March 2014.
  • [tutorial paper]
    Tatsuhiro Tsuchiya, and Toshifua Sekizawa:
    "Applications of Model Checking in the Area of Control Systems," ISCIE Journal 'Systems, Control and Information', Vol. 57, No. 5, pp.195-200, 2013 (in Japanese).
  • Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi, and Kazuko Takahashi:
    "Probabilistic Symmetry Reduction for a System with Ring Buffer"
    The IEICE Transactions on Information and Systems, Special Section on Formal Approach,
    Vol. E94-D, No. 5, pp. 967-975, May 2011.
  • Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi, and Kazuko Takahashi:
    "Probabilistic Symmetry Reduction for a System with Ring Buffer"
    The IEICE Transactions on Information and Systems, Special Section on Formal Approach,
    Vol. E94-D, No. 5, pp. 967-975, May 2011.
  • Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi, and Tohru Kikuno:
    "Probabilistic Model Checking of the One-Dimensional Ising Model"
    The IEICE Transactions on Information and Systems, Special Section on Formal Approach, Vol. E92-D, No. 5, pp. 1003-1011, May 2009.
  • Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
    "Pre- and Post-conditions Expressed in Variants of the Modal mu-calculus"
    The IEICE Transactions on Information and Systems, Special Section on Formal Approach, Vol. E92-D, No. 5, pp. 995-1002, May 2009.
  • Toshifusa Sekizawa, Toshinori Takai, Yoshinori Tanabe, and Koichi Takahashi:
    "A Method to Generate Formulas for Temporal Logic Satisfiability Checkers"
    Electronics and Communications in Japan, Part II, Vol. 90, Issue 11, pp. 98-108, October 2007.
      (Technical Report: AIST/CVS PS-2007-004, Feb. 2007)
  • Toshifusa Sekizawa, Toshinori Takai, Yoshinori Tanabe, and Koichi Takahashi:
    "A Method to Generate Formulae for Temporal Logic Satisfiability Checkers"
    The IEICE Transactions on Information and Systems(D) (Japanese Edition), Vol.J89-D, No.4, pp. 642-650, April 2006. (in Japanese)
      (Technical Report: AIST/CVS PS-2005-015, September 2005. (Preliminary version) (in Japanese))
  • Koichi Takahashi, Yoshinori Tanabe, and Toshifusa Sekizawa:
    "Finite Approximation Analysis of One Dimensional Cellular Automata"
    JSSST Computer Software, Vol.23, No.3, pp. 147-157, July 2006. (in Japanese with English abstract)
      (Technical Report: AIST/CVS PS-2005-014, August 2005. (in Japanese))

International Conferences

  • Ryo Watanabe, Kozo Okano, and Toshifusa Sekizawa:
    "Towards Verification of Robot Design for Self-localization,"
    Thirteenth Haifa Verification Conference (HVC 2017), LNCS, Vol. 10629, pp. 245-248, 2017. (Haifa, Israel)
  • Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, and Shin Nakajima:
    "Equivalence Checking of Java Methods - Towards Ensuring IoT Dependability -,"
    The 7th International Workshop on Internet on Things: Privacy, Security and Trust (ICCCN/IoTPST 2017). (Vancouver, Canada)
  • Toshifusa Sekizawa, Makoto Fujiwara, and Koichiro Watanabe:
    "A Case Study: Verification of an Embedded System using Abstraction Refinement with Requirements,"
    In Proceedings of COMPSAC 2016: The 2nd IEEE International Workshop on Dependable Software and Applications (DSA 2016), pp. 490-493, June 2016. (Atlanta, the United States)
  • Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto:
    "Parallel Multiple Counter-Examples Guided Abstraction Loop to Timed Automaton,"
    International Workshop on Informatics 2015 (IWIN2015), pp. 153-160, September 2015. (Amsterdam, Netherlands)
  • Toshifusa Sekizawa, Fumiya Otsuki, Kazuki Ito, and Kozo Okano:
    "Behavior Verification of Autonomous Robot Vehicle in Consideration of Errors and Disturbances,"
    In Proceedings of COMPSAC 2015 Workshop: The 1st IEEE International Workshop on Dependable Software and Applications (DSA 2015), pp. 550-555, July 2015. (Taichung, Taiwan)
  • Kozo Okano, and Toshifusa Sekizawa:
    "Safety Verification of Multiple Autonomous Systems by Formal Approach,"
    In Proceedings of International Conference on Computer Safety, Reliability, and Security (SAFECOMP) 2014 Workshops: ASCoMS, DECSoS, DEVVARTS, ISSE, ReSA4CI, SASSUR, September 2014. (Florence, Italy)
    Lecture Note in Computer Science (LNCS), Vol. 8696, pp. 11-18, 2014.
  • Toshifusa Sekizawa, and Tsugu Kotorii:
    "A Case Study: Verification of Specifications of an Embedded System and Generation of Verification Items using Pairwise Testing",
    In Proceedings of the 20th Asia-Pacific Software Engineering Conference (APSEC 2013), pp. 146-151, December 2013. (Bangkok, Thailand)
  • Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto:
    "Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects",
    International Workshop on Informatics 2013 (IWIN2013), pp. 155-162, September 2013. (Stockholm, Sweden)
  • Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto:
    "Verification of Safety Property of Line Tracer Program using Timed Automaton Model",
    International Workshop on Informatics 2012 (IWIN2012), pp. 136-142, September 2012. (Chamonix Mont-Blanc, France)
  • Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
    "Verification of the Deutsh-Schorr-Waite marking algorithm with Modal Logic"
    Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments ( VSTTE'08 ), Lecture Notes in Computer Science, Vol. 5295, pp. 115-129, Springer, October 2008. (Tronto, Canada)
  • Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, and Koichi Takahashi:
    "MLAT: A Tool for Heap Analysis Based on Predicate Abstraction by Modal Logic"
    Proceedings of the IASTED International Conference on Software Engineering (SE 2008), pp. 310-317, February 2008. (Innsbruck, Austria)
  • Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi:
    "Analyzing the One Dimensional Ising Model by Probabilistic Model Checking"
    Proceedings of the IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007), pp. 199-204, October 2007. (Beijing, China)
  • Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa and Koichi Takahashi:
    "Preconditions of Properties Described in CTL for Statements Manipulating Pointers"
    Supplemental Volume of the 2005 International Conference on Dependable Systems and Networks (DSN-2005), June 28 - July 1, 2005, pp. 228-234. (Yokohama, Japan).
      Technical Report： AIST/CVS PS-2005-007, March 2005.

Doctoral Thesis

  • Toshifusa Sekizawa
    "A Study of Model Checking with Emphasis on Program Verification and Probabilistic Analysis"
    Graduate School of Information Science and Technology, Osaka University, January 2009.

Workshops

  • 矢吹光，関澤俊弦:
    "自己位置推定をするロボットの確率的な振舞いの協調解析に向けて,"
    JSSST FOSE2017, Nov. 2017
  • 渡邊亮，岡野浩三，関澤俊弦:
    "モデル検査を用いたロボット設計の検証,"
    JSSST FOSE2017, Nov. 2017
  • 渡邊亮，岡野浩三 ，関澤俊弦:
    "自己位置推定を行なうロボット設計の検証に向けて,"
    IPSJ/SIGSE SES2017 ワークショップ「ソフトウェアと不確かさ」, August, 2017.
  • 岡野浩三，原内聡，小形真平，関澤俊弦，小原岳士:
    "Javaのメソッド等価性判定とその応用,"
    電子情報通信学会技術研究報告 IEICE-SS2016-65, Vol. 116, No. 512, pp.31-36, March 2017.
  • 渡辺誠人，岡野浩三，関澤俊弦:
    "ペアワイズ法に基づいた検証項目の生成とモデル検査による組み込みシステムの検証に向けて,"
    IPSJ/SIGSE ウィンターワークショップ・イン・飛騨高山, January, 2017.
  • 田幸玄陽，小形真平，岡野浩三，関澤俊弦:
    "Kuromojiと構文解析による要求仕様書から状態遷移系への自動変換の試み,"
    IPSJ/SIGSE ウィンターワークショップ・イン・飛騨高山, pp. 45-46, January, 2017.
  • Ryo Watanabe, Kozo Okano, and Toshifusa Sekizawa:
    "二次元系における自己位置推定の振舞い検証に向けて,"
    JSSST FOSE2016, ソフトウェア工学の基礎XXIII, pp. 275-276, Dec. 2016. (in Japanese)
  • Yoshimasa Kobayashi, Kozo Okano, and Toshifusa Sekizawa弦:
    "移動時間を考慮に入れた自律移動ロボットの確率的な振舞い検証に向けて," (ポスター)
    JSSST 第23回 ソフトウェア工学の基礎ワークショップ (FOSE2016), Dec. 2016. (poster, in Japanese)
  • Yoshimasa Kobayashi, Kozo Okano, and Toshifusa Sekizawa:
    "Modeling of an autonomous mobile robot using probabilistic timed automata,"
    IPSJ SIG Technical Report, Vol. 2016-SE-192, No. 14, June 2016. (in Japanese)
  • Toshifusa Sekizawa, and Kozo Okano:
    "Towards Behavior Verification of Estimation of Self-localization in One-dimensional Systems,"
    IEICE Technical Report SS2015-100, Vol. 115, No. 508, pp.145-150, March 2016. (in Japanese)
  • Ken Endo, Shinpei Ogata, Kozo Okano, and Toshifusa Sekizawa:
    "Towards Formal Verification on Specification in a Natural Language - Model Checking for "Electric pot, GOMA type 1015"-,"
    IPSJ/SIGSE Winter Workshop 2016 in Zushi, pp. 3-4, February 2016. (in Japanese)
  • Yoshimasa Kobayashi, Kozo Okano, Toshifusa Sekizawa:
    "時間的性質を考慮に入れた自律移動ロボットの誤差検出と振舞い検証に向けて,"
    JSSST 第22回 ソフトウェア工学の基礎ワークショップ (FOSE2015), November, 2015. (poster)
  • Fumiya Otsuki, Kazuki Ito, Kozo Okano, and Toshifusa Sekizawa:
    "Towards behavior verification of autonomous mobile robot with error detection and correction,"
    IPSJ/SIGSE Winter Workshop 2015 in Ginowan, pp. 69-70, January 2015. (in Japanese).
  • Toshifusa Sekizawa, and Tsugu Kotorii:
    "組込みシステムの仕様検証とペアワイズ法を用いた検証項目の生成,"
    JSSST 第20回 ソフトウェア工学の基礎ワークショップ (FOSE2013), November, 2013. (poster)
  • Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, and Shinji Kusumoto:
    "UPPAALによるライントレーサの安全性検証のケーススタディ,"
    IPSJ/SIGSE Software Engineering Symposium (SES2012), August 2012.
  • Toshifusa Sekizawa, Koichi Takahashi, and Kazuko Takahashi:
    "リングバッファ上の系に対する確率的対称性簡約,"
    Winter Workshop 2012 in Biwako, IPSJ Symposium Series Vol.2012, No.1, pp.115-116, January 2012.
  • Hideki Kawai, Kozo Okano, and Toshifusa Sekizawa:
    "Towards Quantitative Evaluation and Verification of Linetracer,"
    Winter Workshop 2012 in Biwako, IPSJ Symposium Series Vol.2012, No.1, pp.113-114, January 2012.
  • Toshifusa Sekizawa，Koichi Takahashi, and Kazuko Takahashi:
    "ケーススタディ： Hermanの確率的自己安定化アルゴリズムの状態削減と検証,"
    Dependable System Workshop & Symposium (DSW & DSS 2011), December 2011.
  • Takashi Toyoshima, Kazuko Takahashi, and Toshifusa Sekizawa:
    "Probabilistic Model Checking for AIS with Symmetry Reduction,"
    IEICE Technical Report(SS2009-63), Vol. 109, No. 456, pp.91-96, March 2010.
  • Toshifusa Sekizawa, Satoshi Koike, Takashi Koike, Koichi Shinozaki, Hideaki Nishihara, and Koji Hayamizu:
    "Development of a Scenario-based Method for Introducing the Model Checking,"
    The 6th Dependable System Symposium (DSS2009), December 2009.
  • Koichi Takahashi, Toshifusa Sekizawa, Yoshifumi Yuasa, and Yoshinori Tanabe:
    "様相論理を使ったDeutsch-Schorr-Waiteマーキングアルゴリズムの検証,"
    The 5th Symposium on System Verification (SSV 2008), November 2008.
  • Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi:
    "A Case Study: Analyzing the One Dimensional Ising Model by Probabilistic Model Checking,"
    5th VERITE (JAIST/TRUST-AIST/CVS joint workshop on VERIfication TEchnology), March 2008.
  • Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
    "Agda-MLAT連携による Schorr-Waiteマーキングアルゴリズムの検証,"
    JSSST 24th Annual Conference, September 2007.
  • Yoshinori Tanabe, Yoshifumi Yuasa, Toshifusa Sekizawa, and Koichi Takahashi:
    "様相μ計算を利用したポインタを扱うプログラムの検証に向けて,"
    JSSST Workshop on Programming and Programming Languages (PPL 2007), March 2007.
  • Koichi Takahashi, Yoshifumi Yuasa, Makoto Takeyama, Toshifusa Sekizawa, and Yoshinori Tanabe:
    "自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について,"
    Theorem Proving and Provers (TPP) Meeting, November 2006.
  • Koichi Takahashi, Yoshinori Tanabe, Toshifusa Sekizawa, and Yoshifumi Yuasa:
    "抽象化ツールMLATについて,"
    第三回システム検証の科学技術シンポジウム, October 2006.
  • Yoshifumi Yuasa, Makoto Takeyama, Toshifusa Sekizawa, Yoshinori Tanabe, and Koichi Takahashi:
    "自動証明系と対話型証明支援系の連携によるポインタ操作プログラムの検証について,"
    JSSST 23nd Annual Conference, September 2006.
  • Yoshinori Tanabe, Yoshifumi Yuasa, Toshifusa Sekizawa, and Koichi Takahashi:
    "様相論理を使用したヒープ検証方式,"
    3rd Dependable Software Workshop (DSW'06), January 2006.
  • Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
    "抽象化ツールTLATの構築に向けて,"
    第2回システム検証の科学技術シンポジウム, October 21, 2005 (poster session, in Japanese)
      (Technical Report： AIST/CVS PS-2005-017, pp. 101-101, October 2005. (in Japanese))
  • Koichi Takahashi, Yoshinori Tanabe, Toshifusa Sekizawa and Yoshifumi Yuasa:
    "Abstraction of programs in PML (Pointer Manipulating Language),"
    JAIST/TRUST - AIST/CVS joint workshop on verification technology (VERITE) (oral presentation), September 21, 2005.
  • Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
    "時相論理による自動抽象化のための充足可能性判定手続き,"
    Japan Society for Software Science and Technology (JSSST), 22nd Annual Conference, September 2005.
  • Koichi Takahashi, Yoshinori Tanabe, and Toshifusa Sekizawa:
    "Finite Approximation Analysis of One Dimensional Cellular Automata,"
    Japan Society for Software Science and Technology (JSSST), 22nd Annual Conference, September 2005.
  • Koichi Takahashi, Yoshinori Tanabe, Toshinori Takai, and Toshifusa Sekizawa:
    "ポインタ処理システムのための自動抽象化手法,"
    JST，CREST program "New High-Performance Information Processing Technology Supporting Information-Oriented Society" 1st symposium, December 2004.
  • Satoshi Hirano, and Toshifusa Sekizawa:
    "Distributed Object-Oriented Technology HORB,"
    COMDEX Las Vegas 2003, November 19, 2003 - November 22, 2003.
  • K. Hosoya, T. Sekizawa, T. Okamoto, S. Kawaji, A. Yutani, and Y. Shiraki:
    "Metal-Insulator Transition and Magnetoresistance in High Mobility Silicon Two-Dimensional Electron System,"
    Meeting abstrasts of the Physical Society of Japan, Vol.53, No.1-3(19980310), p.536, March 30, 1998.
  • T. Sekizawa, T. Okamoto, and S. Kawaji:
    "Magnetoresistance in Strongly Localized States in Si-MOSFETs,"
    Meeting abstracts of the Physical Society of Japan, Vol.52, No.1-2(19970317), p.148, March 28, 1997.
  • T. Okamoto, Y. Ohkawara, T. Sekizawa, and S. Kawaji:
    "Giant Magnetoresistance in Si-MOSFETs in Tilted Magnetic Fields,"
    Abstracts of the meeting of the Physical Society of Japan, Vol.51, No.2(19960315), p.184, March, 1996.

Technical Reports

  • Toshifusa Sekizawa, and Tsugu Kotorii:
    "事例研究：組込みシステムの仕様検証とペアワイズ法を用いた評価項目の生成,"
    MSS技報, Vol.25, February, 2015.
  • Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
    "Pre- and Post-conditions Expressed in Variants of the Modal mu-calculus"
    AIST/CVS PS-2008-009, April 2008.
  • Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, and Koichi Takahashi:
    "MLAT: Modal Logic Abstraction Tool"
    AIST/CVS PS-2007-004, February 2007.