| Refereed Publications
- Shaoying Liu and Satoshi Kagiyama, "A Tool for
Automatic Transformation between SOFL Class Specifications
and UML Diagrams'', Proceedings of 2006 Software Engineering
and Applications (SEA2006), ACTA Press, Dallas, Texas,
USA, November 13-15, 2006, pp.105-110.
Abstract - The successful
application of formal specification techniques in practice
requires support for improving the readability and understandability
of formal specifications. In this paper, we describe our
latest work on the construction of a software tool to
support an automatic transformation between SOFL class
specifications and UML diagrams. It includes the transformations
from SOFL class specifications to UML class diagrams,
from SOFL explicit specifications to UML activity diagrams,
and from UML class diagrams to SOFL class specifications.
We also present a case study using the tool for an ATM
system to evaluate the performance of the tool.
- Shaoying Liu, "Scenario-Preserved Refinement: a
Small Proposal for an Important Problem", 1st International
Workshop on Asian Working Conference on Verified Software
(AWCVS06), UNU-IIST Report No. 347, Macau, Oct. 29-31,
2006, pp. 1-10.
Abstract - Morgan's
strengthen postcondition law allows a feasible specification
to be refined into an infeasible one and does not allow
the refinement of an infeasible partial specification
into a feasible total specification, but this is likely
to incur frustration and high cost for software development
and may not be effective to support incremental development
in practice. On the basis of an analysis of this important
problem with an example, we propose an improvement of
the refinement law to ensure that the underlying principle
of the refinement calculus effectively supports the incremental
software development paradigm and successful refinements
will definitely lead to correct, terminating code. The
proposed refinement law is also expected to effectively
help to reduce the risk of frustration and high cost in
- Yuting Chen, Shaoying Liu, Fumiko Nagoya, "A Tool-Supported
Review Approach to Detecting Structural Consistency Violations'',
Proceedings of 11th IEEE International Conference on Engineering
of Complex Computer Systems (ICEECS 2006), IEEE Computer
Society Press, Stanford University, CA, USA, 14-18 August
2006. pp. 121-130.
Abstract - The application
of specification-based program verification techniques
(e.g., testing, review, and proof) faces strong challenges
in practice when the gap between the structure of a specification
and that of its program is large. In this paper we describe
a tool-supported review approach to detecting structural
consistency violations by introducing the review method,
discuss the design and implementation of the tool, and
present a case study to assess the effectiveness of the
tool and identify points for further improvement.
- Fumiko Nagoya, Yuting Chen, Shaoying Liu, "An Empirical
Study on a Specification-Based Program Review Approach",
2006 International Conference on Dependability
of Computer Systems (DepCoS-RELCOMEX 2006), IEEE Computer
Society Press, Szklarska, Poreba, Poland, 24-28 May 2006,
Abstract - Program review
is an effective technique for detecting faults in software
systems by reading and analyzing code. However, challenges
still remain in providing systematic and rigorous review
techniques. We have recently developed a rigorous review
approach and a software tool that provide reviewers with
support in analyzing whether a program accurately implements
the functions and properties defined in its specification.
In this paper, we describe an empirical study of the application
of our review approach and tool to a software system for
automated teller machines (ATMs). We also discuss the
effectiveness of the review approach, as well as some
weaknesses, based on the results of our study, and potential
solutions to the problems encountered during the study.
- Shaoying Liu, "Formal Methods and Their Developments
toward Practical Applications", Keynote Speech, Japanese
Software Engineers Association Forum on Formal Methods,
Nov. 28, 2006.
- Shaoying Liu, "Can Formal Methods be Applied in
Industry?", (Position Paper) Japanese Software Symposium,
Kumamoto, Japan, July 19-21, 2006.