Программа курса «Формальные методы разработки программных систем»

Скачать 102.21 Kb.

Название	Программа курса «Формальные методы разработки программных систем»
Тип	Программа курса

rykovodstvo.ru > Руководство эксплуатация > Программа курса

Кафедра общей информатики ФИТ НГУ

Программа курса «Формальные методы разработки программных систем»

2003-2004 учебный год

Организационно-методический раздел.

1.1Название курса.

Формальные методы разработки программных систем

Направление - 552800 Информатика и вычислительная техника.

Раздел - специальные дисциплины

Компонент - СД.0? вузовский

1.2Цели и задачи курса.

Дисциплина «Формальные методы разработки программных систем» предназначена для изучения основных формальных методов спецификации и анализа программных систем.

Основной целью освоения дисциплины является знакомство с современными формальными методами разработки программных систем.

Для достижения поставленной цели выделяются следующие задачи курса:

разъяснение положительных и отрицательных сторон применения формальных методов при разработке программных систем;
обзор и сравнительный анализ различных формальных языков и нотаций;

анализ способности формальных методов обеспечить качество создаваемых программных систем.

1.3Требования к уровню освоения содержания курса.

По окончании изучения указанной дисциплины студент должен:

иметь представление о современных формальных методах спецификации и анализа программных систем;
знать ключевые преимущества и ограничения, связанные с применением формальных методов в технологическом процессе;
уметь оценивать целесообразность применения конкретных формальных методов при разработке конкретных систем.

1.4Формы контроля

Итоговый контроль. Для контроля усвоения дисциплины учебным планом предусмотрен экзамен.

Текущий контроль. В течение семестра студенты по указанию преподавателя самостоятельно готовят и представляют доклады, посвященные углубленному рассмотрению конкретных формальных методов. Выполнение указанных видов работ является обязательным для всех студентов, а результаты текущего контроля служат основанием для выставления оценок в ведомость контрольной недели на факультете.

2Содержание дисциплины.

2.1Новизна.

Формальные методы представляют собой мощное средство для спецификации и верификации программных систем. Корректность полученных результатов гарантируется математическим аппаратом, опирающимся на достижения алгебры, логики и дискретной математики. Имеются CASE-средства, повышающие эффективность использования различных формальных методов. Однако широкому применению формальных методов при разработке конкретных систем препятствует высокая сложность используемого математического аппарата. Кроме того, большинство формальных методов ориентируются только на обеспечение правильного функционирования систем, и не предоставляют адекватных средств учета нефункциональных показателей, характеризующих качество программных изделий. В этих условиях актуальной задачей является формирование у специалистов навыка оценки целесообразности применения тех или иных формальных методов при разработке конкретных систем.

Изложение формальных методов разработки программ в той или иной форме присутствует в большинстве учебных планов соответствующих специальностей российских и зарубежных вузов. В крупных зарубежных центрах подготовки специалистов по информационных технологиям, таких как Массачусетский технологический институт (MIT), читаются даже специальные курсы, посвященные конкретным методам. Однако при этом редко обеспечивается широта освещения разнородных формальных методов, не проводится их сравнительный анализ, не всегда проясняется их связь с типами разрабатываемых систем и используемых средств программирования. Поэтому нацеленность настоящего курса не столько на глубину изложения конкретных языков и инструментов, сколько на полноту обзора современных формальных методов, составляет его содержательную новизну.

2.2Тематический план курса.

Наименование разделов и тем	К о л и ч е с т в о ч а с о в
Наименование разделов и тем	Лекции	Семинары	Лаборатор- ные работы	Самостоятель-ная работа	Всего часов
Введение	2	0	0	2	4
Формальные методы в технологическом процессе	4	0	0	4	8
Математические основы формальных методов	4	0	0	4	8
Семантические сети и онтологии	2	0	0	2	4
Алгебраические спецификации	2	0	0	2	4
Денотационное моделирование	2	0	0	2	4
Алгебры процессов	2	0	0	2	4
Дедуктивное описание	2	0	0	2	4
Структуры Крипке	2	0	0	2	4
Мутирующие (эволюционные) алгебры	2	0	0	2	4
Структурный анализ	2	0	0	2	4
Объектно-ориентированный подход	2	0	0	2	4
Компонентное проектирование	2	0	0	2	4
Формальные методы и обеспечение качества	4	0	0	4	8
Оптимизация трудозатрат	2	0	0	2	4
Итого по курсу:	36	0	0	36	72

