Theory of formal specification and verification of concurrency systems and real-time systems based on linear logic

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

We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting.In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification.Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.