International collaborative studies on a logical specification and verification language.

点击翻译按钮获取中文摘要

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.