Publications(January 2002 - December 2002)
- 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.
- 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.
- 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.
- 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.
- 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
- 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.
- 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.
- 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.
- 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.
- 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.