[Формальная верификация ПО] - [PROMELA, SPIN, Cobra] С подачи fk0 ->, которому я сильно признателен за наводку!!! http://caxapa.ru/841641.html
PROMELA Process or Protocol Meta Language - язык описания моделей.
https://en.wikipedia.org/wiki/Promela
http://spinroot.co …/spin/Man/promela.html
SPIN - model checker - средство моделирования на основе PROMELA
https://en.wikiped …iki/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.wikiped …/Linear_temporal_logic
Книги по теме - я почти все нашел
http://spinroot.com/spin/books.html
Темпоральная логика (англ. temporal logic) — это логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.
https://ru.wikiped …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*
Поведение программы описывается на формально непротиворечивом языке, и на этой основе верифицируется поведение программы.
В целом, это какой-то совершенно новый мир в части надежности ПО. Выпал в осадок, надо обдумать.