2.3Содержание отдельных разделов и тем.

Введение.

Формальные языки и методы. Предпосылки и критерии выбора формальных методов разработки.

Формальные методы в технологическом процессе

Формальные методы в технологическом процессе разработки программных систем. Специфика формального подхода к выполнению основных фаз технологического цикла. Технология стерильного цеха (Cleanroom Software Engineering).

Математические основы формальных методов.

Исчисление предикатов, теория множеств, теория моделей, теория категорий.

Семантические сети и онтологии

Семантические сети и онтологии предметных областей. Вычислительные моделии фреймы. OWL – язык структурированной спецификации онтологий.

Алгебраические спецификации

Алгебраические спецификации абстрактных типов данных. Многосортные алгебраические системы. Построение инициальной модели. Институции – теоретико-категорные спецификации сложных систем типов данных.

Денотационное моделирование

Денотационное моделирование динамики систем. Денотационная семантика информационных объектов. Языки денотационной спецификации VDM и Z.

Алгебры процессов.

Исчисление взаимодействующих последовательных процессов (Communicating Sequential Processes, CSP). Свойство универсальности CSP-спецификаций.

Дедуктивное описание

Дедуктивное описание и логический подход к программированию. Аналогия между программами и конструктивными доказательствами. Метод резолюций и язык Пролог.

Структуры Крипке.

Модальные и динамические логики. Графы зависимостей, операторные схемы и сети Петри. Верификация посредством проверки на моделях (model checking).

Мутирующие (эволюционные) алгебры (evolving algebra).

Машины абстрактных состояний (МАС). Язык AsmL и верификация во время исполнения.

Структурный анализ

Структурный анализ и декомпозиция сложных систем. Графические средства представления результатов структурного анализа. Метод SADT (Structured Analysis and Design Technique).

Объектно-ориентированный подход

Объектно-ориентированный подход к анализу и проектированию. F-логика – аппарат логической формализации процесса объектно-ориентированного проектирования. Словари классов и адаптивное программирование.

Компонентное проектирование

Компонентное проектирование и языки описания архитектуры (Architecture Description Languages, ADL). Принципы компонентного подхода. Примеры языков описания архитектуры: Wright, Rapide. xADL – технология создания проблемно-ориентированных ADL.

Формальные методы и обеспечение качества

Формальные методы и обеспечение качества программных систем. Формализация нефункциональных требований эффективности. Язык NoFun. NFR Framework – формальная методика оценки влияния проектных решений на качество создаваемой системы.

Оптимизация трудозатрат

Оптимизация трудозатрат, связанных с использованием формальных методов. Модели алгоритмов и шаблоны проектирования. Подготовка формальных спецификаций к многократному использованию: документирование, параметризация, определение контекста.

2.4Перечень примерных контрольных вопросов и заданий для самостоятельной работы.

Постройте спецификацию мультиграфа как многосортной алгебраической системы.
Постройте обобщение категории, задающей представление моноида как класса морфизмов единственного объекта, на произвольную многосортную алгебру. Такая конструкция называется клоном.
Сложные формальные спецификации, получающиеся путем объединения простых, можно строить двумя способами: сверху вниз либо снизу вверх. Сформулируйте и обоснуйте рекомендации по поводу последовательности построения сложных спецификаций при использовании каждого из известных Вам формальных методов.
Охарактеризуйте пригодность каждого из известных Вам формальных методов для спецификации и анализа распределенных вычислительных систем.
Постройте формальную модель качества какой-либо системы, которую Вы разрабатывали.
Исследуйте возможности языка Пролог для формализации технологического процесса разработки программных систем и анализа последствий принятия тех или иных проектных решений. Постройте соответствующий прототип.

3Учебно-методическое обеспечение дисциплины

3.1Темы рефератов (курсовых работ).

3.2Образцы вопросов для подготовки к экзамену.

Вопросы для подготовки к экзамену совпадают с темами занятий, указанными в тематическом плане. На экзамене студент получает один вопрос. Требуется раскрыть основные положения выбранной темы, продемонстрировать понимание материала. При подготовке разрешается пользоваться любой дополнительной литературой. В ходе приема экзамена студенту могут быть заданы дополнительные вопросы, относящиеся к другим темам.

