Без заголовка

> Верификация и валидация киберфизических систем -- это кошмар, потому как целостность их непонятно как проверять, никто не держит общую картинку. Поэтому я и интересовался в свое время системами доказательства программ. Ибо альтернативы таким системам в контексте мишн-критикал систем не видно. Компьютер куда угодно поместить сейчас не проблема, проблема чтобы он не сделал бяку - или злоумышленник с его помощью этой бяки не сделал. Современный разработки в этой сфере очень мощны. Правда, при всей своей мощи они принципиально недостаточно сильны чтобы "закрыть" проблему. Но в руках специалиста это мощный инструмент. Так что дело только за тем чтобы наклепать специалистов, инструментарий к тому времени подтянется. В то же время MDA от OMG видится мне принципиально ущербной, ибо она в некотором смысле "неполна" - возможности детального моделирования на ней весьма ограниченны. Ничего лучше математической логики тут пока не придумали.