On Improved Verification of Reconfigurable Real-Time Systems

This paper deals with formal modeling and verification of reconfigurable real-time systems under reconfigurability and real-time constraints. To deal with the modeling, we enrich the formalism, named reconfigurable timed net condition event systems (R-TNCESs), with new reconfiguration forms such as the ability to update the earliest/latest firing time on the intervals which are associated to flow arcs. To handle the verification of the new extended formalism, an algorithm is defined to generate a timed accessibility graph for timed net condition event systems (TNCESs). We control the verification complexity of R-TNCESs using a new method which accelerate the generation of accessibility graphs, where redundancies, repetitions, and unnecessary computations are avoided as much as possible. An experimentation is carried out and a performance evaluation is achieved to demonstrate the advantages of the proposed contribution compared with related works.