Обсуждение:OPS: Automata — различия между версиями

Версия 23:10, 22 июля 2009

Недавно прочитала книгу и публикацию (которая совсем не публикация). Обе понравились. Они дополняли друг друга и, в частности, уделяли внимание разработке ПО и тому, через что надо пройти прежде чем кодить, насколько необходимо проделать этот путь, что происходит в современном мире в этом отношении. Рассказывалось и о катастрафических (для проекта) ошибках, повлекших большие убытки и много работы для их исправления, вызванных плохим проетированием, и о том, как легко их можно было бы избежать. Впечатление усиливалось и тем, что книгу я читала пока делала предыдущее задание. Тогда, кстати, я впервые на деле узнала, что значит хорошо спроектировать: дважды приходилось менять внутреннее представление некоторых базовых и широко используемых классов. Каждый раз это занимало 15 минут. Я всегда понимала, что так и должно быть (потому что в конспекте написано и А.М. говорил), но почувствовать удобство "в деле" — это совсем другое. Книга, но еще больше непубликация, имела большое влияние на меня. В какой-то момент чтения приняла революционное для себя решение, что выполнение следующего задания (добровольно! (революционность по большей части в этом)) начну с карандаша, бумаги и UML, а не с клавиатуры, монитора и VS.

А пока вдохновение меня не отпустило, добавлю что-то более конкретное.

Почему именно здесь? Причин этому много. Это как соображения технического удобства, так и субъективные причины (прежде всего, это ощущения открытости и дружественной атмосферы (значение этих слов предоставляю определить читателю)). Не кривя душой, скажу, что для меня приятна и возможность какого-то стороннего интереса, который без элементов открытости, появиться не может. Однако же, отклики – не цель, а написанное — не призыв к ним.

Тогда для чего? Кроме упомянутой функции документирования, хочется также использовать страницу как некий элемент самоконроля. Не уверена, что смогу работать по срокам (особенно не уверена, что смогу их правильно поставить), но, выражаю большие надежды хотя бы на регулярные публикации о сделанном.

Кому предназначается информация? Во-первых, мне. Не скрою, что пока не чувствую глобального понимания поставленного задания: на данный момент вижу что оно из себя представляет, но тону в мелочах. Источников, программ-аналогов и прочего так много, что они постоянно путаются в голове и мне необходимо место, где я могла бы писать о них, фиксировать найденные публикации и сведения, чтобы не искать повторно. То, что будет написано здесь ни чем не отличается от возможного контента .doc-файла, который лежал бы среди прочих документов у меня на винте, но еще раз сказав о сравнительном удобстве вики (мне она не всем нравится), файлик будет лежать на винте у мехмата.

Что мне за это будет?

• Ясность.
• Повод познакомиться с UML.
• Если кто-то (и я в том числе) рискнет через некоторое время разобраться в сделанном, то, имея на руках не только код, но и сопроводительную документацию (еще более кривую, чем код :) ), будет намного проще.

Учитывая, что эта идея ничем не подкреплена (в смысле не подкреплена обязательностью воплощения), она будет жить, пока мне не надоест или пока я не решу, что мне уже все понятно и продолжать что-либо документировать и проектировать не надо, в общем, второе может быть вызвано первым. --Avalanche 02:25, 22 июля 2009 (MSD)

Avalanche, если в процессе изучения вопроса наткнётесь на статью, в которой обсуждается верификация сетевых протоколов с помощью конечных автоматов, маякните, пожалуйста. Я давно хотел включить этот материал в курс по распределённым системам. Хопкрофт/Мотвани/Ульман упоминают о верификации сетевых протоколов, как об одном из приложений автоматов, но ссылок не дают, к сожалению. --Bravit 22:00, 22 июля 2009 (MSD)

Что-то нашлось, но не знаю насколько Вам это подойдет:

• P.R. D’Argenio, J.-P. Katoen, T. Ruys, and G.J. Tretmans. The bounded retransmission protocol must be on time! In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217, 1997.
• G.J. Holzmann. An improved protocol reachability analysis technique. Software–Practice and Experience 18(2), 1988.
• G.J. Holzmann. Design and Validation of Computer Protocols. PrenticeHall, 1991.
• G.J. Holzmann. Tracing protocols. AT&T Technical Journal 64(12), 1985.
• R. Gerth, D. Peled, M. Vardi, P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. Proceedings 13th Symposium on Protocol Specification, Testing and Verification, 1995.
• J.F. Groote, F. Monin and J. van de Pol. Checking verifications of protocols and distributed systems by computer. Concur’98: Concurrency Theory, LNCS 1432, 1998.
• C.H. West. Applications and limitations of automated protocol validation. Proceedings 2nd Symposium on Protocol Specification, Testing and Verification, 1982.

К сожалению, все работы очень старые. В них есть много ссылок на другие работы по интересующей Вас теме, надеюсь (это затрагивает мои личные интересы), что-то поможет.

Вообще, протокол — это тот же самый КА, потому ничто автоматное ему не чуждо, а современный материал по верификации автоматных программ есть по ссылке [6] в статье. По этой же ссылке под блистательным заголовком «Еще одна книга по верификации» скрывается Katoen. Concepts, Algorithms, and Tools for Model Checking. Lecture Notes of the Course «Mechanised Validation of Parallel Systems», Semester 1998/1999 из которой, преимущественно, взяты вышеприведенные источники.