/* Набор тестов, который включает один тест. */ 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 can not respond" response src=s dst=c endpoint=pingComp.pingImpl method=Ping {} } }

/* Набор тестов, который включает два теста. */ assert "ping tests"{ /* Начальная часть каждого из двух тестов, * которая включает два тестовых примера. */ setup { /* Ожидается, что запуск процесса класса Server разрешен. * Если это так, переменной s будет присвоено значение SID * запущенного процесса класса Server. */ s <- execute dst=Server /* Ожидается, что запуск процесса класса Client разрешен. * Если это так, переменной c будет присвоено значение SID * запущенного процесса класса Client. */ 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 } } }

/* Набор тестов, который включает один тест. */ 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 } } }