Application of projection temporal logic in system modeling
Zhenhua Duan · Journal of Northwest University · 2010
Aim To solve the problem that two different tools are needed in system modeling and properties description respectively when doing formal verifications. Methods PTL is employed to describe the properties as well as the implication of the system to be verified within a same logical framework. Results The properties and purpose of projection operators of PTL are analyzed in detail; further,an example is given to illustrate how PTL woks in system modeling. Conclusion PTL has a powerful expressiveness and can be widely used in formal verifications for various software and hardware systems.