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
Simulink được sử dụng rộng rãi trong ngành công nghiệp để mô hình hóa và mô phỏng các hệ thống nhúng. Với việc sử dụng ngày càng tăng của các hệ thống nhúng trong các tình huống an toàn thời gian thực quan trọng, Simulink trở nên thiếu khả năng phân tích yêu cầu (thời gian) với độ tin cậy cao. Trong bài viết này, chúng tôi áp dụng Tính toán Khoảng thời gian Thời gian (TIC) - một ngôn ngữ đặc tả thời gian thực, để bổ sung khả năng kiểm định chính quy TIC cho Simulink. Chúng tôi xây dựng một cách tỉ mỉ các hàm thư viện TIC để mô hình hóa các khối thư viện Simulink, được sử dụng để tạo thành các sơ đồ Simulink. Tiếp theo, các sơ đồ Simulink được tự động chuyển đổi thành các mô hình TIC, bảo toàn các khía cạnh chức năng và thời gian. Các yêu cầu quan trọng như liveness bị giới hạn thời gian có thể được đặc tả chính xác trong TIC cho toàn bộ sơ đồ hoặc một số thành phần. Cuối cùng, việc xác thực các mô hình TIC có thể được tiến hành chặt chẽ với một mức độ tự động hóa cao bằng cách sử dụng một công cụ định lý chung. Khuôn khổ của chúng tôi có thể mở rộng không gian thiết kế bằng cách đại diện cho các thuộc tính môi trường cho các hệ thống mở và xử lý các sơ đồ phức tạp vì việc phân tích hành vi liên tục và rời rạc được hỗ trợ.
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