Last Updated :2021/04/06

Affiliations, Positions
Graduate School of Advanced Science and Engineering, Professor
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, and member of JSSST and IPSJ.

Basic Information

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
  • The University of Manchester

Educational Activity

Course in Charge

  1. 2021, Liberal Arts Education Program1, 1Term, Introductory Seminar for First-Year Students
  2. 2021, Graduate Education (Master's Program) , 4Term, Formal Engineering Methods for Software Development
  3. 2021, Graduate Education (Master's Program) , 1Term, Special Exercises on Informatics and Data Science A
  4. 2021, Graduate Education (Master's Program) , 2Term, Special Exercises on Informatics and Data Science A
  5. 2021, Graduate Education (Master's Program) , 3Term, Special Exercises on Informatics and Data Science B
  6. 2021, Graduate Education (Master's Program) , 4Term, Special Exercises on Informatics and Data Science B
  7. 2021, Graduate Education (Master's Program) , Academic Year, Special Study on Informatics and Data Science
  8. 2021, Graduate Education (Doctoral Program) , Academic Year, Special Study on Informatics and Data Science

Research Activities

Academic Papers

  1. Mutated Specification-based Test Data Generation with Genetic Algorithm, Mathematics, 2021
  2. ★, Rigorous Code Review by Reverse Engineering, Information and Software Technology, 2021
  3. ★, Automatic Test Case and Test Oracle Generation based on Functional Scenarios in Formal Specifications for Conformance Testing, IEEE Transactions on Software Engineering, 20200604
  4. BAGKD: A Batch Authentication and Group Key Distribution Protocol for VANETs, IEEE COMMUNICATIONS MAGAZINE, 58(7), 35-41, 202007

Invited Lecture, Oral Presentation, Poster Presentation

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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

Social Activities

Organizing Academic Conferences, etc.

  1. The 10th International Workshop on SOFL+MSVL for Reliability and Security (SOFL+MSVL 2020), SOFL+MSVL 2020 General Chair, 2103/01
  2. The 20th International Conference on Quality, Reliability and Security (QRS 2020), QRS 2020 General Chair, 2012/06
  3. 2020 International Conference on Engineering of Complex Computer Systems (ICECCS 2020), ICECCS Steering Committee Chair, 1912/01, 2012/30

History as Peer Reviews of Academic Papers

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