[1] 陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A):1933-1938. Chen Huo-wang,Wang Ji,Dong Wei.High confidence software engineering technologies[J].Acta Electronica Sinica,2003,31(12A):1933-1938.(in Chinese) [2] Mahmood S,Lai R,Soo Kim Y,et al.A survey of component based system quality assurance and assessment[J].Information and Software Technology,2005,47(10):693-707. [3] Reay KA,Andrews JD.A fault tree analysis strategy using binary decision diagrams[J].Reliability Engineering & System Safety,2002,78(1):45-56. [4] Čepin M,Mavko B.A dynamic fault tree[J].Reliability Engineering & System Safety,2002,75(1):83-91. [5] Kaiser B.State Event trees:A safety and reliabiity analysis techniqure for software controlled systems[D].Kaiserslautern:Universität Kaiserslautern,2007. [6] Bryant R E.Graph-based algorithms for Boolean function manipulation[J].IEEE Transactions on Computers,1986,100(8):677-691. [7] Hersmans H.Interactive Markov Chains[M].Berlin:Springer-Verlag,2002.57-88. [8] De Alfaro L,Henzinger T A.Interface automata[A].Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE 01)[C].New York:ACM Press,2001,109-120. [9] 周颖,郑国梁,李宣东.面向模型检验的UML状态机语义[J].电子学报,2003,31(12A):2091-2095. Zhou Ying,Zheng Guo-liang,Li Xuan-dong.An operational semantics for UML state machines in model checking context[J].Acta Electronica Sinica,2003,31(12A):2091-2095.(in Chinese) [10] Baier C,Haverkort B,Hermanns H,et al.Model-checking algorithms for continuous-time Markov chains[J].IEEE Transactions on Software Engineering,2003,29(6):524-541. [11] Katoen JP,Khattri M,Zapreevt I.A Markov reward model checker[A].Proceedings of the Second International Conference on the Quantitative Evaluation of Systems (QEST'05)[C].Torino:IEEE Computer Society,2005.243-244. [12] 张广泉,戎玫,朱雪阳,何亚丽,石慧娟.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报,2011,39(3A):86-93. Zhang Guang-quan,Rong Mei,Zhu Xue-ya,He Ya-li,Shi Hui-juan.Specification and verification of web service composition based on XYZ/ADL[J].Acta Electronica Sinica,2011,39(3A):86-93.(in Chinese) [13] 张君华,黄志球,曹子宁.模型检测基于概率时间自动机的反例产生研究[J].计算机研究与发展,2008,45(10):1638-1645. Zhang Jun-hua,Huang Zhi-qiu,Cao Zi-ning.Counterexample generation for probabilistic timed automata model checking[J].Journal of Computer Research and Development,2008,45(10):1638-1645.(in Chinese) [14] Boudali H,Crouzen P,Stoelinga M.A rigorous,compositional,and extensible framework for dynamic fault tree analysis[J].IEEE Transactions on Dependable and Secure Computing,2010,7(2):128-143. |