Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішень
теорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду,
автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект.
Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів API в наближенні першого порядку. Аналізатор, використовуючи ці наближення як моделі та їх формули першого порядку, залучає поведінку специфікації (його негативність) описаної програми. Рішення SMT-LIB формул розглядається як комбінована формула для того, щоб їх «обмежувати» та «розв’язувати». Форма «розв’язку» може використовуватися для ідентифікації логічних помилок (безпеки) Java-програм на базі Android. Властивості
безпеки Android представлено як обмежувальні аналітичні цілі, щоб показати важливість цих обмежень.
Cтатистичний аналіз вихідного коду змодельований для java-програм, які містять додатки з безпекою Android
2015
Aufsatz (Zeitschrift)
Elektronische Ressource
Unbekannt
Metadata by DOAJ is licensed under CC BY-SA 1.0
Вибір системи показників, характеристичних ефективності системи управління безпекою польоту
DOAJ | 2020
|СТУПІНЬ ІНТЕГРАЦІЇ УКРАЇНИ В МІЖНАРОДНУ БАГАТОРІВНЕВУ СИСТЕМУ КЕРУВАННЯ БЕЗПЕКОЮ ПОЛЬОТІВ
DOAJ | 2012
|ПРИНЦИПИ СИСТЕМНОГО ПІДХОДУ ДО КЕРУВАННЯ БЕЗПЕКОЮ ПОЛЬОТІВ ПІД ЧАС ОРГАНІЗАЦІЇ ПОВІТРЯНОГО РУХУ
DOAJ | 2010
|НОРМУВАННЯ РИЗИКІВ У СИСТЕМІ КЕРУВАННЯ БЕЗПЕКОЮ ПОЛЬОТІВ НА АЕРОДРОМАХ ЦИВІЛЬНОЇ АВІАЦІЇ
DOAJ | 2011