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]. //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: //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
10:00 | 19/06/2024
Ngày 18/6, tại Thừa Thiên Huế, Cục Cơ yếu Đảng - Chính quyền, Ban Cơ yếu Chính phủ đã tổ chức triển khai máy tính an toàn đa giao diện có cài đặt sản phẩm mật mã - MTCD-3M (3M) và tập huấn, hướng dẫn quản lý, sử dụng máy 3M cho cán bộ, chuyên viên các phòng chuyên môn thuộc Văn phòng Tỉnh ủy và văn thư các cơ quan tham mưu giúp việc Tỉnh ủy.
09:00 | 13/06/2024
Trong phạm vi của bài báo này, chúng tôi sẽ trình bày những nội dung xoay quanh các vấn đề về sự tác động của trí tuệ nhân tạo (AI) cùng với hậu quả khi chúng ta tin tưởng tuyệt đối vào sức mạnh mà nó mang tới. Cũng như chúng tôi đề xuất sự cần thiết của việc xây dựng và hoàn thiện các chính sách bảo vệ các nội dung do AI tạo ra tuân thủ pháp luật và bảo vệ người dùng.
19:00 | 30/04/2024
Theo báo cáo năm 2022 về những mối đe doạ mạng của SonicWall, trong năm 2021, thế giới có tổng cộng 623,3 triệu cuộc tấn công ransomware, tương đương với trung bình có 19 cuộc tấn công mỗi giây. Điều này cho thấy một nhu cầu cấp thiết là các tổ chức cần tăng cường khả năng an ninh mạng của mình. Như việc gần đây, các cuộc tấn công mã độc tống tiền (ransomware) liên tục xảy ra. Do đó, các tổ chức, doanh nghiệp cần quan tâm hơn đến phương án khôi phục sau khi bị tấn công.
10:00 | 22/03/2024
Với sự tương tác kinh tế, xã hội và văn hóa ngày càng diễn ra phổ biến trên Internet, nhu cầu ngày càng tăng trong vài thập kỷ qua nhằm bắt chước sự ngẫu nhiên của thế giới tự nhiên và tạo ra các hệ thống kỹ thuật số để tạo ra các kết quả không thể đoán trước. Các trường hợp sử dụng cho tính không thể đoán trước này bao gồm đưa vào sự khan hiếm nhân tạo, xây dựng các cơ chế bảo mật mạnh mẽ hơn và tạo điều kiện cho các quy trình ra quyết định trung lập đáng tin cậy. Trong bài viết này, tác giả sẽ phân tích tính ngẫu nhiên, tìm hiểu về các loại ngẫu nhiên và vai trò quan trọng của sự ngẫu nhiên đối với Blockchain và hệ sinh thái Web3.
14:00 | 11/09/2024|Công nghệ PKI
11:00 | 03/09/2024|GP ATM
08:00 | 26/08/2024|GP ATM
10:00 | 19/08/2024|Tin tức sản phẩm
Trong thời đại ngày nay, cùng với sự phát triển của khoa học kỹ thuật có ngày càng nhiều những cuộc tấn công vào phần cứng và gây ra nhiều hậu quả nghiêm trọng. So với các loại tấn công khác, tấn công qua kênh kề đang được nghiên cứu do khả năng khôi phục lại khóa bí mật trong khi hệ thống vẫn hoạt động bình thường mà không hề làm thay đổi phần cứng. Bài báo này sẽ trình bày một cách sơ lược về những kết quả cuộc tấn công kênh kề lên mã hóa RSA cài đặt trên điện thoại thông minh sử dụng hệ điều hành Android tại Viện Khoa học - Công nghệ mật mã. Nhóm tác giả đã tấn công khôi phục được một phần khóa bí mật của mã hóa RSA cài đặt trên điện thoại thông minh và chứng minh khả năng rò rỉ thông tin qua kênh kề.
14:00 | 11/09/2024
Cục An toàn thông tin vừa phát đi cảnh báo về chiêu trò lừa đảo mới mạo danh cơ quan an sinh xã hội, dụ người dân nhận tiền hỗ trợ, trợ cấp... Tuy nhiên, đằng sau những lời "có cánh" lại là cái bẫy tinh vi nhằm chiếm đoạt tài sản.
10:00 | 30/10/2024
