SHAOYING LIU

Last Updated :2024/12/03

Affiliations, Positions
Graduate School of Advanced Science and Engineering, Professor
Web Site
https://home.hiroshima-u.ac.jp/sliu/
E-mail
sliuhiroshima-u.ac.jp
Self-introduction
Shaoying Liu is currently a Professor of Software Engineering at Hiroshima University, Japan. Previously, he was a Professor at Hosei University from April 2000 to March 2020. He received the Ph.D in Computer Science from the University of Manchester, U.K in 1992. His research interests include Formal Methods and Formal Engineering Methods for Software Development, Specification Verification and Validation, Specification-based Program Inspection, Automatic Specification-based Testing, Testing-Based Formal Verification, Human-Machine Pair Programming, and Intelligent Software Engineering Environments. He has published a book entitled "Formal Engineering for Industrial Software Development" with Springer Verlag, twelve edited conference proceedings, and over 200 academic papers in refereed journals and international conferences. He proposed to use the terminology of "Formal Engineering Methods" in 1997, and has established Formal Engineering Methods as a research area based on his extensive research on the SOFL (Structured Object-Oriented Formal Language) method since 1989, and the development of ICFEM conference series since 1997. In recent years, he has served as the General Chair of QRS 2020 and ICFEM 2017, Steering Committee Chair of ICECCS, and PC member for numerous international conferences. He is currently an Associate Editor for IEEE Transactions on Reliability and the Journal of Innovations in Systems and Software Engineering, respectively. He is IEEE Fellow, BCS Fellow, AAIA Fellow, and a member of IPSJ and IEICE.

Basic Information

Major Professional Backgrounds

  • 2017/08/01, 2020/07/31, Beijing Jiaotong University, Department of Computer Science, Visiting Professor
  • 2008/09/01, 2011/08/31, Xi'an Jiaotong University, School of Software, Visiting Professor
  • 2003/08/01, 2006/07/31, Shanghai University, Department of Computer Science, Visiting Professor
  • 2003/08/01, 2006/07/31, Shanghai Jiaotong University, School of Software, Adjunct Professor
  • 2005/04/01, 2006/03/31, University of York (UK), Department of Computer Science, Visiting Professor
  • 1998/12/01, 1999/02/28, University of Oxford (UK), Department of Computer Science, Visiting Professor
  • 1994/12/01, 1995/02/28, The Queen's University of Belfast (Northern Ireland, UK), Department of Computer Science, Research Fellow
  • 2020/04/01, Hiroshima University, Graduate School of Advanced Science and Engineering, School of Informatics and Data Science, Professor
  • 2001/04/01, 2020/03/31, Hosei University, Department of Computer Science, Faculty of Information Sciences, Professor
  • 2000/04/01, 2001/03/31, Hosei University, Department of Computer Science, Faculty of Information Sciences, Associate Professor
  • 1994/04/01, 2000/03/31, Hiroshima City University, Department of Computer Science, Associate Professor
  • 1993/05/21, 1994/03/01, RHBNC, University of London (UK), Department of Computer Science, Research Assistant
  • 1991/02/01, 1993/05/20, University of York (UK), Department of Computer Science, Research Associate
  • 1987/10/01, 1989/01/01, Xi'an Jiaotong University, Department of Computer Science, Lecturer
  • 1982/02/01, 1987/09/01, Xi'an Jiaotong University, Department of Computer Science, Assistant Lecturer

Educational Backgrounds

  • The University of Manchester, England, 1989/01, 1992/10
  • Xi'an Jiaotong University, China, 1984/09, 1987/04
  • Xi'an Jiaotong University, China, 1978/02, 1982/01

Academic Degrees

  • Xi'an Jiaotong University
  • Ph.D (Computer Science), The University of Manchester (UK)

In Charge of Primary Major Programs

  • Mathematical and Information Sciences

Research Fields

  • Informatics;Computing Technologies;Software

Research Keywords

  • Software Engineering, Formal Methods, Formal Specification Techniques, Software Testing, Software Formal Verification, Intelligent Software Engineering Environment

Affiliated Academic Societies

Educational Activity

