In March 2010, Takashi Kitamura (a post-doctoral fellow in AIST/CVS)
made a three-weeks visit to Bath University in British. The main
purpose of this visit was as follows:
1. The first purpose of his visit to Bath university is to develop his
current work, having discussion with researchers in Bath university in
order to refine the work and possibly to find new research directions
from it. His ongoing research work is on requirement engineering with
the approach of formal verification techniques. Formal verification
techniques in general have its theoretical bases on logics and formal
semantics. And these theoretical subjects are a main interest of Prof.
Power, Prof. McCasker and their research groups in Bath university. So
Takashi expected feedback from the theoretical view point of the
groups having interaction with them.
2. The second main purpose of his visit is to investigate the
applicability of category theory to formal methods which is Takashi's
main research interests. Category theory deals in an abstract way with
mathematical structures and relationships between them. Due to its
abstract treatment, its profound theory and its expressiveness as a
description language, category theory has been expected as a suitable
theoretical basis for computer science, especially in the field of
formal methods. As the research group in Bath university have been
active in the research field on category theory and in particular its
application to computer science, Takashi aims to investigate its
applicability to the field of his research interests for his further
development of research directions, taking the advantage of his visit.
The three-weeks of Takashi's visit at Bath university was productive,
resulting in a substantial result. The result includes:
- Substantial progress on his on-going work made having
interactions with researchers in Swansea university as well as Bath
university, which is presented in a workshop
- Investigation on applicability of category theory to software engineering
- Discussions with the laboratory members which conceive further
During his visit, substantial progress on his on-going work was made.
The progress he made was presented as a talk entitled "a logical
approach to requirement traceability and domain knowledge elicitation"
in Bath-AIST-Swansea Workshop held at Bath university on March 24th.
Also in the workshop, he had suggestive discussion with prof. McCasker
and prof. Power in Bath University, and Prof. Setzer and Prof.
Seisenberger in Swansea university. Prof. McCasker mentioned about the
possibility to characterize a part of the work with game semantics.
With prof. Power, he discussed about the relationship between category
theory and this work. These discussion may lead an interesting
research direction with connection between game semantics and category
theory and requirement engineering. Prof. Setzer commented a
possibility to apply Takashi's work to program optimization, and also
was interested in that more investigation on the property of "domain
knowledge", which is introduced in the given talk. Prof. Seisenberger
suggested that extending his work to program derivations would make
the work more practical and interesting from the practical view point.
Takashi found all of these suggestions and comments are quite
valuable to refine his work, and he possibly may be able to find a
further research direction from these suggestions.
Also during his visit, in parallel with his own on-going research, he
learned basics on category theory and investigated its applicability
to software engineering and formal methods in his own way. He leaned a
basic of category theory by studying several mathematical notions
dealt in category theory. Also through the investigation he
encountered a work called as "refinement calculus", which he roughly
understood was a discussion about a refinement technique using the
language of category theory. This idea is to quite extent close to
what he expected for a connection between category theory and
requirement engineering. As Takashi expected that there may be a
profound knowledge and development on this discussion relating his
research interest, he will make further investigation on this topic.
Also he attended some seminars on category theory and game semantics
given by Ms. Ana C. Calderon, a Ph.D. student in Bath university,
and Prof. McCasker.
In addition, he had several casual discussions to exchange research
ideas with other members of the laboratory in Bath university whose
research interests are close to his, including Dr. Jim Laird, Dr.
Dalia Khader, Dr. Owen Cliff, Mr. Martin Churchill, Ms. Ana C. Calderon,
and Mr. Alexey Strelnikov. The discussion with them were also
interesting, as their works also potentially have close connections
with his research interests and work.
In conclusion, Takashi's visit to Bath university was productive and
successful, as it shown by a substantial research progress and
meaningful research exchanges among AIST/CVS, Swansea university and
Bath university. His work including the progress made during this
visit is presented in Bath-AIST-Swansea Workshop at Bath university
held on March 24th. He had a suggestive discussion with researches in
Bath university and Swansea university, with which some refinements
will be made on the work and which contains possibilities of extending
his work to new research directions (such as a connection to game
semantics and an extension his work to program derivation and program
optimization). Also he did investigation on applicability of category
theory to software engineering, and through that he found some
relationship of category theory and requirement engineering which may
explore new research directions. In the end, Takashi thinks this visit
to Bath university was productive, and he wish to have chance to visit
Bath again in the future.