Annals of Faculty of Computer and Information Sciences, Hosei University
Department of computer science <<Previous Next>>
HOME >> No.3 CONTENTS >> Shaoying LIU
Professor
Shaoying LIU
Publications(January 2002 - December 2002)
  1. Shaoying Liu, "Developing Quality Software Systems Using the SOFL Formal Engineering Method", Proceedings of 4th International Conference on Formal Engineering Methods (ICFEM2002), LNCS2495 Springer-Verlag, Shanghai, China, October 21-25, 2002, pp.3-19 (keynote speech paper).
    Abstract - Formal Engineering Methods are a bridge from Formal Methods to industrial applications. Inthis paper I describe the relation between formal engineering methods and formal methods, and present a specific formal engineering method SOFL (Structured Object-Oriented Formal Language) for developing quality software systems. I explain how SOFL can be applied in practice through examples.
  2. Shaoying Liu, "Capturing Complete and Accurate Requirements by Refinement", Proceedings of 8th IEEE International Conference on Engineering of Complex Computer Systems, IEEE Computer Society Press, Greenbelt, Maryland, USA, December 2-4, 2002, pp. 57-67.
    Abstract - Complete and accurate functional requirements are the foundation for valid specification refinement and correctness verification of implemented software systems when they are developed with a formal method. However, capturing quality requirements is a difficult task, and there is a lack of well-defined and effective technique that solves the problem as well. In this paper we argue that the refinement technique used in conventional formal methods for transforming formal specifications into programs is actually an effective technique for capturing the functional requirements. We define the completeness of formal specifications and explain by examples how it can be achieved.
  3. Shaoying Liu, "A Simulation Approach to Verification and Validation of Formal Specifications", Proceedings of First International Conference on Cyber World: Theory and Practice, IEEE Computer Society Press, November 6-8, 2002, pp. 113-120.
    Abstract - Specification simulation is an approach to verifying and validating specifications by well-selected sample data. In this paper we put forward a technique for simulation of formal specifications in order to detect potential faults and validate their desired functions. The important benefit of this technique is to allow us to simulate implicit specifications, which are usually defined with a pair of pre and postconditions and may not be executable. We discuss the ways of simulation case generation, evaluation of logical expressions, and simulation result analysis, and demonstrate how they are applied in practice by examples.
  4. Shaoying Liu, "A Rigorous Approach to Reviewing Formal Specifications", Proceedings of 27th IEEE/NASA Software Engineering Workshop, IEEE Computer Society Press, December 4-6, 2002, 7 pages.
    Abstract - I put forward a new approach to rigorously reviewing formal specifications to ensure their internal consistency and validity. This approach includes four steps: (1) deriving properties as review targets based on the syntax and semantics of the specification, (2) building a review task tree to present all the necessary review tasks for each property, (3) carrying out reviews based on the review task tree, and (4) analyzing the review results to determine whether faults are detected or not. I apply this technique to the SOFL specification language, which is an integrated formalism of VDM, Petri Nets, and Data Flow Diagrams to discuss how each step is performed.
  5. Shaoying Liu, "Formal Engineering Methods for Information Systems Development", Proceedings of Second International Conference on INFORMATION (INFORMATION2002), Beijing, July 24-27, 2002, pp. 148-154 (invited paper).
    Abstract - With the rapid growing of deployment of information systems in almost every domain of our society, their reliability and efficiency have become one of our greatest concerns. Since modern information systems become more and more complex, their developments have become so difficult that the delivery of final products often falls behind the schedule and the cost often exceeds the budget. To tackle these problems effectively, we have been working on the integration of mathematical notation and commonly used comprehensible notation over last ten years to design the SOFL (Structured Object-oriented Formal Language) specification language and method for information systems development. As a specification language, SOFL integrates VDM-SL, Data Flow Diagrams, and Petri nets to provide an intuitive, rigorous, and comprehensible formal notation for specification. As a method, it combines Structured Methods and Object-Oriented Methods, and advocates an evolutionary approach to constructing specifications; it integrates the idea of formal proof and commonly used verification and validation techniques, such as testing and reviews, to offer rigorous but practical verification techniques. In this paper I present a three-step approach to constructing formal specifications for information systems, and demonstrate its effectiveness with a case study.
  6. Shaoying Liu, Jin Song Dong, "Extending SOFL to Support Both Top-Down and Bottom-Up Approaches", Proceedings of 2002 IEEE International Conference on Systems, Man, and Cybernetics (SMC 2002), IEEE Computer Society Press, Hammamet, Tunisia, October 6-9, 2002, WA1Q2.
    Abstract - This paper presents an integrated approach to support both top-down and bottom-up design of software systems by combining UML (Unified Modeling Language) and the Formal Engineering Method SOFL (Structured Object-oriented Formal Language). We demonstrate by examples that the top-down principle used in conventional Structured Design can be effectively utilized to carry out Object-Oriented design that is usually seen as a way to suit bottom-up analysis and design. Furthermore, we also explain how the integrated approach helps to improve the preciseness and understandability of design documentations.
  7. Jin Song Dong, Shaoying Liu, "The Semantics of Extended SOFL", Proceedings of 26th Annual International Software and Application Conference, IEEE Computer Society Press, Oxford, England, 26-29 August 2002, pp. 653 -658.
    Abstract - Recently SOFL (Structured-Object-based-Formal Language) has been extended to a formal object-oriented language and method while keeping its structured features. This extension allows powerful object-oriented reuse mechanisms, such as class inheritance and object composition, to be utilized in the early design phases. This paper presents the semantics for this extended SOFL and further demonstrates the extendibility and reusability of the object-oriented approach to specifying the semantics of computer languages.
  8. Shaoying Liu, "Integrating UML and SOFL for Object-Oriented Design", Proceedings of The Third International Conference on Computer and Information Technology(CIT2002), Aizu-Wakamatsu City, Japan, September 11 - 14, 2002, pp. 92-98.
    Abstract - This paper presents a decompositional approach to object-oriented design of software systems using a notation resulting from combination of UML (Unified Modeling Language) and SOFL (Structured Object-oriented Formal Language). We use examples and case studies to explain how traditioanl Structured Design can be effectively applied to carry out object-oriented design that is usually seen as a way to support bottom-up analysis and design.
  9. Shaoying Liu, "An Approach to Transforming Visual Formal Specifications to Java Programs", Proceedings of The Third International Conference on Computer and Information Technology (CIT2002), Aizu-Wakamatsu City, Japan, September 11 - 14, 2002, pp. 116-123.
    Abstract - Condition Data Flow Diagrams is a formalized notation used in SOFL (Structured Object-Oriented Formal Language) for systems specification. It was developed by integrating conventional Data Flow Diagrams, Petri Nets, and pre-post notation. In this paper we describe a method for transformation of Condition Data Flow Diagrams into Java programs by defining transformation strategy and rules, and discuss their applications with examples.
  10. Shaoying Liu, "A Top-Down Approach to Identifying and Defining Words for Lyee Using Condition Data Flow Diagrams", Proceedings of 2002 Lyee International Workshop (Lyee-W02), IOS international publisher, Paris, France, October 3- 5, 2002, pp. 75-87.
    Abstract - We present a top-down approach to identifying and defining words for the Lyee system using the visual formalism known as Condition Data Flow Diagram used in the SOFL (Structured Object-Oriented Formal Language) formal engineering method. The proposed technique can facilitate the analyst to effectively identify the necessary words as outputs of operations in a structured manner and to represent the relations among words in a visual formalism.

>PAGE TOP