Inh dữ liệu thử cho ứng dụng Lustre/Scade sử dụng điều kiện kích hoạt

Kỷ yếu Hội nghị Quốc gia lần thứ VIII về Nghiên cứu cơ bản và ứng dụng Công nghệ thông tin (FAIR); Hà Nội, ngày 9-10/7/2015 DOI: 10.15625/vap.2015.000202 SINH DỮ LIỆU THỬ CHO ỨNG DỤNG LUSTRE/SCADE SỬ DỤNG ĐIỀU KIỆN KÍCH HOẠT Trịnh Công Duy1, Nguyễn Thanh Bình1, Ioannis Parissis2 1 Trường Đại học Bách Khoa, Đại học Đà Nẵng, Đà Nẵng, Việt Nam 2 Viện Đại học Bách khoa Grenoble, Cộng hòa Pháp. tcduy@dut.udn.vn, ntbinh@dut.udn.vn, ioannis.parissis@grenoble-inp.fr TÓM TẮT - Kiểm thử là một trong những hoạt động quan trọng trong tiến trình phát triển phần mềm. Phần mềm phát triển ngày càng phức tạp, yêu cầu chất lượng ngày càng cao hơn, vai trò kiểm thử càng quan trọng hơn, đặc biệt là trong phát triển phần mềm cho các hệ thống phản ứng. Hệ thống phản ứng được phát triển phổ biến trong các lĩnh vực như hàng không, năng lượng, hạt nhân Những hệ thống này thường yêu cầu rất cao về chất lượng và đòi hỏi các hoạt động kiểm thử nghiêm ngặt trước khi chúng được triển khai sử dụng. 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. Điều này đòi hỏi việc kiểm thử phải được tiến hành thường xuyên và liên tục khi có bất cứ sự thay đổi nào trên ứng dụng. 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 kỹ thuật sử dụng các điều kiện kích hoạt 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. Trong đó, kỹ thuật kiểm chứng mô hình (model checking) được sử dụng trong việc sinh tự động các dữ liệu thử này. Cuối cùng, chúng tôi thử nghiệm giải pháp này trên một chương trình Lustre/SCADE trong hệ thống điều khiển nhiệt độ môi trường. Từ khóa - Hệ thống phản ứng; Kiểm chứng mô hình; Kiểm thử; Thuộc tính bẫy; Lustre/SCADE; Sinh dữ liệu thử. I. GIỚI THIỆU Việc phát hiện và khắc phục lỗi cho các phần mềm là một công việc đòi hỏi nhiều nỗ lực và chi phí trong phát triển phần mềm. Hiện nay, phần mềm đang được ứng dụng ngày càng rộng rãi trong nhiều lĩnh vực, do đó chất lượng phần mềm ngày càng được quan tâm. Trong công nghệ phần mềm, kiểm thử là hoạt động cơ bản nhằm phát hiện các lỗi của phần mềm. Trong đó, kiểm thử tự động nhằm xử lý một cách tự động quy trình kiểm thử, sinh ca kiểm thử, thực thi kiểm thử và đánh giá kết quả kiểm thử. Hệ thống phản ứng (reactive system) khi hoạt động đáp ứng (phản ứng) với các sự kiện bên ngoài [3]. Chẳng hạn, các hệ thống sinh học là những hệ thống phản ứng, bởi vì nó phản ứng với các sự kiện nhất định. Tuy nhiên, trong tin học và điều khiển, thuật ngữ này được sử dụng chủ yếu để mô tả các hệ thống nhân tạo. Hệ thống phản ứng liên tục tương tác với môi trường và thực thi theo yếu tố tác động bởi môi trường. Ở một khía cạnh trừu tượng thì nó được xem là một hộp đen, ta cung cấp các giá trị đầu vào thì hệ thống sẽ cho ra các giá trị đầu ra thích hợp. Các hệ thống phản ứng có thể được xem là đang ở một trạng thái nhất định và đợi thông tin đầu vào (input). Với mỗi đầu vào, chúng thực hiện tính toán và sinh đầu ra (output) và chuyển sang một trạng thái mới. Thông thường, các hệ thống nhúng và các hệ thống điều khiển cũng là các hệ thống phản ứng [2]. Lập trình đồng bộ (synchronous programming) [3] đã được giới thiệu vào cuối những năm 80 như là một phương pháp tiếp cận để thiết kế các hệ thống phản ứng. Kể từ đó, nó đã được sử dụng rộng rãi, chủ yếu trong lĩnh vực yêu cầu độ an toàn cao như hệ thống điện tử, vận tải, sản xuất năng lượng (các hệ thống phản ứng). Một lợi thế quan trọng của cách tiếp cận đồng bộ này là nhằm cung cấp một khuôn khổ chính thức, hiệu quả và đồng nhất cho các hoạt động phát triển - thiết kế, cài đặt và xác minh. Một số ngôn ngữ lập trình, đặc biệt đối với các ngôn ngữ sử dụng phương pháp tiếp cận đồng bộ như Esterel, Signal hoặc Lustre [4]. SCADE (Safety Critical Application Development Environment) là những công cụ thương mại dựa trên các mô hình đồng bộ và ngôn ngữ lập trình Lustre. SCADE đã được sử dụng trong các dự án quan trọng tại châu Âu (Airbus A340-600, A380, Eurocopter) và trở thành một tiêu chuẩn trong lĩnh vực này. Lustre [4] là một ngôn ngữ đồng bộ luồng dữ liệu, được thiết kế năm 1984 bởi Viện IMAG tại Grenoble. Chương trình Lustre gồm một chuỗi có thứ tự các phương trình giúp xác định phương thức dòng đầu vào được chuyển thành các dòng đầu ra thông qua một tập hợp các toán tử. Do đó, cách biểu diễn phù hợp nhất cho các chương trình Lustre là một đồ thị có hướng, gọi là mạng lưới toán tử (trong thực tế, người sử dụng không viết chương trình Lustre mà sử dụng trình soạn thảo đồ họa trong công cụ SCADE để xây dựng các mạng lưới toán tử liên quan). Việc kết hợp của cả hai mô hình đồng bộ và dòng dữ liệu, cú pháp đồ họa đơn giản, áp dụng khái niệm thời gian rời rạc là một số trong những đặc điểm chính làm cho Lustre trở thành ngôn ngữ lý tưởng cho việc xây dựng các mô hình, các thiết kế hệ thống điều khiển trong một số lĩnh vực công nghiệp, chẳng hạn như hệ thống điện tử, ô tô và năng lượng, hạt nhân nói riêng và hệ thống phản ứng nói chung. Với các hệ thống này, yếu tố an toàn (safety) được quan tâm hàng đầu. Vì vậy việc hệ thống bị lỗi khi đang vận hành sẽ gây hậu quả rất nghiêm trọng. Hơn nữa, “lỗi hệ thống” có xu hướng được phát hiện muộn trong quá trình phát triển khi mà nó đã gây ra thiệt hại đáng kể, rất khó để gỡ lỗi và tốn nhiều chi phí. Trong tiến trình phát triển phần mềm cho các hệ thống phản ứng, giai đoạn kiểm thử đóng vai trò rất quan trọng. Phần Tm t đ d ứ c c R p x th k th tr T c k d th g p c d h L c c A 1 v v n p đ v rịnh Công Duy, N ềm càng lớn ốt, ngăn ngừa Bắt đầu ó đến nay, nh Nhóm t ụng trên ngôn ng trên Lustr hí bao phủ. N ông cụ LESA inus Plasmeij hản ứng. Tiếp ây dựng tập c ử cho các ứn Nhìn ch iểm thử, kiểm ấy chưa có n ong việc kiểm Trong b rong đó, sử d hứng mô hình iểm chứng m ữ liệu thử dựa Nội dun ống phản ứn iới. Mục II tr háp sử dụng ụ kiểm chứng ụng giải pháp ướng phát tri Trong m ustre và môi ác điều kiện hứng mô hình . Tổng quan . Ngôn ngữ l Hệ thốn ới các tác độn ới các tác độ ày không thể hải tôn trọng ược xem là m ào trước đó v guyễn Thanh B và càng phức các khiếm kh từ đầu những iều công trình ác giả Laya M ngữ Lustre [ e, tuy nhiên n ăm 1999, nh R để kiểm ch er đến từ Đạ đến, nhóm t a kiểm thử c g dụng dựa tr ung các nghi thử tự động hiều nghiên thử các chư ài báo này, c ụng các điều để sinh tự đ ô hình LESA trên các kết g của bài bá g, ngôn ngữ l ình bày các cơ điều kiện kích mô hình LE này cho một ển tiếp theo. ục này chún trường SCAD kích hoạt cho trong sinh dữ về Lustre/SC ập trình Lustr g phản ứng l g từ bên ngo ng bên ngoài. đồng bộ hóa nghiêm ngặt ột chuỗi vô h à hiện tại. ình, Ioannis Paris tạp, thủ tục k uyết trước kh năm 90, lĩnh nghiên cứu đ adani ở Đại 10]. Nhóm ng ghiên cứu này óm tác giả N ứng mô hình i học Nijmege ác giả Elizabe ần thực hiện ên mô hình U ên cứu đến th các hệ thống cứu thực hiện ơng trình Lus húng tôi đề x kiện kích ho ộng các dữ l R để tiến hàn quả sinh ra từ o được tổ chứ ập trình Lustr sở lý thuyết hoạt trên mạ SAR để tạo d hệ thống cụ t g tôi trình bày E. Đồng thời một chương liệu thử. ADE e trong các h à một hệ thốn ài nó. Hệ thốn Hệ thống ph một cách hợp ràng buộc về ạn các véc tơ sis iểm thử đòi h i thực hiện ki vực nghiên c ã và đang đư học Grenobl hiên cứu này sử dụng phư icolas Halbw các hệ thống n mở rộng cô ta Fourneret ở phiên bản m ML. ời điểm hiện phản ứng v hướng tiếp c tre/SCADE. uất kỹ thuật ạt trên mạng iệu thử dựa t h kiểm chứng quá trình kiể c như sau: M e và các nghiê nền tảng sử d ng lưới toán ữ liệu thử ch hể và các kết II. CƠ cơ sở lý thuy chúng tôi cũn trình Lustre/S ệ thống phản g thay đổi hàn g này có thể ản ứng liên tụ lý với hệ th thời gian thực đầu vào và đ Hình 1. Mô ỏi tốn nhiều ểm thử ở mức ứu về kiểm th ợc thực hiện. e thực hiện ki đã xây dựng ơng thức xác achs và Pasc phản ứng [9] ng cụ kiểm th [13] ở đại họ ới, trong ngh tại tập trung à chương trìn ận sử dụng c sinh dữ liệu t lưới toán tử rên các điều k mô hình cho m chứng này. ục I giới thi n cứu về kiểm ụng trong ngh tử của một ch o các chương quả của việc SỞ LÝ TH ết của nghiên g trình bày k CADE. Và c ứng h động của n tự định hướng c phản ứng l ống. Nói cách cần đáp ứng ầu ra. Ở mỗi b hình hệ thống p thời gian và c chi tiết hơn, ử cho các hệ ểm thử tự độn công cụ Lute định ngẫu nh al Raymond đ [12]. Năm 20 ử tự động GA c Franche-Co iên cứu này vào nghiên cứ h Lustre/SCA ác điều kiện hử tự động c của chương t iện kích hoạ một chương ệu chung về b thử cho các iên cứu này. ương trình L trình Lustre/ thử nghiệm. C UYẾT cứu, bao gồm ỹ thuật xây dự uối cùng sẽ l ó với đầu ra, hoặc được đ ại với các tác khác, môi tr kịp thời [12]. ước thì giá tr hản ứng ông sức. Việ phức tạp hơn thống phản ứ g cho các ứn s[11] để kiểm iên các ca kiể ến từ Đại họ 04, nhóm tác ST để có th mté đã thực h tác giả đề xuấ u các kỹ thu DE. Tuy nhi kích hoạt trên ho các chươn rình Lustre, đ t này. Chúng trình Lustre c ài báo và trì chương trình Trong mục II ustre, kết hợp SACDE. Phầ uối cùng là p các nội dun ng mạng lướ à những nội d điều kiện và t iều khiển định động từ môi ường không Việc thực th ị đầu ra được c tìm lỗi càng và chi phí cao ng được hình g dụng phản thử các ứng m thử dựa tr c Grenoble đ giả Pieter Ko ể kiểm thử cá iện sinh ca k t kỹ thuật sin ật kiểm chứng ên, theo chún mạng lưới c g trình Lustr ồng thời sử tôi sẽ sử dụn ụ thể, từ đó nh bày tổng q Lustre/SACD I, chúng tôi đ với việc sử n IV trình bà hần kết luận g về ngôn ng i toán tử, các ung về ứng rạng thái nhằ hướng để ph trường, khi m thể chờ đợi v i của hệ thống xác định bởi 629 sớm càng hơn [1]. thành. Từ ứng và áp dụng phản ên các tiêu ã sử dụng opman và c hệ thống iểm thử và h ca kiểm mô hình, g tôi nhận ác toán tử e/SCADE. dụng kiểm g công cụ sinh ra các uan về hệ E trên thế ề xuất giải dụng công y việc ứng và đề xuất ữ lập trình lộ trình và dụng kiểm m đáp ứng ản ứng lại ôi trường à hệ thống phản ứng giá trị đầu 6đ h tr tr lĩ h tr v tr n p n ứ x c k đ đ d d s d tr g k n 30 Hình 1 ầu ra và chuy ệ thống phản ong các lĩnh Lustre ình điều khiể nh vực năng ệ thống thời g ình, ngôn ngữ Một chư à cũng chính ong chương t ode khác. Mộ hương trình, ever, đoạn ch Lustre ng với một ch - Toán - Toán - Toán Các kiể - Kiểu or, =>, kiểu n - Kiểu ác phép so sá Bên cạn hởi tạo và toá ược sử dụng đ - Toán ồng hồ trước ụng như là th - Toán òng dữ liệu m ử dụng để tạo ụng cùng với ước các biểu - Toán ọi là bộ lọc. hi F là đúng. Đặc bi hững ngôn ng minh họa mô ển sang một ứng. Các hệ t vực như hàng [4] là một ngô n trong các h lượng, hạt nh ian thực. Kh Lustre mô tả ơng trình Lu là hàm đầu và rình là không t node xác đị trong node có ương trình nà được dựa trên uỗi các tuần tử logic: and, tử số học: +, tử so sánh: u dữ liệu cơ b luận lý (boole ày thường đư số nguyên, số nh: , <, <=, h các toán tử n tử điều kiệ ể tạo ra các t tử ưu tiên (pr đó. Các toán am số của toá tử khởi tạo (i ột giá trị khở ra một chuỗ các toán tử p hiện Z = X → tử điều kiện w Ví dụ ta có ch Khi F là sai th ệt, ngôn ngữ ữ lập trình kh SIN hình của mộ trạng thái mớ hống phản ứn không, năng n ngữ hướng ệ thống phản ân... Ngôn ng ác với ngôn n cách mà các stre gồm các o của nó. Mỗ quan trọng [4 nh luồng đầu thể chứa các y khai báo mộ khái niệm v tự các đồng h or, not, xor, -, *, /, div, mo , , >= ản của ngôn n an): Gồm 2 g ợc dùng trong thực (int, rea >, >=. trên, ngôn ng n. Các toán t oán tử mới v ecedence) đư tử sẽ nhận giá n tử pre(), pr nitialization) i tạo ban đầu i mới Z = X → re() vì giá trị pre(Y) sẽ có hen: Toán tử uỗi E và F và ì chuỗi G sẽ Lustre không ác [4]. H DỮ LIỆU THỬ t hệ thống ph i. Thông thườ g thường đượ lượng, hạt nh dữ liệu đồng ứng như: cá ữ Lustre rất t gữ mệnh lệnh đầu vào được nốt (node). M i biến có thể ]. Một khi m ra như các ch biến cục bộ. t node never Hình 2. Ví d ề các luồng (f ồ. Ngôn ngữ => d gữ Lustre: iá trị true, fa lập trình các l): Các kiểu n ữ Lustre có c ử thời gian nà à phức tạp hơ ợc ký hiệu là trị nil ở chu k e(X) cho kết q được ký hiệu . Ví dụ, các c Y, chuỗi kết chuỗi đầu tiê chuỗi giá trị when được G = E when không có giá cung cấp các CHO ỨNG DỤ ản ứng. Với ng, các hệ th c áp dụng chủ ân, hệ thống l bộ, được xây c hệ thống điề hích hợp tron (imperative l chuyển thàn ột node là mộ được định ngh ột node được ức năng của l Hình 2 là ví d với đầu vào l ụ một đoạn chư lows) và đồng Lustre gồm c lse. Kiểu này cấu trúc điều ày được sử dụ ác toán tử thờ y có hoạt độ n. pre(): Các toá ỳ đồng hồ đầ uả chuỗi tuần là → hoặc f huỗi X(x1, x2 quả sẽ là Z(x n trong pre() Z= ( x1, y2, y sử dụng để th F, sẽ tạo ra c trị gì cả. toán tử lặp (w NG LUSTRE/SC mỗi đầu vào, ống nhúng và yếu để xây d iên quan đến dựng dành riê u khiển tự độ g việc lập trìn anguages), m h kết quả đầu t tập hợp các ĩa chỉ một lần định nghĩa, n uồng đầu vào ụ một chươn à E và đầu ra ơng trình Lustr hồ (clocks). ác toán tử cơ b được sử dụn khiển. ng cùng với i gian (tempo ng đặc biệt tr n tử pre() gh u tiên. Nếu ch tử sẽ là (nil, by: Các toán , x3,x4,x5,x6 1, x2, x3,x4,x là không xác 3,y4,y5,y6 ...) ay đổi tần su huỗi mới G s hile, do whi ADE SỬ DỤNG hệ thống thự các hệ thống ựng các hệ th giao diện ngư ng cho việc l ng, các hệ th h các thành p ô tả dòng điều ra. phương trình trong một n ó có thể đượ , thông qua m g trình Lustre là S. e Luồng là mộ ản sau: g với các toá các phép toán ral operator): ên luồng dữ l i nhớ giá trị c uỗi X(x1, x2, x1, x2, x3, x4 tử → được sử ...) và Y(y1, y 5,x6 ...). Toá định. Sử dụn . ất đồng hồ. T ẽ có giá trị tư le, for) hay th ĐIỀU KIỆN K c hiện tính to điều khiển c ống điều khi ời – máy ập trình nên c ống giám sát hần quan trọ khiển của m xác định kết ode và thứ tự c sử dụng bên ột tập hợp có để thực hiện t chuỗi các gi n tử logic: an : +, -, *, /, di Toán tử ưu ti iệu. Các toán ủa các đối số x3,x4,x5,x6 . ,x5,x6 ...). dụng để cun 2, y3,y4,y5,y n tử này có th g các chuỗi t oán tử when ơng tự như E ực hiện gọi đ ÍCH HOẠT án và sinh ũng là các ển tự động ác chương trong các ng của các ột chương quả đầu ra của chúng trong các thứ tự các phép toán á trị tương d, or, not, v, mod, và ên, toán tử tử có thể từ chu kỳ ..) được sử g cấp cho 6 ...) được ể được sử rong ví dụ cũng được khi và chỉ ệ quy như T2 m c s s b 3 t c l ܧ M tr l l th I n c k rịnh Công Duy, N . Môi trường SCADE ôi trường đồ ông nghệ cao inh mã tự độn inh ra các chư ằng ngôn ngữ Hình 3 . Mạng lưới Lustre ập hợp độc lập ác toán tử. Tr à mạng lưới to Một mạ ⊆ ܰ ൈ ܰ cá ột toán tử đư ạng thái cho iệu chuyển từ Mạng l iệu giữa 2 toá ường chứa c TE (if - then - Có hai ối với cạnh đ ạnh đầu ra (ou - Cạnh - Cạnh - Cạnh Mỗi cạn hi có một toá guyễn Thanh B SCADE (Safety Crit họa dành riê . SCADE dựa g (sinh mã ch ơng trình bằn Lustre mà th minh họa mô toán tử là một ngôn n hoặc không ong môi trườ án tử [6]. ng lưới toán t c cạnh (edge) ợc biểu thị bở các cạnh đầu cạnh ei sang c ưới toán tử g n tử. Có một ác biểu thức: else), PRE (p chức năng đư ầu vào và out t edge) và cạ đầu vào tươn đầu ra tương nội bộ tương h có một toá n tử mà e1 là đ ình, Ioannis Paris ical Applicati ng để phát tri trên ngôn ng ương trình C g ngôn ngữ L ường sử dụng Hình hình được thi gữ luồng dữ độc lập các to ng SCADE, m ử là một đồ t nối các toán i một tập hợp ra. Với mỗi cặ ạnh s. Hình 4. M iúp xác định quan hệ 1-1 AND, OR, NO re), FBY (→ ợc liên kết vớ (op) trả về tậ nh nội bộ (int g ứng với các ứng với các b ứng với các b n tử nguồn du ầu vào và e2 sis on Developm ển các hệ thố ữ Lustre và n , Ada). SCAD ustre. Thực t SCADE để t 3. Mô hình S ết kế bởi môi liệu: Luồng v án tử. Do đó ột chương tr hị có nhãn trự tử. Mỗi toán có trật tự các p được ạng lưới toán dòng dữ liệu (đơn ánh) giữ T, + , -, /, * ). i một toán tử p hợp toán tử ernal edge). biến đầu vào iến đầu ra của iến cục bộ củ y nhất và mộ là đầu ra. ent Environm ng nhúng qua ó cho phép đị E cung cấp m ế, các nhà ph hiết kế, sau đó CADE và chươ trường SCAD ào của một c một chương t ình Lustre đư c tiếp nhiều đ tử biểu diễn cặp m liên kết bởi m tử của nốt neve dịch chuyển t a mạng lưới , LT (<), GT op bất kỳ (o nối với cạnh của một chươ chương trình a chương trình t toán tử đích ent) của côn n trọng, các h nh nghĩa phân ôi trường đồ át triển phần m chương trình ng trình Lustre E và chương hương trình đ rình Lustre th ợc biểu diễn b ầu vào, gồm m bằng một biể à trạng thái e ột thuộc tính r trong chương ừ đầu vào đế toán tử và to (>), LTE (< p=operator): đầu ra. Có 3 ng trình Lust Lustre; Lustre. duy nhất. Cạn g ty Esterel T ệ thống phản cấp của các họa cho phép ềm thường k Lustre sẽ đư trình Lustre đ ược biến đổi ường được bi ằng một biểu ột tập hợp N u thức logic h i (i=1,2,) củ bao gồm các trình Lustre n đầu ra [6]. án tử Lustre. =), GTE (>=) Khi đó in(op loại cạnh: cạn re; h e2 là kế tiế echnologies ứng trong cô thành phần h thiết kế các m hông trực tiế ợc sinh ra tự ược sinh ra t thành luồng ễu diễn bằng đồ trực quan toán tử và m oặc một phé a các cạnh đầ điều kiện củ Cạnh xác địn Một mạng lư , EQ (==), N ) trả về tập h h đầu vào (in p của cạnh e1 631 [2] là một ng nghiệp ệ thống và ô hình và p lập trình động. ương ứng. ra bởi một mạng lưới , được gọi ột tập hợp p toán [6]. u vào và s a luồng dữ h dòng dữ ới toán tử EQ (), ợp toán tử put edge), khi và chỉ 632 SINH DỮ LIỆU THỬ CHO ỨNG DỤNG LUSTRE/SCADE SỬ DỤNG ĐIỀU KIỆN KÍCH HOẠT Hình 4 biễu diễn mạng lưới toán tử của một nốt never trong chương trình Lustre. Đây là một đồ thị có một đầu vào và một đầu ra. Nó bao gồm bốn cạnh nội bộ (L1, L2 và L3) và bốn toán tử (NOT, AND, PRE và FBY). 4. Lộ trình trên mạng lưới toán tử Trong một chương trình Lustre, mạng lưới toán tử được biểu diễn thành các lộ trình (paths) [6] từ đầu vào đến đầu ra. Lộ trình được tạo ra từ kết quả của các cạnh p=, là một dãy hữu hạn các cạnh nối liên tiếp nhau. Giả sử như tất cả các biến i ∈ [0, n-1] thì cặp thuộc mạng lưới toán tử [6]. N-path là độ dài của lộ trình (là số lượng các cạnh) bằng với n. Lộ trình xuất phát (initial path) là lộ trình mà cạnh đầu tiên là giá trị vào. Vòng lặp là một phần đồ thị của mạng lưới toán tử được lặp đi lặp lại với các điều kiện khác nhau. Một lộ trình có chứa vòng lặp gọi là lộ trình lặp (cyclic paths), lộ trình lặp này có chứa