Xác minh hệ thống điều khiển chủ động bằng cách sử dụng đại số quá trình tạm thời

Engineering with Computers - Tập 12 - Trang 46-61 - 1996
Wael M. Elseaidy1, John W. Baugh1, Rance Cleaveland2
1Department of Civil Engineering, North Carolina State University, Raleigh, USA
2Department of Computer Science, North Carolina State University, Raleigh, USA

Tóm tắt

Trong bài báo này, chúng tôi mô tả những phương pháp bổ sung có thể được sử dụng để đảm bảo độ tin cậy của các hệ thống thời gian thực, chẳng hạn như các hệ thống kiểm soát kết cấu chủ động. Những phương pháp này bao gồm cả kiểm tra mô hình và mô phỏng, và dựa trên một đại số quá trình tạm thời. Chúng tôi kết hợp các phương pháp chính quy này với một kỹ thuật lập mô hình đồ họa, Modechart, để xác định một hệ thống kiểm soát kết cấu chủ động bao gồm nhiều bộ xử lý. Các yêu cầu về thời gian trên hệ thống được xác định và xác minh bằng sự kết hợp giữa các mô hình đại số quá trình và logic dạng hợp, và nhiều khái niệm mô phỏng khác nhau được mô tả để gỡ lỗi các mô hình và để có cái nhìn sâu sắc về hành vi của hệ thống.

Từ khóa

#hệ thống thời gian thực #hệ thống kiểm soát kết cấu chủ động #đại số quá trình tạm thời #kiểm tra mô hình #mô phỏng #kỹ thuật lập mô hình đồ họa #Modechart #yêu cầu thời gian.

Tài liệu tham khảo

Chong, K.P.; Liu, S.C.; Li, J.C. (Editors) (1990) Intelligent Structures, Elsevier, Amsterdam. Proceedings of the International Workshop on Intelligent Structures held in Taipei, Taiwan Wen, Y. (Editor) (1992) Intelligent Structures 2: Monitoring and Control, Elsevier, Elsevier Applied Science, London. Proceedings of the International Workshop on Intelligent Systems held in Perugia, Italy Soong, T.T. (1990) Active Structural Control, Longman Scientific, New York Leveson, N.G. (1986) Software safety: Why, what, and how. Computing Surveys, 18, 2, 125–163, June. Burns, A.; Wellings, A. (1990) Real-Time Systems and Their Programming Languages, Addison-Wesley, New York. Rose, B.D.; Baugh, J.W., Jr. (1993) Parametric study of a pulse control algorithm with time delays. Technical Report CE-302-93, Department of Civil Engineering, North Carolina State University, Raleigh, NC, August Bennett, S. (1988) Real-Time Computer Control: An Introduction, Prentice-Hall International Series in System and Control Engineering. Prentice-Hall, Englewood Cliffs, NJ Juang, J.N.; Papa, R.S. (1984) An eigensystem realization algorithm (ERA) for modal parameter identification and model reduction. In NASA/JPL Workshop on Identification and Control of Flexible Space Structures, 620–627, San Diego, CA Alur, R. (1991) Techniques for automatic verification of real-time systems, PhD Thesis STAN-CS-91-1378, Stanford University, Department of Computer Science, Stanford, California, August Henzinger, T.A. (1991) The temporal specification and verification of real-time systems, PhD thesis STAN-CS-91-1380, Stanford University, Department of Computer Science, Stanford, California, August Jahanian, F.; Mok, A.K.-L. (1986) Safety analysis of timing properties in real-time systems. IEEE Transactions On Software Engineering, 21, 9, September 890–904 Baugh, J.W., Jr.; Elseaidy, W.M. (1995) Real-time software development with formal models. Journal of Computing in Civil Engineering, 9, 1, 73–86 Jahanian, F.; Stuart, D.A. (1988) A method for verifying properties of Modechart specifications. In IEEE 9th Real-Time Symposium, IEEE Computer Society Press, 12–21 Moller, A.; Tofts, C. (1990) A temporal calculus of communicating systems. In Proceedings of CONCUR'90, Lecture Notes in Computer Science 458, Springer-Verlag, 401–415 Milner, R. (1989) Communication and Concurrency, Prentice-Hall, Englewood Cliffs, NJ Cleaveland, R.; Parrow, J.; Steffen, B. (1989) The Concurrency Workbench. In Proceedings of the Workshop on Automatic Verification Method of Finite-State Systems, Lecture Notes in Computer Science 407, Springer-Verlag, 24–37 Cleaveland, R.; Parrow, J.; Steffen, B. (1989) A semantics based verification tool for finite state systems. In Proceedings of the Ninth International Symposium on Protocol Specification, Testing, and Verification. North-Holland, Amsterdam Moller, F. (1991) The Edinburgh Concurrency Workbench (Version 6.0). Technical report, Department of Computer Science, University of Edinburgh Stirling, C. (1989) An introduction to modal and temporal logic for CCS. In Joint UK/Japan Workshop on Concurrency, Lecture Notes in Computer Science 491, Springer-Verlag, Berlin, 2–20 Schutz, W. (1993) The Testability of Distributed Real-Time Systems, Kluwer Academic Publishers, Boston Baugh, J.W., Jr.; Elseaidy, W.M. (1993) Verification of real-time software for active structural control. In Computing in Civil and Building Engineering: Proceedings of the Fifth International Conference (Cohn, L.F., Editor), American Society of Civil Engineers (ASCE), 1672–1679 Baugh, J.W., Jr.; Elseaidy, W.M. (1994) Timing analysis of a multiprocessor architecture for active control. In Analysis and Computation; Proceedings of the Eleventh Conference (Cheng, F.Y., Editor), American Society of Civil Engineers, 203–212