Đang chuẩn bị liên kết để tải về tài liệu:
Validation of Communications Systems with SDL phần 5

Nếu cần thiết, các dấu vết MSC tương ứng với lỗi này có thể được tạo ra bằng cách nhấn các nút Bắt đầu MSC, lùi lại và sau đó làm lại. Chúng tôi sẽ không sửa lỗi này, bởi vì chúng ta sẽ tìm hiểu làm thế nào để tìm thấy nó với mô phỏng đầy đủ. | 114 Validation of Communications Systems with SDL obs_1 inst_dlca I DLCa sigA I sigB_ sigC I I Figure 5.4 The observer MSC obs_1 of the MSC to verify in this case the Simulator will not explore the states leading to an error a violation of the MSC because the default configuration is error cut equivalent to prune in Tau . 5.2 CASE STUDY WITH TAU SDL SUITE In Chapter 4 we have used the Tau SDL Suite Simulator. To benefit from automatic observation features we will now switch to the Tau SDL Suite Validator. Note that the Simulator can also be used to check the SDL model against an MSC. 5.2.1 Simulate with user-defined rules In the Validator only one user-defined rule can be used at a time. To check several conditions you can use the operator or to group them in a single rule. 5.2.1.1 Detect DLC establishment We want to detect that a DLC is established. This means in our V.76 SDL model that instance 1 of process DLC in block DLCa is in state connected and instance 1 of process DLC in block DLCb is in state connected. It seems that the Validator rules do not accept qualifiers such as Block DLCa . As there are two processes named DLC one in block DLCa and the other in block DLCb it is not possible to write a rule to detect that both DLCs are in state connected. An observer process could be used instead. The solution would be to modify the SDL model to have a copy of block V76_DLC on each side transformation of the block type V76_DLC into a block named V76a making a copy of it and naming the copy V76b and in each block renaming the DLC process respectively DLC_a and DLC_b. Then the Validator user-defined rule would be state DLC_a 1 connected and state DLC_b 1 connected Rather than performing this model modification you will use rules concerning process AtoB and BtoA which do not require the use of qualifiers as they are unique in the system. Automatic Observation of Simulations 115 5.2.1.2 Detect state of processes AtoB and BtoA We want to .