Virual Oral Presentation Slide by Slide

IEEE/ICACT20220362 Slide.12        [Big Slide]       [YouTube]	Oral Presentation
	The query language of UPPAAL model Checker is a subset of TCTL(timed computation tree logic) Verification attributes include reachability, safety, and liveness. Reachability properties are used while designing a model to perform sanity checks and validate the basic behavior of the model. Let P be a state formulae. E<> P : Some state satisfying P should be reachable. Safety is the property that ˇ°Something bad will never happen.ˇ± In UPPAAL these properties are formulated positively, for example, something good is invariantly true. Liveness is the property of ˇ°good things happen someday.ˇ± A<>P : P is eventually satisfied. P-->Q : Whenever P is satisfied, then Q will eventually be satisfied

[Go to Next Slide]

Select Voice: Virtual Oral Presentation!!