M. S. Sobolev, “Using X-CTL logic to implement formal verification of X-machines”, Informatsionnye Tekhnologii i Vychslitel'nye Sistemy, 2010, Issue 3,Pages <nobr>47

MATHEMATICAL MODELING

Using X-CTL logic to implement formal verification of X-machines

M. S. Sobolev

Moscow Institute of Physics and Technology (State University), Dolgoprudny, Moscow region

Abstract: The article contains the review of CTL logic and its application to formal verification. X-CTL logic is proposed, allowing implementing the formal verification of X-machines. The sample model of a counter is presented.

Keywords: Formal verification, model checking, X-Machine, complex systems.