It has been needed to stop systems for software maintenance, that is, modifying software for debugging or improvement while the system is operating. However, the recent trends of rapid changes of system requirements and operating environments demand more and more frequent maintenance. Thus, stopping the systems at every maintenance activity make it impossible to use the systems appropriately. In particular, it is not desirable to stop net services that bring large benefits and systems requiring high reliability such as medical applications. Researchers are investigating technology to change software with no system interruptions. This technology is called dynamic software evolution.
Dynamic software evolution may case failures due to the timing of changes because the software changes during the system operation. However, it is difficult to find such failures because of the difficulties in testing considering all such timings. It is promising to investigate advanced techniques to make sure the correctness of software rigorously on the basis of mathematical theories. We aim at dynamic software evolution without failures by applying cutting edge technologies such as model checking and controller synthesis.
Model checking: This technique verifies if the software satisfies the specified properties by representing the behaviors of the software and the properties by finite state models and logical formulae respectively and checking exhaustively the behavior sequences. However, it it difficult to create behavior models of dynamic software evolution. We are investigating approaches to create such models effectively.
Controller synthesis: This technique captures a system behavior as control by interacting with the environments and automatically generate specifications of the controller. As mentioned before, it is important to control the timing of software change appropriately in order to realize dynamic software evolution without failures. We are investigating approaches to automatically generate the controller specification of the timing that satisfies given properties.