Course in Charge

  1. 2024, Liberal Arts Education Program1, 3Term, Starting Programming from Scratch
  2. 2024, Liberal Arts Education Program1, 1Term, Introductory Seminar for First-Year Students
  3. 2024, Undergraduate Education, 1Term, Informatics Seminar I
  4. 2024, Undergraduate Education, 2Term, Informatics Seminar II
  5. 2024, Undergraduate Education, Second Semester, Graduation Thesis
  6. 2024, Graduate Education (Master's Program) , 1Term, Special Exercises on Informatics and Data Science A
  7. 2024, Graduate Education (Master's Program) , 2Term, Special Exercises on Informatics and Data Science A
  8. 2024, Graduate Education (Master's Program) , 3Term, Special Exercises on Informatics and Data Science B
  9. 2024, Graduate Education (Master's Program) , 4Term, Special Exercises on Informatics and Data Science B
  10. 2024, Graduate Education (Master's Program) , Academic Year, Special Study on Informatics and Data Science
  11. 2024, Graduate Education (Doctoral Program) , Academic Year, Special Study on Informatics and Data Science

Research Activities

Academic Papers

  1. ★, Detecting Security Vulnerabilities in Human-Machine Pair Programming with Pointer Analysis, ICECCS 2023, 152-156, 20230614
  2. A Framework of Formal Specification-Based Data Generation for Deep Neural Networks, ICSCA '23: Proceedings of the 2023 12th International Conference on Software and Computer Applications, 20230201
  3. Multi-Misconfiguration Diagnosis via Identifying Correlated Configuration Parameters, IEEE Transactions on Software Engineering, 49(10), 4624-4638, 20231001
    Link to Paper Search Results by DOI
  4. ★, Towards Pointer-Analysis-Based Vulnerability Discovery in Human-Machine Pair Programming, International Journal of Software Engineering and Knowledge Engineering (IJSEKE), 20240105
    Link to Paper Search Results by DOI
  5. ID-SR: Privacy-preserving Social Recommendation based on Infinite Divisibility for Trustworthy AI, ACM Transactions on Knowledge Discovery from Data, 20240102
    Link to Paper Search Results by DOI
  6. ★, Detecting security vulnerabilities with vulnerability nets, Journal of Systems and Software, 208(111902), 20240201
    Link to Paper Search Results by DOI
  7. The Threat of Adversarial Attack on a COVID-19 CT Image-Based Deep Learning System, Bioengineering (Basel), 10(2), 194, 20230201
  8. Real-time Diagnosis of Configuration Errors for Software of AI Server Infrastructure, IEEE Transactions on Dependable and Secure Computing, 1-12, 20230410
    Link to Paper Search Results by DOI
  9. ASQ-FastBM3D: An Adaptive Denoising Frameowrk for Defending Adversarial Attacks in Machine Learning Enabled Systems, IEEE Transactions on Reliability, 72(1), 317-328, 20230301
    Link to Paper Search Results by DOI
  10. ★, A Practical Model-Driven Approach for Designing Security Aware RESTful Web APIs using SOFL, IEICE Transactions on Information and Systems, E106.D(5), 986-1000, 20230501
    Link to Paper Search Results by DOI
  11. NNTBFV: Simplifying and Verifying Neural Networks Using Testing-Based Formal Verification, INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 34(02), 273-300, 202402
    Link to Paper Search Results by DOI
  12. ★, Cross-Project Transfer Learning on Lightweight Code Semantic Graphs for Defect Prediction, INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 33(07), 1095-1117, 20230701
    Link to Paper Search Results by DOI
  13. ★, Requirements-related fault prevention during the transformation from formal specifications to programs, IET SOFTWARE, 17(3), 316-332, 20230501
    Link to Paper Search Results by DOI
  14. Requirements-Related Fault Prevention Mechanism for SOFL Formal Specification-Based Programming, 2022 IEEE 22nd International Conference on Software Quality, Reliability, and Security Companion (QRS-C), 359-367, 20221205
  15. Construction of Semantic Model for GUI of Mobile Applications Using Deep Learning, 2022 IEEE International Conference On Artificial Intelligence Testing (AITest), 7-11, 20220815
  16. A systematic method for identifying safety-related faults in formal specifications using FTA, The 13th International Conference on Reliability, Maintainability, and Safety (ICRMS 2022), 87-92, 20220821
  17. Delay-CJ: A novel cryptojacking covert attack method based on delayed strategy and its detection, Digital Communicationks and Networks, 20220513
  18. Mining Python Fix Patterns via Analyzing Fine-Grained Source Code Change, Empirical Software Engineering, 27(48), 1-37, 20220128
  19. An Integrated Formal Method Combining Labeled Transition System and Event-B for System Model Refinement, IEEE ACCESS, 10, 13089-13102, 20220205
  20. ★, Automatic Test Case and Test Oracle Generation based on Functional Scenarios in Specifications for Conformance Testing, IEEE Transactions on Software Engineering, 48(2), 691-712, 20220201
  21. A Framework for Modeling and Detecting Security Vulnerabilities in Human-Machine Pair Programming, JOURNAL OF INTERNET TECHNOLOGY, 23(5), 1129-1138, 2022
    Link to Paper Search Results by DOI
  22. Probabilistic mediator: A coalgebraic perspective, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 129, 202211
    Link to Paper Search Results by DOI
  23. CPFL: An Effective Secure Cognitive Personalized Federated Learning Mechanism for Industry 4.0, IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 18(10), 7186-7195, 202210
    Link to Paper Search Results by DOI
  24. DevFemOps: enhancing maintainability based on microservices using formal engineering methods, CONNECTION SCIENCE, 34(1), 2125-2138, 20221231
    Link to Paper Search Results by DOI
  25. TBEM: Testing-Based GPU-Memory Consumption Estimation for Deep Learning, IEEE ACCESS, 10, 39674-39680, 2022
    Link to Paper Search Results by DOI
  26. Knowledge Graph Construction for SOFL Formal Specifications, INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 32(04), 605-644, 202204
    Link to Paper Search Results by DOI
  27. Gated Homogeneous Fusion Networks With Jointed Feature Extraction for Defect Prediction, IEEE TRANSACTIONS ON RELIABILITY, 71(2), 512-526, 202206
    Link to Paper Search Results by DOI

  28. SG-PBFT: A secure and highly efficient distributed blockchain PBFT consensus algorithm for intelligent Internet of vehicles

    , JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 164, 1-11, 202206
    Link to Paper Search Results by DOI
  29. Applying Cognitive Complexity to Checklist-Based Human-Machine Pair Inspection, IEEE International Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement (FPDRE), QRS 2021 Companion, 20211204
  30. A Tool to Support Vibration Testing Method for Automatic Test Case Generation and Test Result Analysis, The 21st IEEE International Conference on Software Quality, Reliability, and Security (QRS 2021), 149-156, 20211204
  31. EPR: a Neural Network for Automatic Feature Learning from Code for Defect Prediction, The 21st IEEE International Conference on Software Quality, Reliability, and Security (QRS 2021), 482-492, 20211204
  32. Multilevel Traceability Links Establishment Between SOFL Formal Specifications and Java Codes Using Multi-dimensional Similarity Measures, The 21st IEEE International Conference on Software Quality, Reliability, and Security (QRS 2021), 852-863, 20211204
  33. Testing Program Segments to Detect Software Faults during Programming, International Journal of Performability Engineering, 11, 907-917, 20211115
  34. An Integrated Formal Method Combining Labeled Transition System and Event-B for System Model Refinment, IEEE ACCESS, 10, 13089-13102, 20220201
  35. Checklist-Based Intelligent Human-Machine Pair Inspection, 270-274, 202109
  36. A Framework for Automatic Detection of Vulnerabilities in Human-Machine Pair Programming, 129-136, 202109
  37. Program Segment Testing for Software Fault Prevention, 191-195, 202109
  38. Testing-based GPU-Memory Consumption Estimation for Deep Learning, 196-199, 202109
  39. Building SOFL-to-Java Traceability Links using Multi-dimensional Similarity Measures, 143-150, 202109
  40. Combining Attention-based Gated Bidirectional LSTM and ODCN for Software Defect Prediction, 175-180, 202109
  41. Defending Use-After-Free via Relationship Between Memory and Pointer, Proceedings of International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom 2020), 583-597, 202101
  42. A Formal Approach to Secure Design of RESTful web APIs using SOFL, proceedings of the 10th International Workshop on SOFL+MSVL for Reliability and Security (SOFL+MSVL 2020), 105-125, 2021
  43. SMT-Based Theorem Verification for Testing-Based Formal Verification, Proceedings of the 10th International Conference on Software and Computer Applications (ICSCA2021), 251-257, 2021
  44. ★, Range Partition Testing: Principle and Technique, Proceedings of 2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C), 104-107, 2020
  45. A Fault Localization Approach Derived from Testing-Based Formal Verification, Proceedings of the 25th International Conference on Engineering of Complex Computer Systems, 165-170, 2021
  46. ★, A Framework for Integrating Formal Specification, Review, and Testing to Enhance Software Reliability, International Journal of Software Engineering and Knowledge Engineering, 21(2), 259, 2011
  47. ★, SOFL: A Formal Engineering Methodology for Industrial Applications, IEEE Transactions on Software Engineering, 24-45, 1998
  48. ★, A Rigorous Method for Inspection of Model-Based Formal Specifications, IEEE Transactions on Reliability, 59(4), 667, 2010
  49. ★, A Formal Approach to Testing Programs in Practice, Journal of Computer Science and Information Systems, 9(4), 1469-1491, 2012
  50. ★, Formal Specification-Based Inspection for Verification of Programs, IEEE Transactions on Software Engineering, 35(8), 1100-1122, 2012
  51. ★, A Formal Framework for Service-Based Software Modelling, IEEE Transactions on Services Computing, 6(4), 536-550, 2013
  52. ★, Computer-aided Formalization of Requirements Based on Patterns, IEICE Transactions on Information and Systems, E97.D(2), 198-212, 2014
  53. ★, Integrating Animation-Based Inspection into Formal Design Specification Construction for Reliable Software Systems, IEEE Transactions on Reliability, 65(1), 88-106, 2016
  54. Development of a Web Dictionary System Using SOFL, International Journal on Wireless Personal Communications, 94(2), 253-266, 2017
  55. Design and Implementation of Automated Visualization for Input / Output for Processes in SOFL Formal Specifications, 9(4), 139-157, 2018
  56. Validation and Verification of SYSML Activity Diagrams Using Hoare Logic, International Journal of Software Engineering & Applications, 9(4), 101-117, 2018
  57. autoC: an Efficient Translator for Model Checking Deterministic Scheduler based OSEK/VDX Applications, Science China Information Sciences, 61, 052102, 2018
  58. Test Oracle Generation Based on BPNN using Values of Variables at Different Breakpoints for Programs, International Journal of Software Engineering and Knowledge Engineering, 2021
  59. OFEI: A Semi-black-box Android Adversarial Sample Attack Framework Against DLaaS, IEEE Transactions on Computer, 2021
  60. ★, Automatic Test Case and Test Oracle Generation based on Functional Scenarios in Formal Specifications for Conformance Testing, IEEE Transactions on Software Engineering, 202006
    Link to Paper Search Results by DOI
  61. BAGKD: A Batch Authentication and Group Key Distribution Protocol for VANETs, IEEE COMMUNICATIONS MAGAZINE, 58(7), 35-41, 2020
    Link to Paper Search Results by DOI
  62. ★, Rigorous Code Review by Reverse Engineering, Information and Software Technology, 133, 106503, 2021
    Link to Paper Search Results by DOI
  63. Mutated Specification-based Test Data Generation with Genetic Algorithm, Mathematics, 9(4), 331, 2021
  64. ★, A three-step hybrid specification approach to error prevention, JOURNAL OF SYSTEMS AND SOFTWARE, 178, 110975, 2021
    Link to Paper Search Results by DOI
  65. ★, A formal specification animation method for operation validation, JOURNAL OF SYSTEMS AND SOFTWARE, 178, 110948, 2021
    Link to Paper Search Results by DOI
  66. ★, SIT-SE: A Specification-Based Incremental Testing Method With Symbolic Execution, IEEE TRANSACTIONS ON RELIABILITY, 70(3), 1053-1070, 2021
    Link to Paper Search Results by DOI
  67. Sparse Trust Data Mining, IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY, 16, 4559-4573, 2021
    Link to Paper Search Results by DOI
  68. Test Oracle Generation Based on BPNN by Using the Values of Variables at Different Breakpoints for Programs, INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 31(10), 1469-1494, 202110
    Link to Paper Search Results by DOI
  69. Modeling and Verifying the CKB Blockchain Consensus Protocol, MATHEMATICS, 9(22), 202111
    Link to Paper Search Results by DOI
  70. Mining Python fix patterns via analyzing fine-grained source code changes, EMPIRICAL SOFTWARE ENGINEERING, 27(2), 202203
    Link to Paper Search Results by DOI
  71. An Integrated Formal Method Combining Labeled Transition System and Event-B for System Model Refinement, IEEE ACCESS, 10, 13089-13102, 2022
    Link to Paper Search Results by DOI

Publications such as books

  1. 2022/10/24, Structured Object-Oriented Formal Language and Method, 11th International Workshop, SOFL-MSVL 2022, LNCS 13854. Revised selected papers, 11th International Workshop, SOFL-MSVL 2022, LNCS 13854. Revised selected papers., Formal engineering method, SOFL, MSVL, Formal methods, Springer, 2022, 10, Scholarly Book, Joint work, 英語, Shaoying Liu, Zhenhua Duan, Ai Liu, ISBN-10: 3031294750, ISBN-13: 978-3031294754, 163, 163
  2. 2021, Structured Object-Oriented Formal Language and Method, The Structured Object-Oriented Formal Language (SOFL) has been developed to address the challenge of how to transform formal methods principles and techniques into practice by providing a comprehensible specification language, a practical mod-eling method, various verification and validation techniques, and tool support through effective integration of formal methods with conventional software engineer-ing techniques. SOFL integrates Data Flow Diagram, Petri Nets, and VDM-SL to offer a visualized and formal notation for specification construction; a three-step ap-proach to requirements acquisition and system design; specification-based inspection and testing methods for detecting errors in both specifications and programs, and a set of tools to support modeling and verification. The Modeling, Simulation and Veri-fication Language (MSVL) is a parallel programming language. Its supporting toolkit MSV has been developed to enable us to model, simulate and verify a system in a formal manner. Following the success of previous SOFL+MSVL workshops, this workshop aims to continuously promote the development and combinations of the SOFL formal engineering method and the formal method MSVL, as well as the appli-cations of their fundamental principles and specific techniques to developing other formal engineering techniques. The workshop attracted 24 submissions on formal modeling, formal verification, model checking, metamorphic testing, natural language processing, and geometric modeling. Each submission is rigorously reviewed by two or more PC members on the basis of technical quality, relevance, significance, and clarity, and 13 papers were accepted for publication in the workshop proceedings. The acceptance rate is 54%., The Structured Object-Oriented Formal Language (SOFL) has been developed to address the challenge of how to transform formal methods principles and techniques into practice by providing a comprehensible specification language, a practical mod-eling method, various verification and validation techniques, and tool support through effective integration of formal methods with conventional software engineer-ing techniques. SOFL integrates Data Flow Diagram, Petri Nets, and VDM-SL to offer a visualized and formal notation for specification construction; a three-step ap-proach to requirements acquisition and system design; specification-based inspection and testing methods for detecting errors in both specifications and programs, and a set of tools to support modeling and verification. The Modeling, Simulation and Veri-fication Language (MSVL) is a parallel programming language. Its supporting toolkit MSV has been developed to enable us to model, simulate and verify a system in a formal manner. Following the success of previous SOFL+MSVL workshops, this workshop aims to continuously promote the development and combinations of the SOFL formal engineering method and the formal method MSVL, as well as the appli-cations of their fundamental principles and specific techniques to developing other formal engineering techniques. The workshop attracted 24 submissions on formal modeling, formal verification, model checking, metamorphic testing, natural language processing, and geometric modeling. Each submission is rigorously reviewed by two or more PC members on the basis of technical quality, relevance, significance, and clarity, and 13 papers were accepted for publication in the workshop proceedings. The acceptance rate is 54%., Springer, 2021, 2021, Scholarly Book, Joint work, English, Jinyun Xue, Fumiko Nagoya, Shaoying Liu, Zhenhua Duan, ISBN 978-3-030-77473-8, 204, 204

Invited Lecture, Oral Presentation, Poster Presentation

  1. Formal Engineering Methods: Bridging Formal Methods and Software Engineering, Shaoying Liu, The 5th World Symposium on Software Engineering (WSSE 2023), 2023/09/22, With Invitation, English, Tokyo
  2. Formal Engineering Methods: Bridging Formal Methods and Software Engineering, Shaoying Liu, Tokyo IEEE Chapter, 2023/06/23, With Invitation, Japanese, IEEE Japan Council, Tokyo
  3. Agile Formal Engineering Method for High Productivity and Reliability, Shaoying Liu, The 13th International Conference on Software Technology and Engineering (ICSTE 2023), 2023/10/27, With Invitation, English, Osaka, Japan
    Related URL
  4. Specification-Based Fault Prevention and Detection for Software Quality Assurance, Shaoying Liu, 2022 10th International Conference on Information and Education Technology (ICIET 2022), 2022/04/09, With Invitation, English, ICIET Steering Committee, Matsue City
  5. Agile Formal Engineering Methods for High Productivity and Reliability, Shaoying Liu, 2022 8th International Conference on Computer Technology Applications (ICCTA 2022), 2022/05/17, With Invitation, English, ACM, Vienna, Austria, other
    Related URL
  6. Testing-Based Formal Verification: Promise and Challenges, Shaoying Liu, 2022/09/05, With Invitation, Japanese, IPSJ, Tokyo
    Related URL
  7. Software Fault Prevention and Verification for Human-Machine Pair Programming, Shaoying Liu, The 29th Workshop on Foundation of Software Engineering (FOSE 2022), 2022/11/10, With Invitation, English, Japan Society for Software Science and Technology, Matsue City, Shimane
    Related URL
  8. The Role of Mathematics in Software Engineering, Shaoying Liu, CFMAI 2022: 2022 International Conference on Frontiers of Mathematics and Artificial Intelligence, 2022/12/02, With Invitation, English, Southwest Jiaotong University, Beijing, China
    Related URL
  9. A Systematic Method for Identifying Safety-Related Faults in Formal Specifications using FTA, Wen Jiang, Shaoying Liu, Ai Liu, IEICE Tech. Rep, 2021/10/22, Without Invitation, English, online
    Related URL
  10. Adversarial Attack against COVID-19 CT Images Deep Learning System, Yang Li, Ai Liu, Shaoying Liu, IEICE Tech. Rep, 2021/10/22, Without Invitation, English, online
  11. Testing-Based Formal Verification for Software Quality Assurance and Cost Reduction, Shaoying Liu, 2022 The 2nd IEEE International Conference on Information Communication and Software Engineering (ICICSE 2022), 2022/03/18, With Invitation, English, IEEE, Chongqing, China
    Related URL
  12. DevFemOps: Enhancing Maintainability based on Microservices using Formal Engineering Methods, D206171, Tetsuo Fukuzaki, Shaoying Liu, IEEE International Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement (FPDRE) at QRS 2021, 2021/12/08, Without Invitation, English, IEEE International Conference QRS 2021, Hainan, China
    Related URL
  13. TBEM: Testing-based GPU-Memory Consumption Estimation for Deep Learning, Haiyi Liu, Shaoying Liu, Ai Liu, Chenglong Wen, IEEE International Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement (FPDRE) at QRS 2021, 2021/12/08, Without Invitation, English, IEEE International Conference QRS 2021, Hainan, China
    Related URL
  14. A Framework for Modeling and Detecting Security Vulnerabilities in Human-Machine Pair Programming, Pingyan Wang, Pingyan Wang, Shaoying Liu, Ai Liu, IEEE International Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement (FPDRE) at QRS 2021, 2021/12/08, Without Invitation, English, IEEE International Conference QRS 2021, Hainan, China
    Related URL
  15. Testing-Based Formal Verification for Software Quality Assurance and Cost Reduction, Shaoying Liu, IPSJ/SIGSE Software Engineering Symposium(SES2021), 2021/09/08, With Invitation, Japanese, IPSJ
  16. Human-Machine Pair Programming for Future Software Engineering, Shaoying Liu, 2021/06/02, With Invitation, Japanese
  17. A Formal Approach to Secure Design of RESTful web APIs using SOFL, Busalire Emeka, Busalire Emeka, Soichiro Hidaka, Shaoying Liu, 10th International Workshop on SOFL+MSVL for Reliability and Security (SOFL+MSVL 2020), 2021/03/01, Without Invitation, English, SOFL+MSVL 2020 organizing committee, Singapore
  18. SMT-Based Theorem Verification for Testing-Based Formal Verification, Kenta Sugai, Hiroshi Hosobe, Shaoying Liu, 2021 10th International Conference on Software and Computer Applications (ICSCA 2021), 2021/02/23, Without Invitation, English, ICSCA 2021 Organization Committee, Kuala Lumpur, Malaysia, Testing-based formal verification with symbolic execution (TBFV-SE) checks whether programs correctly implement their formal specification. Given a formal specification and a program, it first derives a theorem expressing the correctness property of the executed program paths and then formally verify the validity of the theorem. However, such theorems still need to be verified manually due to the lack of a tool support for dealing with expressions involved. In this paper, we propose a method for automatically verifying theorems for TBFV-SE. This method uses an SMT solver to check whether a theorem is valid. For this purpose, the method converts the conditions in the theorems written in the SOFL specification language into appropriate constraints that are supported by the SMT solver. We present a tool to support the method, and present two case studies to demonstrate how the tool works in the context of Java programs and SOFL specifications.
    Related URL
  19. Testing-Based Formal Verification for Software Quality Assurance and Cost Reduction, Shaoying Liu, 2020/07/11, With Invitation, English, Testing and formal verification are two important means for software verification and validation, but they suffer from critical challenges. Testing shows the presence of bugs but never their absence. Formal verification can show the correctness for programs but not for incorrect programs. Unfortunately, the very reality in software development is that a newly developed system always contains bugs and cannot be correct in the beginning. How to formally prove the correctness of programs in a cost-effective manner is still a challenge. In this talk, after briefly discussing the characteristics and challenges of current verification and validation approaches, a new approach, known as testing-based formal verification (TBFV), will be introduced. TBFV results from an appropriate integration of formal specification-based testing and Hoare logic for proving program correctness. It is a rigorous gray-box testing approach that takes both the specification and the program structure into account. The most important benefit of TBFV is that it can be applied automatically to ensure the correctness or high reliability of programs.
  20. Specification-Based Fault Prevention and Detection for Reliability and Security, Shaoying Liu, The 3rd International Conference on Frontiers in Cyber Security (FCS 2020), 2020/12/17, With Invitation, English, FCS 2020 Steering Committee and Tianjin University, Tianjin, China, The reliability and security of cyber systems are considerably dependent on the quality of software design and verification. In this talk, I will introduce an agile formal engineering method for software development called Agile-SOFL. The method reflects the latest development in Software Engineering and is characterized by emphasizing a specification-based agile programming paradigm. A three-step hybrid specification technique is used for fault prevention in defining both functional and security requirements. A specification-based testing approach is used to facilitate test-driven development and verification of programs. Future development of Agile-SOFL requires several challenging issues to be addressed, and I will briefly explain them at the end of this talk.
    Related URL
  21. Human-Machine Pair Programming: An Intelligent and Automated Approach for Software Productivity and Reliability, Shaoying Liu, International Symposium on System and Software (ISSSR 2020), 2020/10/24, With Invitation, English, ISSSR Steering Committee, Chengdu, China, Pair programming is one of the promising techniques advocated in agile development paradigm, but it tends to be more costly than one person-based programming and to lack a rigorous principle for governing the cooperation of the two programmers. In our recent work on Agile Formal Engineering Methods, we put forward a novel technique called Software Construction Monitoring and Predicting (SCMP) to study an intelligent and automatic approach to human-machine pair programming (HMPP). Its aim is to automatically, dynamically monitor the process of software construction for fault detection and to predict the possible future contents of the software towards its error- free completion based on existing programming experiences and knowledge. This research field is still in its beginning and there are many challenging issues to be addressed. In this talk, I will first discuss the theoretical foundation and frameworks for Software Construction Monitoring and Predicting (SCMP) for HMPP. I will then discuss with examples how it can be applied to support specification construction and program construction, respectively. Finally, I will talk about some challenging issues to be addressed in the future.
    Related URL
  22. A Fault Localization Approach Derived From Testing-based Formal Verification, Rong Wang and Shaoying Liu, Rong Wang, Shaoying Liu, Yuji Sato, The 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020), 2021/03/04, Without Invitation, English, ICECCS Steering Committee and National University of Singapore, Singapore, Symbolic execution is a powerful technique for automating software testing to detect many types of errors like memory errors and assertion violations. However, it encounters the problem of path explosion, and by using only assertions it still lacks the capability to go deep into checking the functional correctness of a path based on the formal specifications. To address these problems, we propose a specification-based incremental testing method with symbolic execution, called SIT-SE, providing a much more rigorous way to automatically check the functional correctness of all the discovered program paths, by introducing theorems (instead of assertions) for path correctness and Branch Sequence Coverage (BSC) algorithm for guiding a moderate path exploration. The proposed method carefully treats the relationship between a path condition and specifications in a theorem to restrict the monotonous path exploration, whereas traditional concolic testing methods roughly using one test data to determine the path correctness by assertions during long path searching. We use a classic case to demonstrate how the method works, and conduct an experiment to evaluate the performance of both proposed method and the commonly used well-known concolic testing tool KLEE. The experimental results show the effectiveness of our method, and the method SIT-SE outperforms KLEE on detecting faulty paths based on the specifications.
  23. Range Partition Testing: Principle and Technique, Shaoying Liu, 2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C), 2020/12/11, Without Invitation, English, IEEE Reliability Society, Macau, Domain partition testing is a well known approach for software testing but it does not necessarily ensure that all of the desired outputs and the related services are tested. It also has a limitation in dealing with incomplete specifications whose domain is only a subset of the desired one. In this paper, we propose a Range Partition Testing as an alternative approach to testing software systems. We discuss the principle of the approach and how it can be applied to formal specifications for automatic test case generation. Our work is expected to set up a foundation for further developments of the approach and for expanding the approach to support specification-based reliability and bug predictions in the future., published, Paper
    Related URL, Attached File's URL

External Funds

Acceptance Results of Competitive Funds

  1. 2021/06, 2022/03

Social Activities

Organizing Academic Conferences, etc.

  1. The 24th International Conference on Formal Engineering Methods, Steering Committee member, 2023/11, 2023/11
    Permalink
  2. The 10th International Conference on Dependable Systems and Their Applications, PC member, 2023/08, 2023/08
    Permalink
  3. 26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), 2022/03, 2022/03
    Permalink
  4. 11th International workshop on SOFL+MSVL for Reliability (SOFL+MSVL 2022) and Security, 2022/10, 2022/10
    Permalink
  5. (6) 23rd International Conference on Formal Engineering Methods (ICFEM 2022), Steering Committee Member, 2022/10, 2022/10
    Permalink
  6. QRS 2022 Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement, 2022/12, 2022/12
    Permalink
  7. (4) 22nd IEEE International Conference on Software Quality, Reliability, and Security (QRS 2022), PC member, 2022/12, 2022/12
    Permalink
  8. 9th International Conference on Dependable Systems and Their Applications (DSA 2022), PC member, 2022/08, 2022/08
    Permalink
  9. The 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2021), 2022/03, 2022/03
  10. 15th International Conference on Theoretical Aspects of Software Engineering (TASE 2021), PC member, 2021/08, 2021/08
    Permalink
  11. The 22nd International Conference on Formal Engineering Methods, Steering Committee Member, 2020/01, 2021/03
    Permalink
  12. QRS 2021, PC Member, 2021/12, 2021/12
  13. The 26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), General Chair, 2022/03, 2022/03
    Permalink
  14. QRS 2021 Workshop on Fault Prediction, Prevention, Detection, and Reliability Enhancement (FPDRE), Chair, 2021/12, 2021/12
  15. The 7th International Symposium on System and Software Reliability (ISSSR 2021), General Chair, 2021/09, 2021/09
  16. The 10th International Workshop on SOFL+MSVL for Reliability and Security (SOFL+MSVL 2020), SOFL+MSVL 2020 General Chair, 2021/03, 2021/03
    Permalink
  17. The 20th International Conference on Quality, Reliability and Security (QRS 2020), QRS 2020 General Chair, 2012/06
    Permalink
  18. 2020 International Conference on Engineering of Complex Computer Systems (ICECCS 2020), ICECCS Steering Committee Chair, 2019/12, 2022/03
    Permalink

History as Peer Reviews of Academic Papers

  1. 2021, IEEE Transactions on Software Engineering, Others, Reviewer, 1
  2. 2020, The Computer Journal, Others, Reviewer, 1
  3. 2021, Innovation of Systems and Software Engineering, Editor, Associate Editor
  4. 2021, IEEE Transactions on Reliability, Editor, Associate Editor
  5. 2020, IET Software, Others, Guest Editor for the Special Section on Software Engineering Track of ACM SAC 2021
  6. 2020, Mathematics, Others, Invited Editor for a Special Issue on Mathematics in Software Reliability and Quality Assurance
  7. 2020, Innovations in Systems and Software Engineering, Editor, Associate Editor
  8. 2020, IEEE Transactions on Reliability, Editor, Associate Editor
  9. 2020, International Journal of Software Engineering and Knowledge Engineering, Others, Reviewer, 3