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.
Yangli Jia Zhoujun Li Xutao Du Zhenling Zhang
School of Computer Science and Engineer, Beihang University, Beijing, China Department of Computer Science and Technology, Tsinghua University, Beijing, China School of Computer Science and Technology, LiaoCheng University, Liaocheng, China
国际会议
Third Asia-Pacific Trusted Infrastructure Technologies Conference(第三届亚太地区可信基础架构技术大会)(APTC 2008)
武汉
英文
142-149
2008-10-14（万方平台首次上网日期，不代表论文的发表时间）