分野別セミナー

In this talk, I present an approach to develop logical structures supporting the efficient development of correct reconfigurable software systems, i.e. systems with reconfigurable mechanisms managing the dynamic evolution of their configurations in response to external stimuli or internal performance measures. The potential of reconfigurable software systems is virtually unlimited. So, one natural question emerges: if applications with reconfigurable features are so great why isn’t the market full of them? One of the main problems is the lack of formal methods to support the implementation of such architectures.


The present approach is rooted in algebraic specification, one of the most important classes of formal methods, where it is mandatory to have a logic, formalized as an institution, to underlie the specification language. The developments are guided by the following simple idea: reconfigurations are regarded as transitions from one configuration to another, which in turn are formalized as "local" models. This suggest the idea of a modal language to express them. Since in practice we require the ability to refer to individual states of the models, the natural choice is to use a hybrid logic. Different problems require various formalisms, and therefore, an abstract framework for the development of the results is proposed, and a list of issues that need to be addressed are presented.