スマートモビリティ研究開発センター

研究成果 2003 2017

フィルター
会議での発言
2017

ZipPath: A simple-but-useful path finder for HSTM designs in ZIPC

Kong, W., Hou, G., Hu, X., Arimoto, Y., Watanabe, M., Ando, T., Kenji, H. & Fukuda, A., 1 10 2017, Proceedings - 2016 International Conference on Agents, ICA 2016. Institute of Electrical and Electronics Engineers Inc., p. 154-157 4 p. 7812997. (Proceedings - 2016 International Conference on Agents, ICA 2016).

研究成果: 著書/レポートタイプへの貢献会議での発言

Transition Matrix
State Transition
Path
Software design
Software Design
2016
5 引用 (Scopus)

Towards sustainable information infrastructure platform for smart mobility - Project overview

Fukuda, A., Kenji, H., Ishida, S., Mine, T., Nakanishi, T., Furusho, H., Tagashira, S., Arakawa, Y., Kaneko, K. & Kong, W., 8 31 2016, Proceedings - 2016 5th IIAI International Congress on Advanced Applied Informatics, IIAI-AAI 2016. Hiramatsu, A., Matsuo, T., Kanzaki, A. & Komoda, N. (版). Institute of Electrical and Electronics Engineers Inc., p. 211-214 4 p. 7557604. (Proceedings - 2016 5th IIAI International Congress on Advanced Applied Informatics, IIAI-AAI 2016).

研究成果: 著書/レポートタイプへの貢献会議での発言

Life cycle
Uncertainty
2015
12 引用 (Scopus)

Software for wearable devices: Challenges and opportunities

Jiang, H., Chen, X., Zhang, S., Zhang, X., Kong, W. & Zhang, T., 9 21 2015, Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference Workshops, COMPSACW 2015. Ahamed, S. I., Chang, C. K., Crnkovic, I., Hsiung, P-A., Yang, J., Huang, G. & Chu, W. (版). IEEE Computer Society, p. 592-597 6 p. 7273430. (Proceedings - International Computer Software and Applications Conference; 巻数 3).

研究成果: 著書/レポートタイプへの貢献会議での発言

Computer science
Computer systems
2013
5 引用 (Scopus)

Formalization and model checking of SysML state machine diagrams by CSP#

Ando, T., Yatsu, H., Kong, W., Hisazumi, K. & Fukuda, A., 8 1 2013, Computational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings. PART 3 版 p. 114-127 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 7973 LNCS, 番号 PART 3).

研究成果: 著書/レポートタイプへの貢献会議での発言

Model checking
State Machine
Formalization
Model Checking
Diagram
2 引用 (Scopus)

Harnessing SMT-based bounded model checking through stateless explicit-state exploration

Kong, W., Liu, L., Ando, T., Yatsu, H., Kenji, H. & Fukuda, A., 1 1 2013, APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. Muenchaisri, P. & Rothermel, G. (版). IEEE Computer Society, 巻 1. p. 355-362 8 p. 6805426

研究成果: 著書/レポートタイプへの貢献会議での発言

Surface mount technology
Model checking
Systems analysis
Switches
3 引用 (Scopus)

Towards formal description of standards for automotive operating systems

Yatsu, H., Ando, T., Kong, W., Kenji, H., Fukuda, A., Aoki, T. & Futatsugi, K., 9 9 2013, Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013. p. 13-14 2 p. 6571601

研究成果: 著書/レポートタイプへの貢献会議での発言

Specifications
2012

A combined formal analysis methodology and towards its application to hierarachical state transition matrix designs

Kong, W., Liu, L., Yatsu, H. & Fukuda, A., 12 1 2012, VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle. p. 99-106 8 p.

研究成果: 著書/レポートタイプへの貢献会議での発言

Theorem proving
Model checking
Formal methods
Surface mount technology
Formal verification

A dynamic channel assignment method based on location information of mobile terminals in indoor WLAN positioning systems

Li, M., Han, L., Kong, W., Tagashira, S., Arakawa, Y. & Fukuda, A., 12 1 2012, 2012 International Conference on Indoor Positioning and Indoor Navigation, IPIN 2012 - Conference Proceedings. 6418883. (2012 International Conference on Indoor Positioning and Indoor Navigation, IPIN 2012 - Conference Proceedings).

研究成果: 著書/レポートタイプへの貢献会議での発言

Wireless local area networks (WLAN)
Wireless networks
Throughput
guarantee

Formal verification of communicating HSTM designs

Liu, L., Kong, W., Zhou, S., Qin, Z. & Fukuda, A., 12 1 2012, Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012. p. 383-390 8 p. 6391931

研究成果: 著書/レポートタイプへの貢献会議での発言

Message passing
Model checking
Formal verification
Systems analysis
Communication
6 引用 (Scopus)

On accelerating SMT-based bounded model checking of HSTM designs

Kong, W., Liu, L., Yamagata, Y., Taguchi, K., Ohsaki, H. & Fukuda, A., 1 1 2012, APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference. IEEE Computer Society, 巻 1. p. 614-623 10 p. 6462717

研究成果: 著書/レポートタイプへの貢献会議での発言

Model checking
Computer systems
Experiments
2008
1 引用 (Scopus)

Trace anonymity in the OTS/CafeOBJ method

Kong, W., Ogata, K., Cheng, J. & Futatsugi, K., 9 22 2008, Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008. p. 754-759 6 p. 4594769. (Proceedings - 2008 IEEE 8th International Conference on Computer and Information Technology, CIT 2008).

研究成果: 著書/レポートタイプへの貢献会議での発言

2007

Formalization and analysis of public administration domain with the OTS/CafeOBJ method

Chen, X., Xiang, J., Kong, W. & Futatsugi, K., 1 1 2007, ICEG 2007 - 3rd International Conference on e-Government. Academic Conferences Limited, p. 77-86 10 p. (ICEG 2007 - 3rd International Conference on e-Government).

研究成果: 著書/レポートタイプへの貢献会議での発言

Public administration
formalization
public administration
Transparency
electronic government
2006
4 引用 (Scopus)

Falsification of OTSs by searches of bounded reachable state spaces

Ogata, K., Kong, W. & Futatsugi, K., 12 1 2006, 18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006. p. 440-445 6 p. (18th International Conference on Software Engineering and Knowledge Engineering, SEKE 2006).

研究成果: 著書/レポートタイプへの貢献会議での発言

Authentication
14 引用 (Scopus)

Induction-guided falsification

Ogata, K., Nakano, M., Kong, W. & Futatsugi, K., 1 1 2006, Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings. Springer Verlag, p. 114-131 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 4260 LNCS).

研究成果: 著書/レポートタイプへの貢献会議での発言

Proof by induction
Counterexample
Authentication
State Space
Mathematical Induction
2005
23 引用 (Scopus)

A lightweight integration of theorem proving and model checking for system verification

Kong, W., Ogata, K., Seino, T. & Futatsugi, K., 12 1 2005, Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05. p. 59-66 8 p. 1607137. (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; 巻数 2005).

研究成果: 著書/レポートタイプへの貢献会議での発言

Theorem proving
Model checking
Specifications
1 引用 (Scopus)

Formal analysis of workflow systems with security considerations

Kong, W., Ogata, K. & Futatsugi, K., 12 1 2005, 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005. p. 531-536 6 p. (17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005).

研究成果: 著書/レポートタイプへの貢献会議での発言

Specification languages
Access control