SE-LTL Model-checking on Timed GRAFCETS via ε-TPN

Main Article Content

Médésu Sogbohossou
Rodrigue Yehouessi
Tahirou Djara
Theophile Aballo
Antoine Vianou

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.

Article Details

How to Cite
Sogbohossou, M., Yehouessi, R., Djara, T., Aballo, T., & Vianou, A. (2019). SE-LTL Model-checking on Timed GRAFCETS via ε-TPN. Current Journal of Applied Science and Technology, 38(6), 1-12. https://doi.org/10.9734/cjast/2019/v38i630433
Section
Original Research Article

References

Darvas D, Majzik I, Vi˜nuela EB. PLC program translation for verification purposes. Periodica Polytechnica, Electrical Engineering and Computer Science. ;61:151-165.

Clarke EM, Henzinger TA, Veith H. Introduction to model checking. Springer International Publishing, Cham. 2018;1-26.

IEC 60848. Grafcet specification language for sequential function charts. Technical Report, International Electrotechnical Commission; 2013.

IEC 61131-3. Programmable controllers -part 3: Programming languages. Technical Report, International Electrotechnical Commission; 2013.

Ovatman T, Aral A, Polat D, U¨nver AO. An overview of model checking practices on verification of PLC software. Softw. Syst. Model. 2016;15(4):937-960.

L’Her D, Le Parc P, Marc´e L. Proving sequential function chart programs using timed automata. Theoretical Computer Science. 2001;267(1-2):141-155.

Sogbohossou M, Vianou A. Formal modelling of grafcets with time petri nets. IEEE Transactions on Control Systems Technology. 2015;23(5):1978-1985.

Chaki S, Clarke EM, Ouaknine J, Sharygina N, Sinha N. State/event-based software model checking. In IFM, Springer. ;2999:128-147.

Bauer N, Engell S, Huuck R, Lohmann S, Lukoschus B, Remelhe M, Stursberg O. Verification of PLC programs given

as sequential function charts. Integration of Software Specification Techniques for Applications in Engineering. 2004;517-540.

Toussaint J, Simonot-Lion F, Thomesse JP. Time constraint verification methods based on time petri nets. Proceedings of the Sixth IEEE Computer Society Workshop on Future Trends of Distributed Computing Systems. 1997;262-267.

Berthomieu B, Vernadat F. Time Petri nets analysis with TINA. In Quantitative Evaluation of Systems, QEST 2006. IEEE. ;123-124.

Sogbohossou M, Vianou A. ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets. ARIMA Journal, Special Issue CARI 2018. Nabil Gmati, Eric Badouel, Bruce Watson, Eds., 2019;31:1-22.

ter Beek MH, Fantechi A, Gnesi S, Mazzanti F. An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In FMICS. Springer. 2007;133-148.

Alur R, Courcoubetis C, Dill D. Modelchecking in dense real-time. Information and Computation. 1993;104(1):2-34.

Markey N, Schnoebelen P. TSMV: A symbolic model checker for quantitative analysis of systems. In QEST. 2004;4:330-331.

Boucheneb H, Gardey G, Roux OH. TCTL model checking of time petri nets. Journal of Logic and Computation. 2009;19(6):1509-1540.

Cassez F, Roux OH. Structural translation from time petri nets to timed automata. Journal of Systems and Software. ;79(10):1456-1468.