Dependable Software Engineering Research

Projects

Recent Research Themes and Collaboration with Industry.

Research Themes

1. Formal Methods and their Applications

Application of Formal Methods to Early Stages of Software Development such as Modeling or Requirements

• Automated Analysis of Behavioral Specifications in Event-B
• Formalization and Analysis of Feature Diagram -- Software Product Line Engineering

2. Automated Verification of Programs

A Posteriori Verification and Automated Test Generation

• Integrating the Notion of Design-by-Contract with Bounded Model-Checking Method
• Specification-based Test Generation
• Automated Diagnosis of Programs -- Locating Bugs

3. Model Checking Tools

Application of Automated Verification Methods to Various Issues in Software Engineering

• Automated Analysis of Object-Oriented Design with SMT Tools
• Aspectual SPIN : SPIN/Promela with the Notion of Aspect
• Behavioral Analysis of Web Service Flows with SPIN/Promela

4. Soft Faults in Software Intensive Systems

Architectural Framework and Intrinsic Properties of Open Systems Self-Adapted in Response to Changes in Requirements or High-Level Policy

• Self-Reconfigurable PHP-based Web Applications
• Systematic Derivation of User Policy

5. Highly Reliable Embedded Systems Design

Modeling and Automated Analysis of CPS-type (Cyber-Physical Systems) Software-Intensive Embedded Systems

Collaboration with Industry

1. Dependable Software Forum (DSF)

Conducting Feasibility Studies of using Formal Methods in Development of Business Critical Systems (Enterprise Software Systems)

Six Major IT Companies (NTT Data, Fujitsu, NEC, Hitachi, Toshiba, CSK) and NII

2. Survey on Software Engineering in CPS-Era (Cyber-Physical Systems)

Supported by SSR (Joint Forum for Strategic Software Research) in 2010

Report in Japanese (Password Required)