Một khung làm việc chính quy để mô hình hóa và xác thực các sơ đồ Simulink
Tóm tắt
Từ khóa
#Tính toán Khoảng thời gian Thời gian #Simulink #hệ thống nhúng #xác thực chính quy #mô hình hóa #ngôn ngữ đặc tả thời gian thựcTài liệu tham khảo
Adams MM Clayton PB (2005) ClawZ: cost-effective formal verification for control systems. In: Proceedings of the 7th international conference on formal engineering methods. Springer Heidelberg pp 465–479
Arthan R Caseley P O’Halloran C Smith A (2000) Clawz: control laws in Z. In: Proceedings of the 3rd international conference on formal engineering methods. IEEE Computer Society Washington pp 169–176
Butler RW (2004) Formalization of the integral calculus in the PVS theorem prover. Technical report NASA Langley Research Center Hampton Virginia
Cavalcanti A Clayton P O’Halloran C (2005) Control law diagrams in Circus. In: Proceedings of the 13th international symposium of formal methods europe. Springer Heidelberg pp 253–268
Chen C Dong JS (2006) Applying timed interval calculus to simulink diagrams. In: Proceedings of the 8th international conference on formal engineering methods. Springer Heidelberg pp 74–93
Chen C Dong JS Sun J (2007) A formal framework for modeling and verifying simulink diagrams. http://www.comp.nus.edu.sg/~chenchun/SimInTIC
Chen C Dong JS Sun J (2007) Machine-assisted proof support for validation beyond Simulink. In: Proceedings of the 9th international conference on formal engineering methods. Springer Heidelberg pp 96–115
Chen C Dong JS Sun J (2008) A verification system for timed interval calculus. In: Proceedings of the 30th international conference on software engineering. ACM New York pp 271–280
Fidge CJ Hayes IJ Mahony BP (1998) Defining differentiation and integration in Z. In: Proceedings of the 2nd international conference on formal engineering methods. IEEE Computer Society Washington pp 64–73
Fidge CJ Hayes IJ Martin AP Wabenhorst A (1998) A set-theoretic model for real-time specification and reasoning. In: Proceedings of the mathematics of program construction. Springer Heidelberg pp 188–206
Gupta S Krogh BH Rutenbar RA (2004) Towards formal verification of analog designs. In: proceedings of the international conference on computer-aided design. IEEE Computer Science Washington pp 210–217
Henzinger TA Sifakis J (2006) The embedded systems design challenge. In Proceedings of the 14th international symposium on formal methods. Springer Heidelberg pp 1–15
Jersak M Cai Y Ziegenbein D Ernst R (2000) A transformational approach to constraint relaxation of a time-driven simulation model. In: Proceedings of the 13th international symposium on System synthesis. IEEE Computer Society Washington pp 137–142
Kowalewski S Stursberg O Fritz M Graf H Hoffmann I Preußig J Remelhe M Simon S Treseler H (1999) A case study in tool-aided analysis of discretely controlled continuous systems: The two tanks problem. In: Hybrid systems V. Springer Heidelberg pp~163–185
Liu Y Sun J Dong JS (2008) An analyzer for extended compositional process algebras. In: Companion of the 30th international conference on software engineering. ACM New York pp 919–920
Meenakshi B Bhatnagar A Roy S (2006) Tool for translating simulink models into input language of a model checker. In: Proceedings of the 8th international conference on formal engineering methods. Springer Heidelberg pp 606–620
Mahony BP Dong JS (1998) Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of the 20th international conference on software engineering. IEEE Computer Society Washington pp 95–104
Owre S Rushby JM Shankar N (1992) PVS: a prototype verification system. In: Proceedings of the 11th international conference on automated deduction. Springer Heidelberg pp 748–752
Pnueli A (2002) Embedded systems: challenges in specification and verification. In: Proceedings of the 2nd international conference on embedded software. Springer Heidelberg pp 1–14
Sims S Cleaveland R Butts K Ranville S (2001) Automated validation of software models. In: Proceedings of the 16th international conference on automated software engineering. IEEE Computer Society Washington pp 91–96
Sun J Liu Y Dong JS Wang HH (2008) Specifying and verifying event-based fairness enhanced systems. In: Proceedings of the 10th international conference on formal engineering methods. Springer Heidelberg pp 5–24
The MathWorks. Simulink ® 7—reference March 2008
The MathWorks. Simulink ® 7—using Simulink March 2008
Woodcock J, 1996, Using Z: specification, refinement and proof
Zhou C Li X (1994) A mean value calculus of durations. In: A classical mind: essays in honour of C. A. R. Hoare. Prentice-Hall International Englewood Cliffs pp 431–451