Computer Science ›› 2018, Vol. 45 ›› Issue (6A): 523-526.
• Interdiscipline & Application • Previous Articles Next Articles
LI Yun-chou,YIN Ping
CLC Number:
| [1]王蓁蓁.模型检验综述[J].计算机科学,2013,40(Z6):1-14. [2]CLARKE E M,EMERSON E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C]∥Workshop on Logic of Programs.Springer,Berlin,Heidelberg,1981:52-71. [3]CLARKE E M,EMERSON E A,SISTLA A P.Automatic verification of finite-state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems (TOPLAS),1986,8(2):244-263. [4]CLARKE E,KROENING D,LERDA F.A tool for checking ANSI-C programs[C]∥International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Springer,Berlin,Heidelberg,2004:168-176. [5]BALL T,RAJAMANI S.Checking temporal properties of software with boolean programs[C]∥Proceedings of the Workshop on Advances in Verification.2000:2-9. [6]HOLZMANN G J.The SPIN Model Checker:Primer and Refe- rence Manual[M].Addision-Wesley,2003. [7]BEYER D,HENZINGER T A,JHALA R,et al.Checking memo- ry safety with Blast[C]∥International Conference on Fundamental Approaches to Software Engineering.Springer,Berlin,Heidelberg,2005:2-18. [8]GODEFROID P.Software model checking:The VeriSoft ap- proach[J].Formal Methods in System Design,2005,26(2):77-101. [9]Jpf project[OL].http://babelfish.arc.nasa.gov/trac/jpf. [10]CIMATTI A,CLARKE EM,GIUNCHIGLIA F,et al.NuSMV:A new symbolic model checker[J].International Journal on Software Tools for Technology Transfer (STTT),2000,2(4):410-425. [11]DELANGE J,PAUTET L,KORDON F.Design,implementa- tion and verification of MILS systems[J].Software:Practice and Experience,2012,42(7):799-816. [12]PERVEZ S,GOPALAKRISHNAN G,KIRBY R M,et al.Formal methods applied to high-performance computing software design:a case study of mpi one-sided communication-based locking[J].Software:Practice and Experience,2010,40(1):23-43. [13]CHIAPPINI A,CIMATTI A,MACCHI L,et al.Formalization and validation of a subset of the European Train Control System[C]∥2010 ACM/IEEE 32nd International Conference Software Engineering.IEEE,2010:109-118. [14]BOCHOT T,VIRELIZIER P,WAESELYNCK H,et al.Model checking flight control systems:The airbus experience[C]∥Proceedings of the 31st International Conference on Software Engineering (ICSE 2009).Companion Volume,IEEE,2009:18-27. [15]HAVELUND K,LOWRY M R,PENIX J.Formal analysis of a spacecraft controller using SPIN[J].IEEE Transactions on Software Engineering,2001,27(8):749-765. [16]KROENING D,CLARKE E.The CPROVER User Manual [EB/OL].http://www.cprover.org/cbmc/doc/manual.pdf. [17]METTA R.Verifying code and its optimizations:An experience report[C]∥2011 IEEE Fourth International Conference Software Testing,Verification and Validation Workshops (ICSTW).IEEE,2011:578-583. [18]CHEN T Y,CHEUNG S C,YIU S M.Metamorphic testing:a new approach for generating next test cases:Technical Report HKUST-CS98-01[R].Hong Kong:Department of Computer Science,Hong Kong University of Science and Technology,1998. [19]董国伟,徐宝文,陈林,等.蜕变测试技术综述[J].计算机科学与探索,2009,32(2):130-143. |
| [1] | RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130. |
| [2] | CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314. |
| [3] | XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211. |
| [4] | HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31. |
| [5] | ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294. |
| [6] | LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75. |
| [7] | NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214. |
| [8] | YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493. |
| [9] | ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602. |
| [10] | LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319. |
| [11] | DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266. |
| [12] | GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503. |
| [13] | QU Yuan-yuan, HONG Mei and SUN Ning. Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System [J]. Computer Science, 2017, 44(Z11): 542-546. |
| [14] | ZHANG Xing-long, YU Lei, HOU Xue-mei and HOU Shao-fan. Method of Metamorphic Relations Constructing for Object-oriented Software Testing [J]. Computer Science, 2017, 44(Z11): 485-489. |
| [15] | GUO Zong-hao and WEI Ou. Optimal Control of Probabilistic Boolean Networks Using Model Checking [J]. Computer Science, 2017, 44(5): 193-198. |
|
||
Home