3.3Список основной и дополнительной литературы.

Ахо А.В., Хопкрофт Дж., Ульман Дж. Структуры данных и алгоритмы. М.: «Вильямс», 2001.
Бауэр Ф.Л., Гооз Г. Информатика. Вводный курс. Т. 1-2. М.: Мир, 1990.
Брукс Ф. Мифический человеко-месяц. СПб.: Символ-Плюс, 1999.
Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на C++. 2-е изд. М.: Бином, СПб.: Невский Диалект, 1999.
Замулин А.В. Формальные методы спецификации программ. Новосибирск: НГУ, 2002.
Котов В.Е. Сети Петри. М.: Наука, 1984.
Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логика и теории алгоритмов. 4-е изд. М.: Физматлит, 2001.
Лавров С.С. Программирование. Математические основы, средства, теория. СПб.: БХВ-Петербург, 2001.
Логическое программирование. М.: Мир, 1988.
Марка Д.А., Мак-Гоуэн К. Методология структурного анализа и проектирования. М.: Метатехнология, 1993.
Математическая логика в программировании. М.: Мир, 1991.
Минский М. Фреймы для представления знаний. М.: Энергия, 1979.
Непейвода Н.Н. Прикладная логика. Новосибирск: НГУ, 2000.
Соммервилл И. Инженерия программного обеспечения. 6-е изд. М.: «Вильямс», 2002.
Тыугу Э.Х. Концептуальное программирование. М.: Наука, 1984.
Хоар Ч. Взаимодействующие последовательные процессы. М.: Мир, 1989.
Allen R. J., Garlan D. A formal basis for architectural connection // ACM Trans. on Software Engineering and Methodology, 6(3), 1997. P. 213-249. http://www-2.cs.cmu.edu/afs/cs/project/able/ftp/wright-tosem97.ps.
Barnett M., Schulte W. Runtime verification of .NET contracts // Journal of Systems and Software, 65(3), 2003. P. 199-208.
Botella P., Burgués X., Franch X., Huerta M., Salazar G. Modeling non-functional requirements // Proc. JIRA'2001. Sevilla: 2001. http://www.lsi.us.es/~amador/JIRA/Ponencias/JIRA_Botella.pdf.
Clarke E., Wing J. Formal methods: state of the art and future directions // ACM Computing Surveys, 28(4), 1996. P. 626-643. http://www.cs.cmu.edu/afs/cs/usr/wing/www/mit/paper/paper.ps.
Dashofy E.M., van der Hoek A., Taylor R.N. An infrastructure for the rapid development of XML-based architecture description languages // Proc. 24th ICSE. Orlando: ACM Press, 2002. P. 266-276. http://www.ics.uci.edu/~edashofy/papers/icse2002.pdf.
Goguen J. An introduction to algebraic semiotics, with applications to user interface design // Computation for Metaphor, Analogy and Agents. Springer Lecture Notes in Artificial Intelligence. Vol. 1562, 1999. P. 242-291. http://www.cs.ucsd.edu/users/goguen/ps/as.ps.gz.
Gruber T.R. Toward principles for the design of ontologies used for knowledge sharing // Intl. Journal of Human-Computer Studies, 43, 1995. P. 907-928. ftp://ftp.ksl.stanford.edu/pub/KSL_Reports/KSL-93-04.ps.
Gurevich Y. Evolving Algebras 1993: Lipari Guide // Specification and Validation Methods. Oxford: Oxford University Press, 1995. P. 9-36.
Gurevich Y., Rosenzweig D. Partially ordered runs: a case study // Lecture Notes in Computer Science. Vol. 1912, 2000. P. 131-150.
Jones C. B. Systematic Software Development using VDM. London: Prentice-Hall, 1990.
Kifer M., Lausen G., Wu J. Logical foundations of object-oriented and frame-based languages // Journal of the ACM, 42(4), 1995. P. 741-843.
Lieberherr K.J. Adaptive Object-Oriented Software: The Demeter Method. Boston: PWS Publishing Company, 1996.
Luckham D., Vera J., Bryan D., Augustin L., Belz F. Partial orderings of event sets and their application to prototyping concurrent, timed systems // Journal of Systems and Software, Vol. 21, No. 3, June 1993. P. 253-265. ftp://reports.stanford.edu/pub/cstr/reports/csl/tr/92/515/CSL-TR-92-515.pdf.
Medvidovic N., Taylor R.N. A classification and comparison framework for software architecture description languages // IEEE Trans. Software Engineering, 26(1), 2000. P. 70-93. http://sunset.usc.edu/~neno/papers/TSE-ADL.pdf.
Mylopoulos J., Chung L., Nixon B. A. Representing and using non-functional requirements: a process-oriented approach // IEEE Trans. on Software Engineering, 18(6), 1992. P. 483-497.
OWL Web Ontology Language guide. W3C working draft. W3 Consortium, 2003. http://www.w3.org/TR/2003/WD-owl-guide-20030331/.
Spivey J.M. The Z Notation: a reference manual. 2nd Edition. London: Prentice Hall, 1992. http://spivey.oriel.ox.ac.uk/~mike/zrm/zrm.pdf.
Wolter U. A coalgebraic introduction to CSP // Proc. CMCS'99. Elsevier Electronic Notes in Theoretical Computer Science. Vol. 19, 1999. http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs19/tcs19006.ps.

