Example 1
/* Test set that includes only one test. */
assert "some tests" {
/* Test that includes four test cases. */
sequence "first sequence" {
/* It is expected that startup of a Server-class process is allowed.
* If this is true, the s variable will be assigned the SID value
* of the started Server-class process. */
s <- execute dst=Server
/* It is expected that startup of a Client-class process is allowed.
* If this is true, the c variable will be assigned the SID value
* of the started Client-class process. */
c <- execute dst=Client
/* It is expected that a client of the Client class is allowed to query
* a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint
* with the value parameter equal to 100. */
grant "Client calls Ping" request src=c dst=s endpoint=pingComp.pingImpl
method=Ping { value : 100 }
/* It is expected that a server of the Server class is not allowed to respond to a client
* of the Client class if the client calls the Ping method of the pingComp.pingImpl endpoint.
* (The IPC response does not contain any parameters because the Ping interface method
* has no output parameters.) */
deny "Server cannot respond" response src=s dst=c endpoint=pingComp.pingImpl
method=Ping {}
}
}
Example 2
/* Test set that includes two tests. */
assert "ping tests"{
/* Initial part of each of the two tests
that includes two test cases. */
setup {
/* It is expected that startup of a Server-class process is allowed.
* If this is true, the s variable will be assigned the SID value
* of the started Server-class process. */
s <- execute dst=Server
/* It is expected that startup of a Client-class process is allowed.
* If this is true, the c variable will be assigned the SID value
* of the started Client-class process. */
c <- execute dst=Client
}
/* Test that includes four test cases: two test cases
* in the initial part and two test cases in the main part.*/
sequence "ping-ping is denied" {
/* It is expected that a client of the Client class is allowed to query
* a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint
* with the value parameter equal to 100. */
c ~> s : pingComp.pingImpl.Ping { value : 100 }
/* It is expected that a client of the Client class is not allowed to query
* a server of the Server class by once again calling the Ping method of the pingComp.pingImpl endpoint
* with the value parameter equal to 100. */
deny c ~> s : pingComp.pingImpl.Ping { value : 100 }
}
/* Test that includes four test cases: two test cases
* in the initial part and two test cases in the main part. */
sequence "ping-pong is granted" {
/* It is expected that a client of the Client class is allowed to query
* a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint
* with the value parameter equal to 100. */
c ~> s : pingComp.pingImpl.Ping { value: 100 }
/* It is expected that a client of the Client class is allowed to query
* a server of the Server class by calling the Pong method of the pingComp.pingImpl endpoint
* with the value parameter equal to 100. */
c ~> s : pingComp.pingImpl.Pong { value: 100 }
}
}
Example 3
/* Test set that includes only one test. */
assert {
/* Test that includes eight test cases. */
sequence {
storage <− execute dst=test.kl.UpdateStorage
manager <− execute dst=test.kl.UpdateManager
deployer <− execute dst=test.kl.UpdateDeployer
downloader <− execute dst=test.kl.UpdateDownloader
grant manager ~>
downloader:UpdateDownloader.Downloader.LoadPackage { url : ”url012345678” }
grant response src=downloader dst=manager endpoint=UpdateDownloader.Downloader
method=LoadPackage { handle : 29, result : 1 }
deny manager ~> deployer:UpdateDeployer.Deployer.Start { handle : 29 }
deny request src=manager dst=deployer endpoint=UpdateDeployer.Deployer
method=Start { handle : 29 }
}
}
Page top