Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Một khung pháp lý chính thức để xác minh hệ thống nhúng phân tán dựa trên các phương pháp trừu tượng
Tóm tắt
Bài báo này trình bày một khung pháp lý chính thức để xác minh các hệ thống nhúng phân tán. Một hệ thống nhúng được mô tả như một tập hợp các chức năng đồng thời theo thời gian thực, tương tác thông qua một mạng lưới các công tắc được kết nối, liên quan đến các hàng đợi tin nhắn và dịch vụ định tuyến. Để cho phép xác minh yêu cầu, mô hình như vậy sau đó được chuyển đổi thành các tự động thời gian. Tuy nhiên, độ phức tạp vốn có trong các hệ thống nhúng phân tán thường không cho phép áp dụng các kỹ thuật kiểm tra mô hình. Do đó, bài báo trình bày một phương pháp xác minh dựa trên trừu tượng, trong đó việc trừu tượng mạng lưới giao tiếp bằng các kênh thời gian đầu cuối. Để chứng minh một thuộc tính an toàn nhất định φ yêu cầu (1) chứng minh một tập hợp nghĩa vụ chứng minh đảm bảo tính đúng đắn của bước trừu tượng (tức là các kênh đầu cuối trừu tượng chính xác mạng lưới), và (2) chứng minh φ ở cấp độ trừu tượng. Lợi thế mong đợi của phương pháp này nằm ở khả năng vượt qua sự bùng nổ tổ hợp thường gặp khi xác minh các hệ thống phức tạp. Phương pháp này được minh họa bằng một nghiên cứu tình huống hàng không.
Từ khóa
#hệ thống nhúng #hệ thống phân tán #xác minh #trừu tượng #tự động thời gianTài liệu tham khảo
Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Proceedings of the 18th Conference Foundation of Software Technology and Theoretical Computer Science (FST & TCS’98), Chennai, India, December 1998, vol. 1530, pp. 245–256. Springer, Berlin Heidelberg New York (1998)
Aceto L., Burgueño A., Larsen K.G. (1998) Model checking via reachability testing for timed automata. In: Steffen B. (eds). TACAS’98, LNCS 1384. Springer, Berlin Heidelberg New York, pp. 263–280
Alur R., Courcoubetis C., Dill D.L. (1993) Model-checking in dense real-time. Inf. Comput. 104(1): 2–34
Alur R., Dill D.L. (1994) A theory of timed automata. Theor. Comput. Sci. 126(2): 183–235
Bozga M., Daws C., Maler O., Olivero A., Tripakis S., Yovine S. (1998) Kronos: a model-checking tool for real-time systems. In: Hu A.J., Vardi M.Y. (eds). Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, Canada, vol. 1427. Springer, Berlin Heidelberg New York, pp 546–550
Burgueño-Arjona, A.: Verification and Synthesis of Timed Systems using Parametric Analysis and Observation Methods. PhD thesis, Ecole Nationale Supérieure de l’aéronautique et de l’espace (1998)
Cruz R.L. (1991) Calculus for network delay-part. I: Network elements in isolation. IEEE Trans. Inform. Theor. 37(1): 114–131
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaal. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS ’97). IEEE Computer Society (1997)
Henzinger T.A., Ho P.-H., Wong-Toi H. (1997) HYTECH: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transfer 1(1–2): 110–122
Jain R. (1991) The Art of Computer Systems Performance Analysis - techniques for Experimental Design, Measurement, Simulation and Modeling. Wiley, New York
Kleinrock L. (1975) Queueing systems—volume 1: theory. Wiley, New york
Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Proceedings of the IFIP Joint International Conference Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV’98), Paris, France, Nov. 1998, pp. 439–456. Kluwer, Dordrecht (1998)
Larsen K.G., Pettersson P., Yi W. (1997) UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer, 1(1–2): 134–152
Le Boudec, J.Y. Thirian, P.: Network Calculus—a theory for Deterministic Queueing Systems for the Internet, vol. LNCS 2050. Springer Berlin Heidelberg New York.
Schnoebelen P. et al. (2001) Systems and Software Verification Model-Checking Techniques and Tools. Springer, Berlin Heidelberg Newyork
Starobinski, D., Karpovsky, M., Zakrevski, L.: Application of network calculus to general topologies using turn-prohibition (2002)