Здравствуйте, avl-kharkov, Вы писали:

AK>Здравствуйте, thesz, Вы писали:

T>>Там есть пункт "Embedded systems development". Я уточню ваш опыт по этому пункту, поскольку мне это интересно.
T>>Каким средствами формальной верификации вы пользуетесь для разработки встроенных систем?
AK>Да, я как раз в Embedded
AK>На тех проектах, в которых я участвовал, отдельно выделенного процесса для формальной верификации не было. В отдельных примерах можно считать, что это делалось в процессе дизайна (проектирование автоматов состояний и переходов, из того что вспомнилось с ходу).

Alloy и похожее вы не использовали?

Коллеги с помощью Alloy выявляли ошибки в спецификациях разных ZigBee и прочих.

AK>И теперь уже интересно стало мне — каким образом можно формально верифицировать, например, осциллограф?

An International Survey of Industrial Applications of Formal Methods: Volume 1 Purpose, Approach, Analysis, and Conclusions (1993)

Там есть описание, как применяли Z notation в Tektronics, AFAIR (может, это во втором томе, я точно не помню). Как связаны Tektronics и осциллографы, наверное, известно?

Производительность труда у Тектрониксов выросла, надо отметить.

AK>Может, конечно, надо начать мыслить концепциями функционального программирования, чтоб начать эти вещи воспринимать естественно...

Надо начать мыслить "какие ошибки я допущу и как мне их избежать как можно раньше, желательно, ещё до юнит-тестов".