| |
|
||Top
page
| Profile | Research| Teaching|
Laboratory information
||
|
Research Interests |
|
(1)
Formal Engineering Methods for Software Development
|
| Formal
Engineering Methods are a bridge between formal methods and their applications in software
engineering. They form an area of research on how to integrate formal methods
into practical software engineering process to enhance the rigor of commonly
used development methods, the comprehensibility of documentation for communication,
and the tool supportability for software productivity and quality. Liu's
particular interests are on the SOFL specification language, method, and support environment. SOFL, standing
for Structured Object-Oriented Formal Language, has been developed by Liu
based on his Ph.,D research at the University of Manchester, U.K. during
1989 - 1992, in collaboration with excellent researchers from USA, UK,
Australia, Singapore, and Japan on several projects funded by the Ministry
of Education, Culture, Sports, Science and Technology of Japan during the
period of 1996 - 2001. As a language, SOFL results from the integration
of Data Flow Diagrams, Petri Nets, and VDM-SL.. Data Flow Diagrams are
an intuitive notation for expressing the overall architecture of a system;
Petri Nets are used to provide an operational semantics for the Data Flow
Diagrams; and VDM-SL, with certain syntactical revision and extension,
is employed to specify the behavior of processes occurring in the related
formalized Data Flow Diagrams. To achieve information hiding, specification
reusability, and polymorphism in the detailed design, classes are used
to model modules, data flows, data stores, and composite data types. As
a method, SOFL emphasizes the three-step approach,
i.e., informal, semi-formal, and formal specifications,
for requirements analysis and system design,
and the rigorous reviews,
inspection, and testing
as techniques for verifying and validating specifications
and programs. |
|
|
| |
| (2)
Intelligent Software Engineering Environments (ISEE) |
| Liu believes that the radical solution
to the problem of software crisis is to provide a software
engineering environment that takes care of all the process
management and control issues, and guides developers
intelligently to develop their systems step by step.
Within such an environment, developers are efficiently
supported to concentrate only on the tasks which computer
cannot perform at all. Such an environment should also
be able to learn from previous experience in building
similar systems and to make use of the existing knowledge
from previous experience in the development of new systems.
In the exciting internet era, more and more software
systems are developed by a team or teams, possibly located
in several different places in the world, supporting
distributed software engineering over internet becomes
more and more important and necessary. Liu's another
research interest is to develop internet-based
intelligent software engineering environments for distributed software engineering based on service-oriented computing.. |
|
|
| |
| (3)
Dependable Systems |
| Dependable
systems must have high reliability,
availability, safety,
security, and maintainability. Such systems have become more and more involved in our daily life and
their failures are likely to cause catastrophic damages to human life,
important properties, or high cost of the system providers. Railway control
systems, airplane control systems, nuclear plant control systems, intelligent
transport systems (ITS), and banking systems are typical examples of dependable
systems. Liu's interest in this area is to develop theories, methods, and
software tools to support the application of formal engineering methods,
in particular SOFL, to the development of dependable systems, including
Cyber-Physical Systems, ITS,
Financial Systems, Medicare
Systems, and Information
Systems. |
|
|
|
|
|
SOFL
|
| SOFL offers a specification
language, method, and systematic process for the development
of software systems.
SOFL = Specification Language +
Method + Software Process Model
As a language, SOFL is an integration of Data Flow
Diagrams, Petri Nets, and VDM-SL. Data Flow Diagram
provides an intuitive notation for expressing the
overall architecture of a system; Petri Nets are used
to provide an operational semantics for the Data Flow
Diagrams; and VDM-SL with certain syntactical revision
and extension is employed to specify the behavior
of processes occurring in the related formalized Data
Flow Diagrams. To achieve information hiding, specification
reusability, and polymorphism in the detailed design,
classes are used to model modules, data stores, and
composite data types.
The following figure shows a general
structure of SOFL specifications: 
As a method, SOFL emphasizes the three-step
approach, i.e., informal, semi-formal, and formal
specifications, to constructing system specifications
in a structured manner (including requirements, and
abstract design specifications) and transformation
from a structured abstract design into an object-oriented
detailed design and then implementation (program).
Furthermore, it also offers effective and systematic
rigorous review and testing techniques for verifying
and validating specifications and programs.
SOFL also provides a software process model that supports
a systematic way to develop large-scale and complex
systems. The major features of the process model include
three: (1) using informal and semi-formal specifications
for user requirements, while adopting formal specification
for abstract design; (2) emphasizing evolution
for the development of informal, semi-formal, and
formal abstract design specifications, and refinement
for the development of detailed design and implementation;
and (3) employing rigorous review and testing to verify
and validate specifications and programs.
The following figure shows the SOFL
software process model:
|
|
|
|
|
|
|
SOFL
Tools |
| Five
prototype tools for SOFL have been developed. One is the SOFL
specification creator that supports the construction of quality
specifications. Figure 1 shows a snapshot of the tool. The
second tool supports specification animation, as illustrated
in Figure 2. The third tool supports specification review
using the property-based review approach and the Review Task
Tree (RTT) notation. Figure 3 shows the GUI of the tool. The
fourth tool supports specification-based program inspection,
as illustrated in Figure 4. The fifth tool supports specification
testing for consistency and a snapshot of the tool is given
in Figure 5.
Figure 1: A snapshot of the SOFL specification
creator
Figure 2: SOFL specification animator
Figure 3: SOFL Rigorous Review Method Tool
(RRMT)
Figure 4: SOFL specification-based program
review (inspection) tool
Fogure 5: SOFL specification testing tool
|
|
|
|
|
|
Ongoing Research Projects
|
|
|
|
| |
| (
1 ) Requirements Engineering with Formal Methods |
| This research aims to develop effective
methods and software tools to support requirements acquisition
using formal specification techniques. The essential problem
to resolve is how to use formal specification languages so
that all the potential user requirements can be discovered
and documented consistently, and how such a process can be
effectively supported. |
|
| |
| (
2 ) Automated Rigorous Reviews of Formal Specifications
|
| The goal of this research is first to
establish an effective, rigorous review technique based on
formal analysis for reviews of formal specifications written
in SOFL and then to build a software tool to assist human
reviewers to apply the technique to review their specifications.
The tool is intended to support four activities: (1) derivation
of review targets; (2) construction of review tasks in a compositional
manner; (3) performance of reviews; and (4) analysis of review
results. |
|
| |
| (
3 ) Specification Testing |
| In this research we are interested in
building testing methods, criteria, and software tools to
support testing of formal specifications, including both implicit
specifications (usually written using pre and postconditions)
and explicit specifications. Since implicit specifications
are not executable in general, the output of an operation
may not be obtained by executing specifications. For this
reason, the traditional program testing techniques need to
be modified to support specification testing. Note that specification
testing is different from specification-based testing in the
sense that the former aims to test specifications, while the
latter tries to test their implementations (programs). |
|
| |
| (
4 ) Automatic Test Case Generation Based on Both Program Structure
and Formal Specification |
| Traditional automatic test case generation
approach faces a challenge in test results analysis, because
the intention of the generated test cases and the expected
results can hardly be understood by human testers. Taking
only specification into account, test case generation, on
the other hand, is not sufficient in detecting bugs related
to program structures. In this research we attempt to establish
a method for automatic test case generation based on both
program structures and the functional requirements in specifications,
and then build software tools to support the use of the method. |
|
| |
| (
5 ) Specification-Based Rigorous Inspection of Programs |
| Given a specification S and its implementation
P, how to inspect P so that we can become confident that P
implements S correctly? This research aims to establish an
automated inspection method to perform the task. The method
is intended to take into account the relation between the
functional requirements in the specification and the implementation
paths in the program. |
|
| |
| (
6 ) Visual Specification Animation |
| Before implementing a specification S,
it is important to understand the potential behaviors of the
final program system and whether it satisfies the user's conception
of requirements. In particular, our interest is in visual
animation techniques that allow human to see visual executions
of the specification in both computational context and virtual
reality of the application domain. |
|
| |
| (
7 ) Automatic Transformation from Formal Specifications to
Natural Language Description for Understanding and Documentation
Management |
| An important way to help human understand
formal specifications and to save efforts in documentation
is to automatically produce well-organized and comprehensible
natural language descriptions from the formal descriptions.
The purpose of this work is to establish systematic rules
for transforming formal specifications into natural language
descriptions. The difficulty of this research is not at the
possibility of achieving such a transformation, but at the
possibility of producing good quality informal descriptions
of the formal specifications. |
|
| |
| (
8 ) Automated Software Transformation from Formal Specifications
into Programs |
| Given a formal specification S, how can
we automatically transform it into a program P that satisfies
S in accordance with the well-established refinement rules?
If S is expressed using first order logic, it is extremely
difficult to automatically generate a satisfactory program
in general. However, an interleave process can be adopted
to perform the transformation, but the key point is how to
support the interleave process so that the human developer
interacting with the computer transformer (a program system
for transformation) easily understand what to do to help the
transformation process. One possible way is to allow the developer
only to work on the initial specification level rather than
on every refined intermediate specification level. The target
of this research is to develop effective techniques to support
the interleave approach. |
|
| |
| (
9 ) Formal Engineering Methods for Software Process |
| This research aims to apply the latest
formal specification and rigorous verification techniques
to the description, consistency checking, control, and predication
of software processes. Specifically, we advocate the use of
SOFL as the specification language to describe software processes,
because CDFDs (Condition Data Flow Diagrams) can provide a
graphical but rigorous representation of an overall workflow
for a software process and modules give a textual and precise
definition for each resource (e.g., human, software, computers,
budget, time) and activity (e.g., requirements analysis, abstract
design, risk analysis, planning, detailed design, implementation).
Furthermore, the rigorous review, testing, and simulation
techniques can be used to check the consistency among the
resources and activities in a software process, to predicate
the potential development of the process, and to control the
real progress and deal with exceptional situations during
the performance of the software process. The final goal of
this research is to build effective software tools to rigorously
support software processes in every possible aspect. |
|
| |
| (
10 ) Construction of an Intelligent Software Engineering Environment
for SOFL |
| A SOFL environment is composed of inter-related
tools that support the use of SOFL in the entire software
development process, while the intelligence of such an environment
is reflected in its capability of being able to guide developers
to develop their systems step by step. It may include GUI,
syntax-oriented editor, type checker, review tools, testing
tools, documentation tools, and tools for software process
plan, management, cost estimation, and control. The overall
goal of this research is to build such an environment for
SOFL with good usability. |
|
| |
| (
11 ) Computer-Aided Formalization of Semi-Formal Specifications |
| This research aims to develop techniques
that support the transformation from semi-formal functional
requirements specifications into formal design specifications.
It is usually difficult to achieve a complete automation of
such transformations, but a computer-aided approach can be
possible and useful. |
|
| |
| (
12 ) Dependable Systems Development with SOFL |
| The goal of this research is to investigate
systematic methods and techniques for applying SOFL to develop
dependable systems that require high reliability, safety,
and security, such as ITS (Intelligent Transport Systems),
Medicare Systems, and Banking Systems. In many dependable
systems, reliability, safety, and security may affect with
each other, and it is important to achieve the best balance
among them. To increase the productivity and reliability of
dependable systems development process, we are also interested
in building effective software tools to support the construction
and verification of dependable systems. |
|
| |
| (
13 ) Internet-Based Approach to Supporting Distributed Software
Engineering |
| With the progress of globalization, more
and more software projects are conducted in a distributed
manner. To support distributed software engineering, we need
techniques and software tools to support communications, discussions,
documentation management, reviews, testing, and so on. In
this research we attempt to develop effective techniques and
tools for this purpose. |
|
| |
| (
14 ) Intelligent Homepage Evolution Systems |
| Homepages often need updating to provide
accurate, consistent, and complete information and/or functionality
for situations changed. This research aims to provide effective
methods and software tools to automatically identify the data
items, including texts, pictures, and audio objects, and to
update them properly in accordance with changed situations
of the associated organization or individuals. For example,
the number of a researcher's publications may increase as
time passes by, but the publication list of his or her homepage
may not be updated. An automatic evolution software tool may
help to update the publication list based on his or her new
publications contained in some online proceedings or journals.
Also, when a homepage needs updating, an intelligent evolution
may automatically request the author to provide new information
for updating data items no longer appropriate in his or her
homepages. |
|
|
Funded Research Projects (1995 ~ Present)
|
|
|
(
1 )
|
Automatic Transformation of Formal Specifications (funded
by Hiroshima City University) (1995) |
|
(
2 )
|
Formal
Methods and Intelligent Software Engineering Environments
(funded by the Ministry of Education, Culture, Sports, Science
and Technology of Japan) (1996-1998) |
|
(
3 )
|
Safety-Critical
Systems Development Using Formal Methods (funded by Hiroshima
City University) (1996-1998) |
|
(
4 )
|
Application of Formal Methods to Railway Systems (funded by
Mitsubishi Research Institute in Hyogo pref ) (1997-1999) |
|
(
5 )
|
Software
Evolution (funded by the Ministry of Education, Culture, Sports,
Science and Technology of Japan) (1998-2000) |
|
(
6 )
|
Formal
Engineering Methods for Software Development (funded by the
Ministry of Education, Culture, Sports, Science and Technology
of Japan) (1999-2002) |
|
(
7 )
|
Rigorous
Verification Techniques for Formal Specifications (funded
by the Ministry of Education, Culture, Sports, Science and
Technology of Japan) (1999-2002) |
| (
8 ) |
Research on Automation
of Rigorous Reviews of Formal Specifications and Programs
(funded by the Ministry of Education, Culture,
Sports, Science and Technology of Japan) (2002-2005) |
| (
9 ) |
Research on Formal
Specification-Based Software Testing (funded by the Ministry
of Education, Culture,
Sports, Science and Technology of Japan) (2006-2008) |
|
| ( 10 ) |
Research on Application of Formal Methods (funded by The Nippon Signal Co. Ltd.) (2007-2009) |
| ( 11 ) |
Research on Specification-Based Automatic Testing Techniques (funded by
NII) (2008-2010) |
|
|
