ВходНаше всё Теги codebook PARTS Поиск Опросы Закон Пятница
14 августа
/841665
Evgeny_CD, Архитектор (18.05.2018 02:26 - 26.05.2018 02:17, просмотров: 3382)
[Формальная верификация ПО] - [PROMELA, SPIN, Cobra] С подачи fk0 ->, которому я сильно признателен за наводку!!! ссылка PROMELA Process or Protocol Meta Language - язык описания моделей. https://en.wikipedia.org/wiki/Promela http://spinroot.com/spin/Man/promela.html SPIN - model checker - средство моделирования на основе PROMELA https://en.wikipedia.org/wiki/SPIN_model_checker http://spinroot.com/spin/whatispin.html Cobra - Static Code Analyzer C, C++, Ada, and Python http://spinroot.com/cobra/index.html LTL - Linear temporal logic - SPIN исполняет модели PROMELA на основе этой штуковины. https://en.wikipedia.org/w …/Linear_temporal_logic Книги по теме - я почти все нашел http://spinroot.com/spin/books.html Темпоральная логика (англ. temporal logic) — это логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале. https://ru.wikipedia.org/w …0%B3%D0%B8%D0%BA%D0%B0 Еще есть Логика деревьев вычислений CTL CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure. https://en.wikipedia.org/wiki/CTL* Поведение программы описывается на формально непротиворечивом языке, и на этой основе верифицируется поведение программы. В целом, это какой-то совершенно новый мир в части надежности ПО. Выпал в осадок, надо обдумать.
b [Формальная верификация ПО] b - b [PROMELA SPIN Cobra] b С поверификация
Ответить
Ответы