Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Các hệ thống phân tán phụ thuộc thời gian: chứng minh tính an toàn, tính sống còn và các thuộc tính thời gian thực
Tóm tắt
Hầu hết các hệ thống giao thức truyền thông sử dụng bộ định thời để thiết lập các ràng buộc thời gian thực giữa các sự kiện xảy ra. Những hệ thống như vậy được gọi là phụ thuộc thời gian nếu các ràng buộc thời gian thực là rất quan trọng cho sự hoạt động đúng đắn của chúng. Chúng tôi trình bày một mô hình để xác định và xác minh các hệ thống phân tán phụ thuộc thời gian. Chúng tôi xem xét các mạng của các quy trình giao tiếp với nhau thông qua việc truyền thông điệp. Mỗi quy trình có một tập hợp các biến trạng thái và một tập hợp các sự kiện. Một sự kiện được mô tả bởi một tiền đề liên quan đến các giá trị của các biến trạng thái mạng ngay trước và ngay sau khi sự kiện xảy ra. Tiền đề bao gồm các đặc tả về cả điều kiện kích hoạt và hành động của sự kiện. Các quy tắc suy diễn cho cả thuộc tính an toàn và sống còn được trình bày. Các thuộc tính tiến triển thời gian thực có thể được xác minh như các thuộc tính an toàn. Chúng tôi minh họa với ba giao thức truyền dữ liệu cửa sổ trượt sử dụng số thứ tự modulo-2. Giao thức đầu tiên hoạt động trên các kênh chỉ mất tin nhắn. Đây là một giao thức không phụ thuộc thời gian. Hai giao thức thứ hai và thứ ba hoạt động trên các kênh có tình trạng mất, sắp xếp lại và trùng lặp các tin nhắn. Để hoạt động đúng đắn của chúng, cần thiết rằng các tin nhắn trong các kênh có thời gian sống giới hạn. Đây là các giao thức phụ thuộc thời gian.
Từ khóa
#giao thức truyền thông #hệ thống phân tán #ràng buộc thời gian thực #thuộc tính an toàn #thuộc tính sống còn #tiến trình thời gian thực.Tài liệu tham khảo
Bartlett KA Scantlebury RA, Wilkinson PT (1969) A note on reliable full-duplex transmission over half-duplex links. Commun ACM (May 1969)
Chandy KM, Misra J (1986) An example of stepwise refinement of distributed programs. ACM Trans Program Lang Syst, vol. 8, no. 3 (July 1986)
Clark DD (1983) Protocol implementation: practical considerations. ACM SIGCOMM'83 Tutorial, University of Texas at Austin (March 1983)
Dijkstra EW (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs, NJ
Francez N, Pnueli A (1978) A proof method for cyclic Programs. Acta Inf 9:133–157
Hailpern BT, Owicki SS (1983) Modular verification of computer communication protocols. IEEE Trans Commun, COM-31, 1 (January 1983)
IEEE Project 802 Local Area Network Standards. CSMA/CD access method and physical layer specifications. Draft IEEE Standard 802.3, Revision D (December 1982)
International Standards Organization (1979) Data communication —High-level data link control procedures — frame structure. Ref. No. ISO 3309 (2nd edn). Data communications — HDLC procedures — Elements of procedures. Ref. No. ISO 4335 (1st edn). International Standards Organization, Geneva, Switzerland
International Standards Organization (1984) Information processing systems-Open systems interconnection — Transport protocol specifications. Ref. No. ISO/TC 97/SC 16 N 1990, DIS 8073 Rev (September 1984)
Knuth DE (1973) The art of computer programming, vol 1: fundamental algorithms (2nd edn). Addison-Wesley, p 20
Knuth DE (1981) Verification of link-level protocols. BIT 21:31–36
Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21 (7):558–565
Lamport L (1982) An assertional correctness proof of a distributed algorithm. Sci Comput Program 2:175–206
Lamport L (1983) Specifying concurrent program modules. ACM Trans Program Lang 5 (2):190–222
Lamport L (1983) What good is temporal logic? Proc IFIP 9th World Congress, IFIP, North Holland, Paris (September 1983)
Lamport L (1986) Specification simplified. Preliminary Draft, Digital Equipment Corporation (May 1986)
Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Software Eng Vol SE-7, No 4 (July 1981)
Owicki S, Gries D (1976) Verifying properties of parallel programs: an axiomatic approach. Commun ACM, vol 19, na 5 (May 1976)
Owicki S, Lamport L (1982) Proving liveness properties of concurrent programs. ACM TOPLAS 4 (3):455–495
Postel J (ed) (1980) DOD standard transmission control protocol. Defense Advanced Research Projects Agency, Information Processing Techniques Office, RFC 761, IEN 129. ACM Computer Communication Review 10(4):52–132
Shankar AU, Lam SS (1983) An HDLC protocol specification and its verification using image protocols. ACM Trans Comput Syst 1 (4):331–368
Shankar AU, Lam SS (1984) Time-dependent communication protocols. In: Lam S (ed) Tutorial: principles of communication and networking protocols. IEEE Computer Society
Shankar AU, Lam SS (1985) Time-dependent distributed systems: proving safety, liveness and real-time properties. Tech Rep CS-TR-1586, Comput Sci Dept, Univ Maryland, also TR-85-24, Comput Sci Dept, Univ Texas October 1985
Shankar AU, Lam SS (1986) Construction of sliding window protocols. Tech Rep CS-TR-1647, Comput Sci Dept Univ Maryland, also TR-86-09, Comput Sci Dept, Univ Texas (March 1986)
Shankar AU (1986) A verified sliding window protocol with variable flow control. Proc ACM SIGCOMM '86, Stowe, Vermont (August 1986), also Tech Rep CS-TR-1638, Comput Sci Dept Univ Maryland
Sloan L (1983) Mechanisms that enforce bounds on packet lifetimes. ACM Trans Comput Syst 1 (4):311–330
Stenning NV (1976) A data transfer protocol. Comput Networks 1:99–110