Xây dựng công cụ sinh dữ liệu thử cho chương trình Lustre/SCADE dựa trên kiểm chứng mô hình

##plugins.themes.academic_pro.article.main##

Author

  • Trịnh Công Duy*; Nguyễn Thanh Bình

Từ khóa:

reactive system
model checker
testing
trap propertive
Lustre/SCADE
generate test cases

Tóm tắt

Lustre/SCADE là ngôn ngữ được sử dụng rộng rãi để phát triển phần mềm cho các hệ thống phản ứng, một lĩnh vực mà chất lượng phần mềm được yêu cầu hết sức nghiêm ngặt, gần như là không được phép xảy ra bất cứ một lỗi nhỏ nào. Bên cạnh đó, đối với những ứng dụng trong lĩnh vực này, việc kiểm thử thủ công sẽ rất khó thực hiện và không mang lại hiệu quả, do đó yêu cầu cần phải tự động hóa hoạt động kiểm thử cho các ứng dụng Lustre/SCADE. Trong bài báo này, chúng tôi tập trung nghiên cứu việc kiểm thử tự động cho các ứng dụng Lustre/SCADE. Chúng tôi đề xuất sử dụng kỹ thuật kiểm chứng mô hình trên trên mạng lưới toán tử (operator network) để sinh ra các dữ liệu thử một cách tự động. Cuối cùng, chúng tôi ứng dụng giải pháp này để xây dựng công cụ sinh dữ liệu thử cho chương trình Lustre/SCADE và minh họa trên một chương trình cụ thể

Tài liệu tham khảo

    [1] A. Lakehal and I. Parissis, “Lustructu: A Tool for the Automatic Coverage Assessment of Lustre Programs”, in IEEE International Symposium on Software Reliability Engineering, (Chicago, Illinois, USA), (2005).
    [2] Abdesselam Lakehal, Ioannis Parissis. Structural Coverage Criteria for Lustre/SCADE Programs. Software Testing, Verification & Reliability, John Wiley and Sons Ltd (2009).
    [3] Albert Benveniste, Gerard Berry. The Synchronous Approach to Reactive and Real-Time Systems. Proceedings of the IEEE (1991).
    [4] Esterel Technologies website: http://esterel-technologies.com.
    [5] Gordon Fraser, FranzWotawa, Paul E. Ammann. Testing with model checkers: A survey, Competence Network Softnet Austria, Austria (2007).
    [6] Karolina Zurowska and Juergen Di. Model-based generation of test cases for reactive systems. Applied Formal Methods Group School of Computing Queen’s University Kingston, Ontario, Canada, June (2010).
    [7] L. duBousquet, F. Ouabdesselam, J.- L.Richier, and N. Zuanon. Lutess: testing environment for synchronous software. Advances in Computing Science, Springer (1998).
    [8] Nicolas Halbwachs, Pascal Raymond. Validation of Synchronous Reactive Systems: from Formal Verication to Automatic Testing. Grenoble, France (1999).
    [9] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice, “LUSTRE: A Declarative Language for Programming Synchronous Systems”, in ACM Symposium on Principles of Programming Languages, (Munich, Germany) (1987).
    [10] Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis. Automatic Generation of Test Cases in Regression Testing for Lustre/SCADE. Journal of Software Engineering and Applications, Vol. 6 (2013).
    [11] Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis. Automatic generation of test cases in regression testing for Reactive Systems. FAIR 2013, Hue, Vietnam (2013).
Xem thêm

##plugins.themes.academic_pro.article.sidebar##

Đã Xuất bản

Sep 30, 2015
Download
PDF
Cách trích dẫn
Trinh Cong Duy*; Nguyen Thanh Binh. “Xây dựng công cụ Sinh dữ liệu thử Cho chương trình Lustre/SCADE dựa Trên kiểm chứng Mô hình”. Tạp Chí Khoa học Và Công nghệ - Đại học Đà Nẵng, vol 9, số p.h 94, Tháng Chín 2015, tr 84-89, https://jst-ud.vn/jst-ud/article/view/84-89.

##plugins.themes.academic_pro.article.details##