UPPAAL

UPPAAL là một môi trường công cụ tích hợp cho mô hình, xác nhận và xác minh của các hệ thống thời gian thực mô hình hóa như các mạng của automata timed, mở rộng với các kiểu dữ liệu (số nguyên có giới hạn, mảng, vv).
UPPAAL CORA là một chi nhánh của UPPAAL cho chi phí tối ưu reachability Anslysis phát triển bởi đội UPPAAL như là một phần của dự án VHS và Ametist. Trong khi UPPAAL hỗ trợ mô hình kiểm tra của automata timed, UPPAAL CORA sử dụng một phần mở rộng của máy tự động hẹn giờ gọi LPTA. LPTA cho phép bạn chú thích các mô hình với các khái niệm về chi phí.
Điều này có thể là chi phí của sự chậm trễ trong các tình huống nhất định hoặc chi phí của các hành động cụ thể. UPPAAL CORA sau đó tìm thấy con đường tối ưu phù hợp với điều kiện mục tiêu.
UPPAAL CORA đã được sử dụng trong một số nghiên cứu trường hợp. Một số trong số này được mô tả trên các trang nghiên cứu trường hợp của trang web này. Nếu bạn đến với công dụng thú vị, xin vui lòng liên hệ với chúng tôi. Chúng tôi rất muốn nghe những gì bạn làm!
Do cấu trúc dữ liệu nội bộ khác nhau, UPPAAL CORA hiện nay bao gồm hai phiên bản khác nhau:
Một phiên bản dành cho các trường hợp đơn giản của thời gian phân tích reachability tối ưu.
Một phiên bản dành cho các ngôn ngữ đầy LPTA.
Giống như UPPAAL, UPPAAL CORA là miễn phí cho sử dụng phi lợi nhuận, ví dụ như để đánh giá, nghiên cứu, và mục đích giảng dạy.
Dưới đây là một số tính năng chính của "UPPAAL":
Mạnh
 
· Các ngôn ngữ mô hình của UPPAAL CORA là mạnh mẽ hướng tới những thay đổi trong các vấn đề mô hình hóa. Điều này có nghĩa rằng đầu tư của bạn trong mô hình không bị mất khi các vấn đề thay đổi, vì nó rất dễ dàng để thích ứng với các mô hình hiện có.
 
Nhanh
 
· Mặc dù công nghệ khá mới, thử nghiệm và rất khác nhau từ các kỹ thuật được sử dụng trong nghiên cứu hoạt động truyền thống, UPPAAL CORA là cạnh tranh trong một số nghiên cứu trường hợp.
 
Tương hợp
 
· Ngôn ngữ của UPPAAL CORA là một siêu của UPPAAL. Bất kỳ mô hình UPPAAL hợp lệ cũng là một mô hình UPPAAL CORA hợp lệ. Điều này làm cho nó dễ dàng và thuận tiện để tái sử dụng và thích ứng với mô hình hiện tại của bạn để UPPAAL CORA.
 
Hiện tại
 
· UPPAAL CORA được dựa trên các phiên bản phát triển nội bộ mới nhất của UPPAAL, chứa những cải tiến hiệu suất và ngôn ngữ mới nhất. Tuy nhiên nó là một công cụ thí nghiệm và thiếu nhiều tính năng xác minh của UPPAAL.
Hạn chế:
UPPAAL CORA với sự hỗ trợ đầy đủ LPTA có một số hạn chế. Những hạn chế này không phải là cơ bản, nhưng là kết quả của việc sử dụng các cấu trúc dữ liệu nội bộ mới với một bộ tính năng hiện còn hạn chế. Theo thời gian, những hạn chế này sẽ được giải quyết.
- Không có ngoại suy, do đó chấm dứt không được bảo đảm, trừ khi bạn đảm bảo rằng một trong hai:
· Hệ thống này là mạch hở.
· Tất cả các đồng hồ được bao bọc bởi bất biến.
- Đơn giản chỉ reachability:
· Không có kiểm tra liveness
· Không có kiểm tra bế tắc
- Sử dụng giới hạn của bản hướng dẫn:
· Hỗ trợ (chi phí + còn lại) phân loại được thực hiện (tốt nhất tìm kiếm đầu tiên)
· Hỗ trợ cho biến heuristic, được thực hiện, nhưng sự biểu hiện không có thể tham khảo các biến chi phí.
Có gì mới trong phiên bản này:
· Phiên bản này sửa lỗi crash và rò rỉ bộ nhớ.