| Autor: |
Yangli Jia, Zhenling Zhang, Zhoujun Li, Xutao Du |
| Rok vydání: |
2008 |
| Předmět: |
|
| Zdroj: |
2008 Third Asia-Pacific Trusted Infrastructure Technologies Conference. |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
