Пример 1
/* Описание набора тестов, который включает один тест. */
assert "some tests" {
/* Описание теста, который включает четыре тестовых примера. */
sequence "first sequence" {
/* Ожидается, что запуск процесса класс Server разрешен.
* Если это так, переменной s будет присвоено значение SID
* запущенного процесса класса Server. */
s <- execute dst=Server
/* Ожидается, что запуск процесса класс Client разрешен.
* Если это так, переменной c будет присвоено значение SID
* запущенного процесса класса Client. */
c <- execute dst=Client
/* Ожидается, что клиенту класса Client разрешено обращаться к
* серверу класса Server, вызывая метод Ping службы pingComp.pingImpl
* с параметром value, равным 100. */
grant "Client calls Ping" request src=c dst=s endpoint=pingComp.pingImpl
method=Ping { value : 100 }
/* Ожидается, что серверу класса Server запрещено отвечать клиенту
* класса Client, если клиент вызывает метод Ping службы pingComp.pingImpl.
* (IPC-ответ не содержит параметров, так как интерфейсный метод Ping
* не имеет выходных параметров.) */
deny "Server cannot respond" response src=s dst=c endpoint=pingComp.pingImpl
method=Ping {}
}
}
Пример 2
/* Описание набора тестов, который включает два теста. */
assert "ping tests"{
/* Начальная часть каждого из двух тестов */
setup {
s <- execute dst=Server
c <- execute dst=Client
}
/* Описание теста, который включает два тестовых примера. */
sequence "ping-ping is denied" {
/* Ожидается, что клиенту класса Client разрешено обращаться к
* серверу класса Server, вызывая метод Ping службы pingComp.pingImpl
* с параметром value, равным 100. */
c ~> s : pingComp.pingImpl.Ping { value : 100 }
/* Ожидается, что клиенту класса Client запрещено обращаться к
* серверу класса Server, повторно вызывая метод Ping службы pingComp.pingImpl
* с параметром value, равным 100. */
deny c ~> s : pingComp.pingImpl.Ping { value : 100 }
}
/* Описание теста, который включает два тестовых примера. */
sequence "ping-pong is granted" {
/* Ожидается, что клиенту класса Client разрешено обращаться к
* серверу класса Server, вызывая метод Ping службы pingComp.pingImpl
* с параметром value, равным 100. */
c ~> s : pingComp.pingImpl.Ping { value: 100 }
/* Ожидается, что клиенту класса Client разрешено обращаться к
* серверу класса Server, вызывая метод Pong службы pingComp.pingImpl
* с параметром value, равным 100. */
c ~> s : pingComp.pingImpl.Pong { value: 100 }
}
}
Пример 3
/* Описание набора тестов, который включает один тест. */
assert {
/* Описание теста, который включает восемь тестовых примеров. */
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 }
}
}
В начало