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

研究成果 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
2014
4 引用 (Scopus)

A formal semantics of extended hierarchical state transition matrices using CSP#

Yamagata, Y., Kong, W., Fukuda, A., Van Tang, N., Ohsaki, H. & Taguchi, K., 9 2014, : : Formal Aspects of Computing. 26, 5, p. 943-962 20 p.

研究成果: ジャーナルへの寄稿記事

Formal Semantics
Transition Matrix
State Transition
Semantics
Modeling Language
4 引用 (Scopus)

An SMT-based accurate algorithm for the K-coverage problem in sensor network

Kong, W., Li, M., Han, L. & Fukuda, A., 1 1 2014, p. 240-245. 6 p.

研究成果: 会議への寄与タイプ論文

Sensor networks
Wireless sensor networks
Quality of service
Sensors
6 引用 (Scopus)

Facilitating Multicore Bounded Model Checking with Stateless Explicit-State Exploration

Kong, W., Liu, L., Ando, T., Yatsu, H., Hisazumi, K. & Fukuda, A., 8 11 2014, : : Computer Journal. 58, 11, p. 2824-2840 17 p.

研究成果: ジャーナルへの寄稿記事

Model checking
Temporal logic
Surface mount technology
Scalability
Systems analysis
5 引用 (Scopus)

Translation rules of SysML state machine diagrams into CSP# toward formal model checking

Ando, T., Yatsu, H., Kong, W., Kenji, H. & Fukuda, A., 6 1 2014, : : International Journal of Web Information Systems. 10, 2, p. 151-169 19 p.

研究成果: ジャーナルへの寄稿記事

Model checking
Modeling languages
2013
3 引用 (Scopus)

A survey of acceleration techniques for SMT-based bounded model checking

Liu, L., Kong, W., Ando, T., Yatsu, H. & Fukuda, A., 1 1 2013, p. 554-559. 6 p.

研究成果: 会議への寄与タイプ論文

Surface mount technology
Model checking
Binary decision diagrams
Temporal logic
Switches
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
2010
9 引用 (Scopus)

Towards reliable e-Government systems with the OTS/CafeOBJ method

Kong, W., Ogata, K. & Futatsugi, K., 1 1 2010, : : IEICE Transactions on Information and Systems. E93-D, 5, p. 974-984 11 p.

研究成果: ジャーナルへの寄稿記事

Formal methods
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
1 引用 (Scopus)

Formal support for e-Government system design with transparency consideration

Chen, X., Kong, W. & Futatsugi, K., 12 1 2007, ICEGOV 2007 - Proceedings of the 1st International Conference on Theory and Practice of Electronic Governance. p. 20-29 10 p. (ACM International Conference Proceeding Series; 巻数 232).

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

Public administration
Transparency
Systems analysis
Public works
Formal methods
8 引用 (Scopus)

Specification and verification of workflows with RBAC mechanism and SoD constraints

Kong, W., Ogata, K. & Futatsugi, K., 2 1 2007, : : International Journal of Software Engineering and Knowledge Engineering. 17, 1, p. 3-32 30 p.

研究成果: ジャーナルへの寄稿記事

Access control
Specifications
Specification languages
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
3 引用 (Scopus)

From fault tree analysis to formal system specification and verification with OTS/CafeOBJ

Xiang, J., Ogata, K., Kong, W. & Futatsugi, K., 10 30 2006, : : Computer Software. 23, 3, p. 134-146 13 p.

研究成果: ジャーナルへの寄稿記事

Fault tree analysis
Specifications
Semantics
Formal languages
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
2003

Constructing projection frequent pattern tree for efficient mining

Xiang, J. W., He, Y. X., Kokichi, F. & Kong, W., 6 1 2003, : : Wuhan University Journal of Natural Sciences. 8, 2 A, p. 351-357 7 p.

研究成果: ジャーナルへの寄稿記事

Data warehouses
Data mining
Costs