Tóm tắt - Bài báo này đề xuất một phương pháp để mô hình hóa và kiểm chứng biểu đồ trình tự UML 2.0 sử dụng SPIN/ PROMELA. Ý tưởng chính của phương pháp là xây dựng các mô hình mô tả hành vi của từng đối tượng trong biểu đồ trình tự UML 2.0. Các mô hình này biểu diễn dưới dạng các ôtômát vào/ra nhằm giữ nguyên tính tương tác giữa các đối tượng. Nghiên cứu đưa ra một kỹ thuật hỗ trợ chuyển đổi các mô hình này thành các đặc tả PROMELA để cung cấp cho bộ công cụ SPIN nhằm kiểm chứng tính đúng đắn của các biểu đồ tuần tự. Bằng cách đảm bảo tính chính xác của thiết kế phần mềm, một số thuộc tính có thể được đảm bảo như an toàn, ổn định và thực tế là không còn lỗ hổng nào. Một công cụ hỗ trợ cho phương pháp đề xuất cũng được cài đặt và thực nghiệm với một số hệ thống điển hình nhằm minh chứng cho tính đúng đắn, hiệu quả và dễ sử dụng. Cách tiếp cận này hứa hẹn sẽ được áp dụng trong thực tế.
REFERENCES[1]. ALAWNEH, L., DEBBABI, M., HASSAINE, F., JARRAYA, Y., & SOEANU, A., “A unified approach for verification and validation of systems and software engineering models”, In 13th Annual IEEE International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS'06), pp. 409-418, 2006. [2]. BAIER, C., KATOEN, J. P., LARSEN, K. G., “Principles of model checking”, MIT Press, 2008. [3]. CLARKE, E. M., GRUMBERG, O., PELED, D., “Model checking”. MIT press, 1999. [4]. COBLEIGH, J. M., GIANNAKOPOULOU, D., PĂSĂREANU, C. S., “Learning assumptions for compositional verification”, In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 331-346, 2003. [5]. GRØNMO, R., MØLLER-PEDERSEN, B., “From UML 2 Sequence Diagrams to State Machines by Graph Transformation”. Journal of Object Technology, 10(8), 1-22, 2011. [6]. GUELFI, N., MAMMAR, A., “A formal semantics of timed activity diagrams and its PROMELA translation”, In 12th Asia-Pacific Software Engineering Conference, 2005. [7]. H. M. DUONG, L. K. TRINH, P. N. HUNG, “An Assume-Guarantee Model Checker for Component-Based Systems”, In IEEE-RIVF, pp. 22-26, 2013. [8]. JUSSILA, T., DUBROVIN, J., JUNTTILA, T., LATVALA, T., PORRES, I., & LINZ, J. K. U., “Model checking dynamic and hierarchical UML state machines”, Proc. MoDeV2a: Model Development, Validation and Verification, pp. 94-110, 2006. [9]. KNAPP, A., WUTTKE, J., “Model checking of UML 2.0 interactions”, In International Conference on Model Driven Engineering Languages and Systems, pp. 42-51, 2006. [10]. L. C. LUAN, P. N. HUNG, “A method for model generation from UML 2.0 sequence diagrams”, Proc. FAIR’9, Can Tho, pp. 619-625, 2016. [11]. LATELLA, D., MAJZIK, I., & MASSINK, M., “Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker”, Formal aspects of computing, 11(6), pp. 637-664, 1999. [12]. LIMA, V., TALHI, C., MOUHEB, D., DEBBABI, M., WANG, L., POURZANDI, M., “Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages”, Electronic Notes in Theoretical Com. Science, 254, pp.143-160, 2009. [13]. MIKK, E., LAKHNECH, Y., SIEGEL, M., & HOLZMANN, G. J. (1998). “Implementing statecharts in PROMELA/SPIN”, In Industrial Strength Formal Specification Techniques, Proc. 2nd IEEE Workshop, pp. 90-101, 1998. [14]. P. N. HUNG, T. KATAYAMA, “Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software”, In the 15th Asia-Pacific Software Engineering Conference, IEEE Computer Society Press, pp. 479-486, 2008. [15]. SCHÄFER, T., KNAPP, A., MERZ, S., “Model checking UML state machines and collaborations”, Electronic Notes in Theoretical Com. Sci., 55(3), pp.357-369, 2001. [16]. SIVERONI, I., ZISMAN, A., SPANOUDAKIS, G., “Property specification and static verification of UML models”, In Availability, Reliability and Security, pp. 96-103, 2008. [17]. VAN AMSTEL, M. F., LANGE, C. F., & CHAUDRON, M. R., “Four automated approaches to analyze the quality of UML sequence diagrams”. In Computer Software and Applications Conf., pp. 415-424, 2007. [18]. ZHANG, C. & DUAN, Z., “Specification and Verification of UML 2.0 Sequence Diagrams Using Event Deterministic Finite Automata”, in 'SSIRI (Companion)', IEEE Computer Society, pp. 41-46, 2011. [19]. OMG Unified Modeling Language. [Online]. http://www.omg.org/spec/UML/2.5/PDF. [20]. HOLZMANN, GERARD J (1997). "The model checker SPIN." IEEE Transactions on software engineering 23.5: 279. [21]. Basic SPIN Manual. [Online]. Available: http://spinroot.com/spin/Man/Manual.html |
Thông tin trích dẫn: PhD. Chi Luan Le, “A Method for Modeling and Verifying of UML 2.0 Sequence Diagrams using SPIN”, Nghiên cứu khoa học và công nghệ trong lĩnh vực An toàn thông tin, Tạp chí An toàn thông tin, Vol. 09, pp. 20-28, No. 01, 2019.
PhD. Chi Luan Le
22:00 | 22/02/2020
14:00 | 09/06/2020
09:00 | 28/05/2020
22:00 | 22/02/2020
17:00 | 27/05/2019
14:00 | 23/02/2024
SSH (Secure Socket Shell) là giao thức mạng để đăng nhập vào một máy tính từ xa trên một kênh truyền an toàn. Trong đó, OpenSSH là một chuẩn SSH được sử dụng ở hầu hết các bản phân phối của Linux/BSD như Ubuntu, Debian, Centos, FreeBSD, mã hóa tất cả các thông tin trên đường truyền để chống lại các mối đe dọa như nghe lén, dò mật khẩu và các hình thức tấn công mạng khác. Trong bài viết này sẽ hướng dẫn độc giả cách thức tăng cường bảo mật cho OpenSSH với một số thiết lập bảo mật và cấu hình tùy chọn cần thiết nhằm đảm bảo truy cập từ xa vào máy chủ Linux được an toàn.
08:00 | 10/02/2024
Hệ thống mật mã RSA là một trong các hệ mật mã khóa công khai đang được sử dụng rất phổ biến trong hệ thống mạng máy tính hiện nay. Việc lựa chọn tham số an toàn cho hệ mật RSA là vấn đề rất quan trọng trong cài đặt ứng dụng hệ mật này. Bài báo này trình bày chi tiết về khuyến nghị độ dài các tham số sử dụng cho hệ thống mật mã RSA như thừa số modulo, số mũ bí mật, số mũ công khai và các thừa số nguyên tố trong một số tiêu chuẩn mật mã của châu Âu, Đức và Mỹ.
09:00 | 17/11/2023
Theo Cục An toàn thông tin (Bộ TT&TT), hiện nay có 24 hình thức lừa đảo qua mạng phổ biến mà các đối tượng lừa đảo nhắm vào người dân. Để tránh trở thành nạn nhân, người dân cần nắm bắt, tuyên truyền cho người thân, bạn bè, đồng nghiệp của mình.
14:00 | 14/08/2023
Xu hướng số hóa đã mang lại nhiều lợi ích cho ngành công nghiệp sản xuất, nhưng nó cũng bộc lộ những lỗ hổng trong hệ thống công nghệ vận hành (Operational Technology - OT) được sử dụng trong những môi trường này. Khi ngày càng có nhiều hệ thống điều khiển công nghiệp (Industrial Control System - ICS) được kết nối với Internet, nguy cơ tấn công mạng nhằm vào các hệ thống này sẽ càng tăng lên. Nếu các hệ thống này bị xâm phạm, nó có thể dẫn đến những hậu quả nghiêm trọng, chẳng hạn như ảnh hưởng sản xuất, bị mất cắp dữ liệu, hư hỏng vật chất đối với thiết bị, nguy hiểm cho môi trường làm việc và thậm chí gây hại đến tính mạng con người. Chính vì vậy, việc đưa ra các lưu ý giúp tăng cường bảo mật OT trong môi trường công nghiệp sản xuất trở nên vô cùng quan trọng.
08:00 | 11/01/2024 | Chính sách - Chiến lược
09:00 | 10/01/2024 | Giải pháp khác
09:00 | 05/01/2024|Chính sách - Chiến lược
09:00 | 05/01/2024|An ninh – Quốc Phòng
Lược đồ chữ ký số dựa trên hàm băm là một trong những lược đồ chữ ký số kháng lượng tử đã được Viện Tiêu chuẩn và Công nghệ Quốc gia Mỹ (NIST) chuẩn hóa trong tiêu chuẩn đề cử FIPS 205 (Stateless Hash Based Digital Signature Standard) vào tháng 8/2023. Bài báo này sẽ trình bày tổng quan về sự phát triển của của lược đồ chữ ký số dựa trên hàm băm thông qua việc phân tích đặc trưng của các phiên bản điển hình của dòng lược đồ chữ ký số này.
09:00 | 01/04/2024
Mới đây, Cơ quan An ninh mạng và Cơ sở hạ tầng Hoa Kỳ (CISA) đã phát hành phiên bản mới của hệ thống Malware Next-Gen có khả năng tự động phân tích các tệp độc hại tiềm ẩn, địa chỉ URL đáng ngờ và truy tìm mối đe dọa an ninh mạng. Phiên bản mới này cho phép người dùng gửi các mẫu phần mềm độc hại để CISA phân tích.
13:00 | 17/04/2024