3.4Для изучения дисциплин, которые предусматривают использование нормативно-правовых актов, указывать источник опубликования.

Не предусмотрено.

Похожие:

	Ульяновский государственный технический университет «Программная инженерия» магистерская программа «Методы и средства разработки программных систем» на кафедре «Информационные системы»...		Программа учебного курса гис-системы в приложениях «Технология разработки программных систем» по направлению подготовки магистров техники и технологии 230100 «Информатика и вычислительная...
	Конспект лекций междисциплинарного курса мдк 01. 02 Прикладное программирование ПМ. 01 Разработка программных модулей программного обеспечения для компьютерных систем		Рабочая программа дисциплины Биотехнические системы на базе микроконтроллеров и плис Плис, является формирование у студентов комплекса профессиональных теоретических знаний и практических навыков в области разработки...
	«Разработка и стандартизация программных средств и информационных технологий» Целью подготовки студентов по дисциплине является формирование целостной системы знаний о принципах, моделях и методах, используемых...		Конспект лекций междисциплинарного курса мдк. 03. 01 Технология разработки... Исследовать процессы создания новых технологий и определять их основные тенденции целесообразно, сопоставляя эти технологии с уровнем...
	Конспект лекций междисциплинарного курса мдк. 03. 01 Технология разработки... Исследовать процессы создания новых технологий и определять их основные тенденции целесообразно, сопоставляя эти технологии с уровнем...		Программа курса «Планета здоровья» Программа курса «Подвижные игры» Социальное направление Программа курса «Общественно-полезный труд»
	Информационные технологии Цель курса – ознакомление студентов с принципами и технологией разработки информационных систем, изучение структурных методов и инструментов...		Учебно-методический комплекс учебной дисциплины «Информационные системы нефтегазовой геологии» Гис-систем регионов и России в целом; компьютерных систем бассейнового моделирования; информационных систем моделирования залежей...
	Рабочая программа дисциплины б 27 проектирование мобильных систем... Целью освоения дисциплины является формирование у студентов теоретических основ и практических навыков программной разработки мобильных...		Кафедра программных систем и баз данных Рабочая программа составлена на основании Государственного образовательного стандарта высшего профессионального образования по направлению...
	Рабочая программа курса Код курса: сдм. 19 Тип курса Рабочая программа курса «Компьютерные технологии управления проектами (международный опыт)» в рамках учебной программы «Управление...		О результатах анализа программных систем электронного документооборота... Научно-исследовательское унитарное предприятие «Центр специализированных компьютерных систем» бгу создано в 2001 г
	Рабочая программа элективного курса по информатике и икт «Компьютерная графика» Рабочая программа элективного курса по информатике и икт «Компьютерная графика» составлена на основе авторской программы Л. А. Залоговой,...		Ковшило Д. Ф., Берзегова Л. Ю. Методические разработки по английскому... Методические разработки предназначены для студентов 1 курса, продолжающих изучение английского языка на стоматологическом факультете....

Руководство, инструкция по применению