On Improving RTNCES Rebuilding for Reconfigurable RealTime Systems This paper deals with improved verification of realtime systems that extend the classical formal verification with the rebuilding of reconfigurable timed net condition event systems (RTNCESs). 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 RTNCESs rebuilding method, which allows both verification and modification of realtime system models. The proposed approach generates from an incorrect model a new one that satisfies a given computation tree logicTimed computation tree logic formula. Temporal logic formulas (CTLTCTL) are defined to deal with the system functionaltemporal 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 realtime system models. The obtained results show the efficiency of our contribution and its scalability in large complex systems.

Specification and Analysis of the AERNCA Active Network Protocol Suite in RealTime Maude This paper describes the application of the RealTime Maude tool and the Maude formal methodology to the specification and analysis of the AERNCA suite of active network multicast protocol components. Because of the timesensitive and resourcesensitive behavior and the composability of its components, AERNCA poses challenging new problems for its formal specification and analysis. RealTime Maude is a natural extension of the Maude rewriting logic language and tool for the specification and analysis of realtime objectbased distributed systems. It supports a wide spectrum of formal methods, including: executable specification; symbolic simulation; and infinitestate model checking of temporal logic formulas. These methods complement those offered by finitestate model checkers and generalpurpose theorem provers. RealTime Maude has proved to be wellsuited to meet the AERNCA modeling challenges, and its methods have been effective in uncovering subtle and important errors in the informal use case specification.