Papers - KATAYAMA Tetsuro
-
Kong W., Katahira N., Watanabe M., Katayama T., Hisazumi K., Fukuda A.
Proceedings - Asia-Pacific Software Engineering Conference, APSEC 81 - 88 2011.12
Language：Japanese Publishing type：Research paper (scientific journal) Publisher：Proceedings - Asia-Pacific Software Engineering Conference, APSEC
Hierarchical State Transition Matrix (HSTM) is a table-based modeling language for developing designs of software systems. Although widely used and adopted by (particularly Japanese) software industry, there is still lack of mechanized formal verification supports for conducting rigorous and automatic analysis to improve reliability of HSTM designs. In this paper, we first present a formalization of HSTM designs as state transition systems. Consequentially, based on this formalization, we propose a symbolic encoding approach, through which correctness of a HSTM design with respect to LTL properties could be represented as Bounded Model Checking (BMC) problems that could be determined by Satisfiability Modulo Theories (SMT) solving. We have implemented our encoding approach in a tool called Garakabu2 with the state-of-the-art SMT solver CVC3 as its back-ended solver. Furthermore, in our preliminary experiments, a conceptually simple but steadily effective way of accelerating SMT solving for HSTM designs is investigated and reported. © 2011 IEEE.
-
Proposal of an Execution Paths Indication Method for Integration Testing by Using an Automatic Visualization Tool `Avis' Reviewed
Y. Kita, T. Katayama, and S. Tomita
Proc. 5th World Congress for Softw. Quality(5WCSQ) 2011.11
Language：English Publishing type：Research paper (international conference proceedings)
-
コーディングとテストの並列開発手法実現のための一考察 Reviewed
大久保暢人, 松岡慎吾, 喜多義弘, 片山徹郎
ソフトウェアテストシンポジウム2011九州(JaSST'11 Kyushu) 30 - 32 2011.11
Language：Japanese Publishing type：Research paper (scientific journal)
-
An SMT-based approach to bounded model checking of designs in communicating state transition matrix
Kong W., Katahira N., Qian W., Watanabe M., Katayama T., Fukuda A.
Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011 159 - 167 2011.9
Language：Japanese Publishing type：Research paper (scientific journal) Publisher：Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011
State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results. © 2011 IEEE.
-
ソフトウェア要求仕様書に基づいたテスト項目作成手法の提案 Reviewed
喜多義弘, 鈴木三紀夫, 秋山浩一, 片山徹郎, 西康晴
情報処理学会 ソフトウェアエンジニアリングシンポジウム2011(SES2011) 2011 ( 2 ) 1 - 6 2011.9
Language：Japanese Publishing type：Research paper (scientific journal)
-
組込みソフトウェア開発支援のための命令セットシミュレータ(ISS)作成支援ツールの試作
東園修平, 片山徹郎
宮崎大学工学部紀要 ( 40 ) 263 - 268 2011.8
Language：Japanese Publishing type：Research paper (bulletin of university, research institution)
-
An SMT-based Approach to Bounded Model Checking of Designs in Communicating State Transition Matrix Reviewed
W. Kong, N. Katahira, W. Qian, M. Watanabe, T. Katayama, and A. Fukuda
11th Int'l Conf. on Computational Sci. and Its Application (ICCSA 2011) 159 - 167 2011.6
Language：English Publishing type：Research paper (international conference proceedings)
-
ランダムテスト手法を用いたJava プログラム単体テスト自動実行ツールの試作 Reviewed
松岡慎吾, 喜多義弘, 片山徹郎
ソフトウェア・シンポジウム SS2011 2011.6
Language：Japanese Publishing type：Research paper (scientific journal)
-
An SMT-Based Approach to Bounded Model Checking of Designs in State Transition Matrix Reviewed
W. Kong, T. Shiraishi, N. Katahira, M. Watanabe, T. Katayama, and A. Fukuda
IEICE Trans. on Info. & Sys. E94-D ( 5 ) 946 - 957 2011.5
Language：English Publishing type：Research paper (scientific journal)
-
An SMT-based approach to bounded model checking of designs in state transition matrix
Kong W., Shiraishi T., Katahira N., Watanabe M., Katayama T., Fukuda A.
IEICE Transactions on Information and Systems E94-D ( 5 ) 946 - 957 2011.5
Language：Japanese Publishing type：Research paper (scientific journal) Publisher：IEICE Transactions on Information and Systems
State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported. © 2011 The Institute of Electronics.
-
検証技法としてのモデル検証、その検証結果のフィードバックについて Reviewed
片平典幸, 孔維強, 渡辺政彦, 片山徹郎, 福田晃
ソフトウェアテストシンポジウム2010九州(JaSST'10 Kyushu) 44 - 45 2010.11
Language：Japanese Publishing type：Research paper (scientific journal)
-
Javaプログラム単体テスト自動実行ツール開発に向けた一考察 Reviewed
松岡慎吾, 片山徹郎
ソフトウェアテストシンポジウム2010九州(JaSST'10 Kyushu) 40 - 43 2010.11
Language：Japanese Publishing type：Research paper (scientific journal)
-
状態遷移構文とテスト構文を導入した組込みソフトウェア向けプログラミング言語開発 Reviewed
岡山直樹, 片山徹郎
情報処理学会 組込みシステムシンポジウム2010(ESS2010) 43 - 48 2010.10
Language：Japanese Publishing type：Research paper (scientific journal)
-
信頼性向上を目的とした組込みソフトウェア向けプログラミング言語の開発
岡山直樹, 片山徹郎
宮崎大学工学部紀要 ( 39 ) 301 - 306 2010.9
Language：Japanese Publishing type：Research paper (bulletin of university, research institution)
-
プログラム自動可視化ツールAvisを利用した結合テスト実施のための実行経路抽出手法の提案 Reviewed
喜多義弘, 片山徹郎, 冨田重幸
情報処理学会論文誌 51 ( 9 ) 1859 - 1872 2010.9
Language：Japanese Publishing type：Research paper (scientific journal)
-
Model Checking of Software Design in State Transition Matrix Reviewed
T. Shiraishi, W. Kong, Y. Mizushima, N. Katahira, M. Matsumoto, M. Watanabe, T. Katayama, and A. Fukuda
Proc. 2010 Int'l Conf. Softw. Eng. Research and Practice (SERP'10) 507 - 513 2010.7
Language：English Publishing type：Research paper (international conference proceedings)
-
結合テストのためのプログラム自動可視化ツールAvisによる実行経路表示手法の提案
喜多義弘, 片山徹郎, 冨田重幸
火の国情報シンポジウム2010 CD-ROM 2010.3
Language：Japanese Publishing type：Research paper (scientific journal)
-
Design and development of state transition matrix model checking tool Garakabu2.
SHIRAISHI T., KONG W., MATSUMOTO M., KATAYAMA T., FUKUDA A., MIZUSHIMA Y., KATAHIRA N., WATANABE M.
72 ( 0 ) 283 - 284 2010.3
Language：Japanese Publishing type：Research paper (scientific journal)
-
Extension and evaluation of an automatic visualization tool "Avis" for programming education
Kita Y., Tokunaga T., Katayama T., Tomita S.
Proceedings of the IASTED International Conference on Software Engineering, SE 2009 31 - 36 2009.12
Language：Japanese Publishing type：Research paper (scientific journal) Publisher：Proceedings of the IASTED International Conference on Software Engineering, SE 2009
As the demand for software is increasing more rapidly than ever, demand for educating novice programmers are increasing in order to increase the population of programmers to cope with this issue. We developed an automatic visualization tool "Avis" that generates a flowchart and execution paths from source codes of a Java programs for supporting programming education. This paper describes extension of Avis for generating sequence diagrams together with the evaluation of practical use in education to aids novice programmers to understand source code of programs.
-
FURUTONO TOMOYUKI, SAKAMOTO NORIAKI, MINE TSUNENORI, KUSAKABE SHIGERU, SUGANUMA AKIRA, KANEKO KUNIHIKO, NAKANISHI TSUNEO, FUKASE MITSUAKI, OMORI YOICHI, UDDIN MOHAMMAD MESBAH, NOMA TSUKASA, SUEYOSHI TOSHINORI, KATAYAMA TETSURO, MORIMOTO TSUYOSHI, ARAKI KEIJIRO, FUKUDA AKIRA, YASUURA HIROTO
IPSJ SIG Notes 2009 ( 32 ) 171 - 176 2009.3
Language：Japanese Publishing type：Research paper (scientific journal) Publisher：Information Processing Society of Japan (IPSJ)
The progress of Information Technology, which is the infrastructure of an advanced information society, is remarkable and has the enormous impact on our daily life. On the other hand, it has been pointed out by the industry that there is a lack of highly skilled ICT personnel who can lead the next generation. In order to address this issue, the Graduate School of Information Science and Electrical Engineering in Kyushu University has established Social Information System Engineering Course. In this education course, we have been running the practical education program with an objective to foster world class leader who has extraordinary technical skill and sense of ethics. This program is supported by various companies through Nippon Keidanren and by Ministry of Education, Culture, Sports, Science and Technology. This paper describes the content, method, result and evaluation for our two years experience. We also discuss the issues and concerns that need to be resolved.