Spécification et Vérification des PropriétésTemporelles Qualitatives et Quantitatives desSystèmes Temps Réel Complexes
Abdia Hamdani · HAL (Le Centre pour la Communication Scientifique Directe) · 2023
Analyzing and verifying complex real-time systems permits to verify their correctness, reliability, and safety. Indeed, Model-Cheking is a very well-known method to verify the qualitative (e.g.: state accessibility, liveness, blocking, etc...) and quantitative properties (e.g.: Bounded time response ) of the model. T Petri net formalism and its extensions are widely used in the literature,with an important number of advantages as their graphical and intuitive representations, abundant analysis techniques...etc.. We are interested in using Petri net formalism as a modeling tool, extended to time and synchronization mechanisms. Thus, a new extension is defined calledRT P N for : (Time Petri Nets with Rendezvous). Then, a sub-class of the proposed model is defined noted RTW F N for : (Time Workflow Nets with Rendezvous) dedicated to specify workflow systems. A method forcomputing an abstraction of the state space of the proposed model is proposed. The method is based on the State Class graph formalism which mainly saves linear properties of the model. Finally, we show how to deduce the qualitative and quantitative properties of the model bu considering a case study.