Page 273 - 《软件学报》2021年第6期

陆芝浩 等:Ptolemy 离散事件模型形式化验证方法 1847

[5] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183−235.
[6] Behrmann G, David A, Larsen K. A tutorial on uppaal. In: Proc. of the Formal Methods for the Design of Real-Time Systems.
Springer, 2004. 200−236.
[7] Bengtsson J, Yi W. Timed automata: Semantics, algorithms and tools. LNCS, 2003,87−124.
[8] Xing JS, Theelen BD, Langerak R, Van JDP, Tretmans J, Voeten JPM. From POOSL to UPPAAL: Transformation and quantitative
analysis. In: Proc. of the 2010 10th Int’l Conf. on Application of Concurrency to System Design. 2010. 47−56. [doi: 10.1109/ACSD.
2010.21]
[9] Guo C, Ren SP, Jiang Y, Wu PL, Sha L, Richard B, Berlin J. Transforming medical best practice guidelines to executable and
verifiable statechart models. In: Proc. of the ACM/IEEE Int’l Conf. on Cyber-Physical Systems. ACM, 2016.
[10] Jiang Y, Liu H, Song H, Kong H, Wang R, Guan Y, Liu S. Safety-Assured model-driven design of the multifunction vehicle bus
controller. IEEE Trans. on Intelligent Transportation Systems, 2018,19(10).
[11] Csertan G, Huszerl G, Majzik I, Pap Z, Andras P. VIATRA—Visual automated transformations for formal verification and
validation of UML models. In: Proc. of the Automated Software Engineering. 2002. 267−270. [doi: 10.1109/ASE.2002.1115027]
[12] Jordi C, Robert C, Daniel R. UMLtoCSP: A tool for the formal verification of UML/OCL models using constraint programming. In:
Proc. of the 22nd IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE 2007). New York: Association for Computing
Machinery, 2007. 547−548. [doi: https://doi.org/10.1145/1321631.1321737]
[13] Liu Y, Ma ZY, He X, Shao WZ. Approach to transforming UML model to reliability analysis model. Ruan Jian Xue Bao/Journal of
Software, 2010,21(2):287−304 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3792.htm [doi: 10.3724/SP.J.
1001.2010.03792]
[14] Yang ZB, Hu K, Zhao YW, Ma DF, Bodeveix JP. Verification of AADL models with timed abstract state machines. Ruan Jian Xue
Bao/Journal of Software, 2015,26(2):202−222 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4776.htm [doi:
10.13328/j.cnki.jos.004776]
[15] Berthomieu B, Bodeveix JP, Chaudet C, Zilio SD, Filali M, Vernadat F. Formal verification of AADL specifications in the
topcased environment. In: Proc. of the 14th Ada-Europe Int’l Conf. on Reliable Software Technologies. Berlin, Heidelberg:
Springer-Verlag, 2009. 207−221. [doi: 10.1007/978-3-642-01924-1_15]
[16] Liang ML, Wang XP, Xue XP, Li G. Formal verification of UML models based on TLA. Computer Engineering, 2011,37(2):72−74.
[17] Jiang Y, Song HB, Yang YX, Liu H, Gu M, Guan Y, Sun JG, Sha L. Dependable model-driven development of CPS: From
stateflow simulation to verified implementation. ACM Trans. on Cyber-Physical Systems, 2019,3(1):12:1−12:31.
[18] Hu K, Zhang T, Yang ZB, Gu B, Jiang S, Jiang BC. Formal verification of TASM models by translating into UPPAAL. Journal of
Donghua University (English Edition), 2012,29(1):54−57.
[19] Michael R, Strichman O. Translation validation: From simulink to C. In: Proc. of CAV 2009. 2009. 696−701. [doi: 10.1007/978-3-
642-02658- 4_57]
[20] Guo DQ, Lü JD, Wang SL, Tang T, Zhan NJ, Zhou DT. Formal analysis and verification of train control system of High-speed
railway in China. Scientia Sinica Informationis, 2015,45(3):417−438 (in Chinese with English abstract).
[21] Jiang Y, Zhang HH, Li ZH, Deng YD, Song XY, Gu M, Sun JG. Design and optimization of multiclocked embedded systems using
formal techniques. IEEE Trans. on Industrial Electronics, 2015,62(2):1270−1278.
[22] Jiang Y, Zhang HH, Zhang HF, Liu H, Song XY, Gu M, Sun JG. Design of mixed synchronous/asynchronous systems with multiple
clocks. IEEE Trans. on Parallel Distributed Systems, 2015,26(8):2220−2232.
[23] Bae K, Olveczky PC, Feng TH, Tripakis S. Verifying ptolemy II discrete-event models using real-time maude. In: Proc. of the Int’l
Conf. on Formal Engineering Methods. 2009. 717−736.

附中文参考文献:
[2] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33−61. http://www.jos.org.cn/1000-9825/5652.htm [doi:
10.13328/j.cnki.jos.005652]
[3] 林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(z1):1907−1912.