Средства и методы разработки

[Формальная верификация ПО] - [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* Поведение программы описывается на формально непротиворечивом языке, и на этой основе верифицируется поведение программы. В целом, это какой-то совершенно новый мир в части надежности ПО. Выпал в осадок, надо обдумать.