Books

1. Shaoying Liu, Tom Maibaum, and Keijiro Araki (Eds.), “Formal Methods and Software Engineering”, Springer-Verlag, LNCS 5256, ISBN-10 3-540-88193-X, 2008.
   Abstract - Formal engineering methods are intended to offer effective means for integration of formal methods and practical software development technologies in the context of software engineering. Their purpose is to provide effective, rigorous, and systematic techniques for significant improvement of software productivity, quality, and tool supportability. This volume contains the papers presented at ICFEM 2008, held October 27 - 31, 2008 at the Kitakyushu International Conference Center, Kitakyushu-City, Japan. There were 62 submissions, each of which was reviewed by three Program Committee members. The committee decided to accept 20 papers based on their originality, technical contribution, presentation, and relevance to formal engineering methods.

Refereed Publications

1. Shaoying Liu and Yuting Chen, “A Relation-Based Method Combining Functional and Structural Testing for Test Case Generation” Journal of Systems and Software, Elsevier Science Inc. Vol. 81, No. 2, Feb. 2008, pp. 234-248.
   Abstract - Specification-based (or functional) testing enables us to detect errors in the implementation of functions defined in specifications, but since specifications are often incomplete in practice for some reasons (e.g., lack of ideas, no time to write), it is unlikely to be sufficient for testing all parts of corresponding programs. On the other hand, implementation-based (or structural) testing focuses on the examination of program structures, which allows us to test all parts of the programs, but may not be effective to show whether the programs properly implement the corresponding specifications. To perform a comprehensive testing of a program in practice, it is important to adopt both specification-based and implementation-based testing. In this paper we describe a relation-based test method that combines the specification-based and the implementation-based testing approaches. We establish a set of relations for test case generation, illustrate how the method is used with an example, and investigate the effectiveness and weakness of the method through an experiment on testing a software tool system.
2. Yuting Chen, Shaoying Liu, and W. Eric Wong, “A Review Approach to Detecting Violations of Consistency between Specification and Program Structures”, International Journal of Software Engineering and Knowledge Engineering (IJSEKE), World Scientific Publishing Co. Pte. Ltd, 18(8), Dec., 2008.
   Abstract - The application of specification-based program verification techniques (e.g., black-box testing, formal proof) faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. This paper describes a view-based program review approach to addressing these challenges. The essential idea of the approach is first to derive comparable views from specification and program, and then detect and eliminate the violations of structural consistency in the program views on the basis of a set of criteria. We also developed a prototype tool to support the review approach, and conducted a case study to assess the effectiveness of the approach.
3. Shaoying Liu, “Integrating Top-Down and Scenario-Based Methods for Constructing Software Specifications”, In proceedings of 8^th International Conference on Quality Software (QSIC 2008), IEEE Press, Oxford, Aug. 12-13, 2008, pp. 105-113.
   Abstract - How to construct a complete and consistent software specification by construction is an important issue for software quality assurance, but it is still an open problem. The difficulty lies in the fact that the assurance of the completeness needs user's judgments and the specification keeps changing as requirements analysis progresses. To allow the user to easily make such judgments and to reduce chances for creating inconsistencies due to frequent specification modifications, in this paper we describe an intuitive, formal, and expressive specification method that integrates top-down decompositional and scenario-based compositional methods. The decompositional method is used at an informal level with the goal of achieving a complete coverage of the user's functional requirements, while the compositional method is used to precisely define the functionality of each scenario and to construct complex scenarios by composition of simple scenarios in a formal, intuitive language called SOFL. Combination of the decompositional and compositional processes can facilitate the analyst to complete a specification in a hierarchical structure. We present an example to illustrate how the integrated method is used in practice and describe a software support tool for the method.
4. Shaoying Liu, “Utilizing Formalization to Test Programs without Available Source Code”, In proceedings of 8^th International Conference on Quality Software (QSIC 2008), IEEE Press, Oxford, Aug. 12-13, 2008, pp. 216-221.
   Abstract - How to test a program with no available source code is of great importance for software quality assurance in practice, but still remains a challenge. In this paper, we describe a novel approach to tackling this challenge. Its principal idea is first to formalize the informal requirements into formal operation specifications based upon program interface scenarios, and then utilize the specifications as a foundation for test case generation and test result analysis. We discuss how the formal specifications can be achieved and how formalization benefits the testing. In particular, we focus on the issue of how to test whether all functional scenarios defined in a specification are correctly implemented in the program. We present an example of applying the approach to an IC Card system to demonstrate its usage and to analyze its potential capability and challenges in practice.
5. Shaoying Liu, “Teaching Formal Methods in the Context of Software Engineering”, In proceedings of 1^st International Conference on Formal Methods Education and Training (FMET 2008), Kitakyushu City, Japan, Oct. 28, 2008, pp. 1-9.
   Abstract - Formal methods were developed to provide systematic and rigorous techniques for software development, and they must be taught in the context of software engineering. In this paper, we discuss the importance of such a teaching paradigm and describe several specific techniques for teaching formal methods. These techniques have been tested over the last fifteen years in our formal methods education programs for undergraduate and graduate students at universities as well as practitioners at companies. Our experience shows that students can gain confidence in formal methods only when they learn their clear benefits in the context of software engineering.

>PAGE TOP