 |
Model checking is a type of formal method, which is an automated technique that shows whether the properties of such a model are satisfied for a given system's finite state model and logical properties.
As shown in Figure 4, Model checking consists of a model that specifies the system, specific properties of the system, and a model checker that operates by receiving properties and models.
In order to do model checking, first, finite state-based modeling is performed and specific properties of the model are specified using Temporal Logic. The specified model and properties are verified using the model checker to verify that the model satisfies the properties. Model checker is fully automated and generates counterexamples through error tracking.
UPPAAL is an integrated tool environment for modeling, validation and verificaction of real-time systems modeled as networks of timed automata.
Network means, system is modelled as a network several timed automata in parallel. |
IEEE/ICACT20210216 Slide.08
[Big Slide]