On Improving R-TNCES Rebuilding for Reconfigurable Real-Time Systems

This paper deals with improved verification of real-time systems that extend the classical formal verification with the rebuilding of reconfigurable timed net condition event systems (R-TNCESs). Indeed, previous computation tree logic (CTL) model repair approaches make the model checking eligible for generating a new correct model from a faulty one at the debugging level. We propose R-TNCESs rebuilding method, which allows both verification and modification of real-time system models. The proposed approach generates from an incorrect model a new one that satisfies a given computation tree logic/Timed computation tree logic formula. Temporal logic formulas (CTL/TCTL) are defined to deal with the system functional/temporal properties specification respectively. This paper provides an efficient algorithm with a set of transformation rules to achieve the rebuilding phase. Finally, FESTO MPS platform is used as a case study to demonstrate the proposed rebuilding method for real-time system models. The obtained results show the efficiency of our contribution and its scalability in large complex systems.