||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

SOFL Applications
(1) Modeling of a Railway Crossing Controller
This work is an industrial trial of using SOFL to model a railway crossing controller.
(2) Specification and Implementation of a University Information System
This is an application of SOFL to developing an information system conducted by two students for their graduation project.
(3) Modeling of an Online Banking System
An online banking system is modeled using SOFL by a M.Sc student as a small project of the Advanced Software Engineering Course. This work clearly shows how the SOFL three-step approach to construction of formal specifications can be applied.
(4) Experimental Approach to Modeling of an Accounting System
An ITPC student took an experimental approach to using SOFL to model an accounting system. The result of this work has demonstrated the effectiveness of formal specification technique in clarifying ambiguities and discovering correct definitions of data structures and operational functionalities.
(5) Modeling of a Hotel Reservation System
A hotel reservation system based on a real world hotel system has been specified using SOFL. The result of this work has shown the effectiveness of formal specification technique in communication between the developer and customer and in identifying appropriate data objects and operations.
Ongoing Research Projects
( 1 )
Requirements Engineering with Formal Methods
( 2 )
Automated Rigorous Reviews of Formal Specifications
( 3 )
Specification Testing
( 4 )
Automatic Test Case Generation Based on Both Program Structure and Formal Specification
( 5 )
Specification-Based Rigorous Review of Programs
( 6 )
Visual Specification Animation
( 7 )
Automatic Transformation from Formal Specifications to Natural Language Description for Understanding and documentation management
( 8 )
Automated Software Transformation from Formal Specifications into Programs
( 9 )
Formal Engineering Methods for Software Process
( 10 )
Construction of an Intelligent Software Engineering Environment for SOFL
( 11 )
Computer-Aided Formalization of Semi-Formal Specifications
( 12 )
Dependable Systems Development with SOFL
( 13 )
Internet-Based Approach to Supporting Distributed Software Engineering
( 14 )
Intelligent Homepage Evolution Systems
 
( 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.
Selected Major 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)
(12) Research on Verification Technology for Software Requirements Specification, supported by Okawa Foundation Research Grant, Japan (2011 – 2012)
 (13)  Research on Automatic Detection of Errors for Information Communication Systems Development, funded by SCAT foundation, Japan (2012 – 2015).
 (14)  Research on Techniques for Detecting Program Errors Based on Formal Specifications, funded by NII (period: April 2011 – March 2014).
 (15)  Research and Development of a Highly Practical Formal Engineering Method and Its Supporting Tool, funded by Japan IPA SEC under the Advanced Research Support Project in Software Engineering (2012).
 (16) Research on Highly Reliable Agile Formal Engineering Methods, funded by the Ministry of Education, Culture, Sports, Science and Technology of Japan under Grant-in-Aid for Scientific Research A (No. 26240008)(2014 – 2019, 5 years).
Completed/Ongoing Projects (from 1995)