A Specification and Verification Method on Component Composition of Real-Time Reactive Systems

Timed component interface control flow automata (TCICFA) is presented to specify and verify composite real-time components´ invocation behavior and timing constraint information. By analyzing TCICFAs, a component reachability graph (CRG) can be constructed based on the constructing algorithm we presented. Each node in CRG is equipped with a state formula which has been computed with the construction of the CRG, and assertions can be made at each node to express safety, real-time liveness and other trustworthiness properties. Then all kinds of nonfunctional trustworthiness properties of composite components in real-time reactive systems (RTRS) can be verified based on the CRG using a SAT solver.