OK_GF_ICSOFT-EA_Jul_2015

Khlifi, O.; Mosbahi, O.; Khalgui, M.; Frey, G.: GR-TNCES: New Extensions of R-TNCES for Modelling and Verification of Flexible Systems under Energy and Memory Constraints. Proceedings of the 10th International Conference on Software Engineering and Applications (ICSOFT-EA 2015), ISBN 978-989-758-114-4, pp. 373-380, Colmar/Alsace, France, Jul. 2015.

Abstract

This study deals with the formal modeling and verification of Adaptive Probabilistic Discrete Event Control Systems (APDECS). A new formalism called Generalized Reconfigurable Timed Net Condition Event Systems (GR-TNCES) based on R-TNCES is proposed for the optimal functional and temporal specification of APDECS. It is composed of behavior and control modules. This formalism is used for the modeling and control of unpredictable as well as predictable reconfiguration processes under memory and energy constraints. A formal case study is proposed to illustrate the necessity of this formalism and a formal verification based on the probabilistic model checker Prism is used to check the proposed model.

Keywords: Distributed Discrete Event Control System, Adaptive System, Reconfiguration, Modeling, Formal Verification, Model Checking, Energy Control, Memory Control.