research

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

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.

Current/Future Research Projects

1. Software Error Prevention by Formal Specification and Animation

How to prevent critical and directional software errors in the phase of requirements analysis still remains a challenge for software engineering. In this research, we aim to work out a systematic and effective way to carry out requirements analysis and to prevent requirements errors by means of constructing formal specifications and carrying out specification animation. Since most critical and directional software errors often come from the inconsistency and incompleteness of requirements, the essential problem to address is how to write specifications and carry out their animation so that all the potential user requirements can be discovered and documented consistently, and how such a process can be effectively supported.

2. Automatic Testing-Based Formal Verification (TBFV)

Formal verification for the correctness of programs based on Hoare logic or symbolic execution has the potential to prove that the program is bug-free with respect to its specification but suffers considerable limitations in dealing with loops, side effect, function calls, and complex data structures. Formal specification-based testing can be utilized to automatically identify bugs in programs but lacks the capability of telling that the program is bug-free in general. In this research, we aim to properly integrate specification-based testing and Hoare logic and symbolic execution to establish a unified approach to formal verification of programs. The essential idea is to use testing to identify program paths and use formal verification to prove the correctness of the identified paths. To this end, a proof obligation will be automatically formed based both on the specification and the path, and then either a formal proof or rigorous testing will be deployed to discharge the proof obligation. How to automatically generate adequate test cases and how to automatically identify program paths are the key topics for research in this direction. Further development of this research will include automatic debugging and automatic error correction as well as intelligent software tool support for the technologies.

3. Human-Machine Pair Programming (HMPP)

Programming is the major activity to provide working software advocated in the Agile development paradigm but lacks effective techniques to address the challenges in ensuring software quality, productivity, and maintainability. In this research, we aim to establish an intelligent Human-Machine Pair Programming (HMPP) technology to support efficient and reliable programming.

HMPP is characterized by the feature that humans create algorithms, data structures, and the architecture of the program whereas the machine takes care of checking the program under construction to identify potential software defects or violation of standards in the program and to predict useful program segments for enhancing the robustness and the completeness of the program. This approach includes Software Construction Monitoring (SCM) and Software Construction Predicting (SCP) as its two key techniques, both of which need to integrate the AI knowledge base and machine learning technologies into the technologies for programming. The essential problem is how to carry out SCM and SCP so that the final program can be efficiently produced and its qualities are guaranteed.

To help enhance the maintainability of the program, automatic reversing from the current program version to comprehensible graphical documentation, such as data flow diagrams or UML diagrams, also needs to be supported and the necessary technology needs to be worked out as well.

Another research topic is how to support the iterative programming in which the programmer concentrates on constructing new program code while the machine dynamically and effectively guides the programmer to review the appropriate parts of the already constructed code to identify and correct potential bugs. The challenge is how the programmer can be guided to choose the appropriate target parts of the code to review, to identify bugs, and to correct the uncovered bugs.

4. Specification-Based "Vibration" Testing

Specification-based testing is a black-box testing for programs and can be fully automated if the specification is formalized in a formal notation. It is characterized by the fact that test cases are generated only based on the specification, without the need to know the structure of the corresponding program. However, the challenge is how test cases can be generated to efficiently cover all of the representative program paths. In this research, we aim to establish a systematic method, called "Vibration" Testing or simply V-Testing, based on formal specifications. The essential idea is to repeatedly generate test cases based on the change of the distance between two atomic predicates in the hope of increasing the program path coverage. The problems to address include how the distance change should be planned and how specific test cases can be automatically generated based on the changed distance. An effective tool support for the V-Testing method is also the focus of the research. The V-Testing can be used effectively to test programs whose source code is not available for the tester. Another topic of this research is how to automatically predict the reliability of the program using the V-Testing.

5. Human-Machine Pair Review (HMPR)

Program review is a conventional but effective technique for software quality assurance. In particular, peer review is strongly advocated. However, peer review faces a critical limitation that the peer usually faces great difficulty in understanding the semantics of the program and in making a correct judgement on software defects. In this research, we try to establish en effective technology including both a method and tool to support program review by the programmer himself or herself. The essential issue is how the machine can effectively remind and even guide the programmer to efficiently review the program and to identify bugs. This approach can also be extended to review specifications, designs, and testing documents as well.

6. Intelligent Software Engineering Environment for Agile-SOFL

Agile-SOFL is an Agile Formal Engineering Method for software development, aiming to achieve both high software productivity and reliability. It offers a three-step hybrid specification approach, specification-based human-machine pair programming, and automatic specification-based testing and verification techniques. In this research, we try to utilize AI knowledge base and machine learning technologies to support the entire process of software development using the above techniques in a systematic manner. The ISEE can be divided into Method-Based ISEE, Domain-Based ISEE, and Method-Domain-Based ISEE, depending on how the required knowledge is learned and what specific activities need to be supported.

7. Safety/Security-Critical Systems Specification and Verification

Safety/Security-critical systems are required to ensure both the desired functionality and the safety/security constraints are satisfied by the final software product. To fulfil this goal, Agile-SOFL, characterized by specification-based programming and verification and validation, is regarded as an effective and efficient technology. In this research, we aim to establish a specific specification approach that properly interweaves the functional specification with the safety/security constraints. The functional specification can be written in the functional scenario manner while the safety/security requirements or constraints can be derived by means of fault tree analysis or attacking tree analysis. The questions are how to systematically incorporate the safety/security constraints into the functional specification for programming and how to test and verify the safety/security properties of the program based on the specification. We will also study how this technology can be effectively applied to develop ITS (Intelligent Transport Systems, including automatic railway systems and automatic automobile driving systems) and other safety/security-critical systems.

Selected Major Funded Research Projects (1995 ~ Present)

Automatic Transformation of Formal Specifications (funded by Hiroshima City University) (1995

Formal Methods and Intelligent Software Engineering Environments (funded by the Ministry of Education, Culture, Sports, Science and Technology of Japan) (1996-1998)

Safety-Critical Systems Development Using Formal Methods (funded by Hiroshima City University) (1996-1998)

Application of Formal Methods to Railway Systems (funded by Mitsubishi Research Institute in Hyogo pref ) (1997-1999)

Software Evolution (funded by the Ministry of Education, Culture, Sports, Science and Technology of Japan) (1998-2000)

Formal Engineering Methods for Software Development (funded by the Ministry of Education, Culture, Sports, Science and Technology of Japan) (1999-2002)

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)

Research on Application of Formal Methods (funded by The Nippon Signal Co. Ltd.) (2007-2009)

Research on Specification-Based Automatic Testing Techniques (funded by NII) (2008-2010)

Research on Verification Technology for Software Requirements Specification, supported by Okawa Foundation Research Grant, Japan (2011 – 2012)

Research on Automatic Detection of Errors for Information Communication Systems Development, funded by SCAT foundation, Japan (2012 – 2015).

Research on Techniques for Detecting Program Errors Based on Formal Specifications, funded by NII (period: April 2011 – March 2014).

Research on Techniques for Detecting Program Errors Based on Formal Specifications, funded by NII (period: April 2011 – March 2014).

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

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

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