Research Output 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., Hisazumi, K. & Fukuda, A., Jan 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Transition Matrix
State Transition
Path
Software design
Software Design
2016
5 Citations (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., Aug 31 2016, Proceedings - 2016 5th IIAI International Congress on Advanced Applied Informatics, IIAI-AAI 2016. Hiramatsu, A., Matsuo, T., Kanzaki, A. & Komoda, N. (eds.). 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Life cycle
Uncertainty
2015
14 Citations (Scopus)

Software for wearable devices: Challenges and opportunities

Jiang, H., Chen, X., Zhang, S., Zhang, X., Kong, W. & Zhang, T., Sep 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. (eds.). IEEE Computer Society, p. 592-597 6 p. 7273430. (Proceedings - International Computer Software and Applications Conference; vol. 3).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Computer science
Computer systems
2014
4 Citations (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., Sep 2014, In : Formal Aspects of Computing. 26, 5, p. 943-962 20 p.

Research output: Contribution to journalArticle

Formal Semantics
Transition Matrix
State Transition
Semantics
Modeling Language
4 Citations (Scopus)

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

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

Research output: Contribution to conferencePaper

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

Facilitating Multicore Bounded Model Checking with Stateless Explicit-State Exploration

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

Research output: Contribution to journalArticle

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

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

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

Research output: Contribution to journalArticle

Model checking
Modeling languages
2013
3 Citations (Scopus)

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

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

Research output: Contribution to conferencePaper

Surface mount technology
Model checking
Binary decision diagrams
Temporal logic
Switches
6 Citations (Scopus)

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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Model checking
State Machine
Formalization
Model Checking
Diagram
2 Citations (Scopus)

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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Towards formal description of standards for automotive operating systems

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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., Dec 1 2012, VALID 2012 - 4th International Conference on Advances in System Testing and Validation Lifecycle. p. 99-106 8 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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., Dec 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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., Dec 1 2012, Proceedings - 2012 IEEE 12th International Conference on Computer and Information Technology, CIT 2012. p. 383-390 8 p. 6391931

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

On accelerating SMT-based bounded model checking of HSTM designs

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Model checking
Computer systems
Experiments
2010
9 Citations (Scopus)

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

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

Research output: Contribution to journalArticle

Formal methods
Experiments
2008
12 Citations (Scopus)

A specification translation from behavioral specifications to rewrite specifications

Nakamura, M., Kong, W., Ogata, K. & Futatsugi, K., Jan 1 2008, In : IEICE Transactions on Information and Systems. E91-D, 5, p. 1492-1503 12 p.

Research output: Contribution to journalArticle

Specifications
1 Citation (Scopus)

Trace anonymity in the OTS/CafeOBJ method

Kong, W., Ogata, K., Cheng, J. & Futatsugi, K., Sep 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2007

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

Chen, X., Xiang, J., Kong, W. & Futatsugi, K., Jan 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Public administration
formalization
public administration
Transparency
electronic government
1 Citation (Scopus)

Formal support for e-Government system design with transparency consideration

Chen, X., Kong, W. & Futatsugi, K., Dec 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; vol. 232).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Specification and verification of workflows with RBAC mechanism and SoD constraints

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

Research output: Contribution to journalArticle

Access control
Specifications
Specification languages
2006
4 Citations (Scopus)

Falsification of OTSs by searches of bounded reachable state spaces

Ogata, K., Kong, W. & Futatsugi, K., Dec 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authentication
3 Citations (Scopus)

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

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

Research output: Contribution to journalArticle

Fault tree analysis
Specifications
Semantics
Formal languages
14 Citations (Scopus)

Induction-guided falsification

Ogata, K., Nakano, M., Kong, W. & Futatsugi, K., Jan 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); vol. 4260 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Theorem proving
Model checking
Specifications
1 Citation (Scopus)

Formal analysis of workflow systems with security considerations

Kong, W., Ogata, K. & Futatsugi, K., Dec 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Specification languages
Access control
2004
1 Citation (Scopus)

Formal analysis of an anonymous fair exchange e-commerce protocol

Kong, W., Ogata, K., Xiang, J. & Futatsugi, K., Dec 14 2004, Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004). Wei, D., Wang, H., Peng, Z., Kara, A. & He, Y. (eds.). p. 1100-1107 8 p. (Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Network protocols
Specification languages
2003

Constructing projection frequent pattern tree for efficient mining

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

Research output: Contribution to journalArticle

Data warehouses
Data mining
Costs