SE-LTL Model-checking on Timed GRAFCETS via ε-TPN
Médésu Sogbohossou *
Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Rodrigue Yehouessi
Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Tahirou Djara
Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Theophile Aballo
Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Antoine Vianou
Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
*Author to whom correspondence should be addressed.
Abstract
The GRAFCET standard (IEC 60848) is one of the convenient formalisms used to specify the behaviour of the automated systems. Being just a semi-formal language, the usual practice is to go through an unambiguous formalism such as time Petri net (TPN) in order to validate a specification expressed by a GRAFCET model. In this paper, we propose how to perform model-checking on a GRAFCET model translated into a ε-TPN, specifically with State-Event Linear Temporal Logic (SE-LTL). Especially, we provide a way to take into account quantitative time constraints verification by integrating observers in the ε-TPN intermediate model, since TPN state-space abstractions do not allow directly such kind of model-checking.
Keywords: GRAFCET (IEC 60848), Time Petri Net (TPN), model-checking, SE-LTL, observer.