Скачать 192.54 Kb.
|
Правительство Российской Федерации Федеральное государственное автономное образовательное учреждение высшего профессионального образования "Национальный исследовательский университет "Высшая школа экономики" Факультет Программа дисциплины для направления подготовки магистра для магистерской программы Автор программы: Дворянский Л.В., преподаватель Одобрена на заседании кафедры «___»____________ 2012 г. Зав. кафедрой Рекомендована секцией УМС «___»____________ 2012 г. Председатель Утверждена УС факультета «___»____________ 2012 г. Ученый секретарь _________________ Москва, 2012 Настоящая программа не может быть использована другими подразделениями университета и другими вузами без разрешения кафедры-разработчика программы. Government of the Russian Federation Federal state autonomous educational institution of higher professional education "National Research University - Higher School of Economics" Faculty Syllabus of “Formal methods in software engineering” course for the direction of master training for the master program Program author: Tutor, L. W. Dworzanski Approved by the panel of the «___»____________ 2012 г. School of Software Engineering School head S.M. Avdoshin Recommended by the «___»____________ 2012 г. Education board of Business Informatics Secretary Yu. V. Taratoukhine Accepted by the Academic Council «___»____________ 2012 г. of the Faculty of Business Informatics Academic secretary V. A. Fomichov _________________ signature Moscow, 2012 It is prohibited to use the document content by other University’s departments and other institutions without permission from the department that developed the document. 1Application field and normative referencesThis syllabus of the “Formal methods in software engineering” course states knowledge and skills prerequisites and determines a content and forms of control for the course. The syllabus is intended for instructors of the course, teaching assistants, and students of the direction , that take master program “System and software engineering”, specializations “Methods and theory of software engineering”, “Software development management” and the course . The syllabus is developed in accordance with: Educational standard of Federal state autonomous educational institution of higher professional education "National Research University - Higher School of Economics" for the direction of master training (http://www.hse.ru/data/2012/08/27/1242910132/ProgInzh%20mag.pdf); Educational program of the direction of master training; Curriculum of the university for the direction of master training, specializations , approved in 2012. AbstractIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the fact that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification. Formal methods can:
In contrast to other design systems, formal methods use mathematical proof as a complement to system testing in order to ensure correct behavior. As systems become more complicated, and safety becomes a more important issue, the formal approach to system design offers another level of insurance. Formal methods differ from other design systems through the use of formal verification schemes, the basic principles of the system must be proven correct before they are accepted. Traditional system design has used extensive testing to verify behavior, but testing is capable of only finite conclusions. Dijkstra and others have demonstrated that tests can only show the situations where a system won't fail, but cannot say anything about the behavior of the system outside of the testing scenarios. In contrast, once a theorem is proven true it remains true. It is very important to note that formal verification does not obviate the need for testing. Formal verification cannot fix bad assumptions in the design, but it can help identify errors in reasoning which would otherwise be left unverified. In several cases, engineers have reported finding flaws in systems once they reviewed their designs formally. Roughly speaking, formal design can be seen as a three step process, following the outline given here:
In many ways, this step of the formal design process is similar to the formal software engineering technique developed by Rumbaugh, Booch and others. At the minimum, both techniques help engineers to clearly define their problems, goals and solutions. However, formal modeling languages are more rigorously defined. And the clarity that this stage produces is a benefit in itself.
Verification is a difficult process, largely because even the simplest system has several dozen theorems, each of which has to be proven. Even a traditional mathematical proof is a complex affair. Given the demands of complexity, almost all formal systems use an automated theorem proving tool of some form. These tools can prove simple theorems, verify the semantics of theorems, and provide assistance for verifying more complicated proofs.
Formal methods offer additional benefits outside of provability, and these benefits do deserve some mention.
The discipline involved in formal specification has proved useful even on already existing systems. Engineers using the PVS system, for example, reported identifying several microcode errors in one of their microprocessor designs.
For engineers designing safety-critical systems, the benefits of formal methods lie in their clarity. Unlike many other design approaches, the formal verification requires very clearly defined goals and approaches. In a safety critical system, ambiguity can be extremely dangerous, and one of the primary benefits of the formal approach is the elimination of ambiguity. The purpose of this course is to learn how to specify behavior of systems and to experience the design of a system where you can prove that the behavior is correct. Students will learn how to formally specify requirements and to prove (or disprove) them on the behavior. The behavior of systems will be represented by such formalisms as
With a practical assignment students will experience how to apply the techniques in practice. The first part of this course focuses on the study of the semantics of a variety of programming language constructs. We will study structural operational semantics as a way to formalize the intended execution and implementation of languages, axiomatic semantics, useful in developing as well as verifying programs, and denotational semantics, whose deep mathematical underpinnings make it the most versatile of all. Then the special emphasis will be put on parallel and distributed systems modeling, specification and analysis. We consider two basic approaches to concurrent systems specification and analysis: process algebras and Petri nets. Process algebra is a mathematical framework in which system behavior is expressed in the form of algebraic terms, enhancing the available techniques for manipulation. Fundamental to process algebra is a parallel operator, to break down systems into their concurrent components. A set of equations is imposed to derive whether two terms are behaviorally equivalent. In this framework, non-trivial properties of systems can be established in an elegant fashion. For example, it may be possible to equate an implementation to the specification of its required input/output relation. In recent years a variety of automated tools have been developed to facilitate the derivation of such properties. Applications of process algebra exist in diverse fields such as safety critical systems, network protocols, and biology. In the educational vein, process algebra has been recognized to teach skills to deal with complex concurrent systems, by representing and reasoning about such systems in a mathematically clear and precise manner. Petri nets is another popular formalism for modeling, analyzing and verifying reactive and distributed systems. Their strength are their simple but precise semantics, their clear graphical notation, and many methods and algorithms for analysis and verification. The course introduces Petri nets and their theory by the help of examples from different application domains. The focus, however, will be on traditional Petri net theory, in particular on Place/Transition-Systems and on concepts such as place and transition invariants, deadlocks and traps, and the coverability tree. The course also covers different versions and variants of Petri nets as well as different modeling and analysis techniques for particular application areas. Thus we consider an urgent topic of modeling and analysis of workflow processes in more details. The forth module covers a prominent verification technique that has emerged in the last thirty years – model checking. This approach is based on systematical check whether a model of a given system satisfies a property such as deadlock freedom, invariants, or request-response. This automated technique for verification and debugging has developed into a mature and widely-used industrial approach with many applications in software and hardware. It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits. Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking. Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability. This course provides an introduction to the theory of model checking and its theoretical complexity. We introduce transition systems, safety, liveness and fairness properties, as well as omega-regular automata. We then cover the temporal logics LTL, CTL and CTL*, compare them, and treat their model-checking algorithms. Techniques to combat the state-space explosion problem are at the heart of the success of model checking. We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures. Its complexity is analyzed using standard techniques from complexity theory. |
Программа дисциплины для направления подготовки магистра для магистерской программы Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки, обучающихся... | Программа дисциплины [Введите название дисциплины] для направления/... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 030200.... | ||
Программа дисциплины Экономическая психология для направления 030300.... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 030300.... | Программа дисциплины «Экономика города» для направления 081100. 68... Менеджмент” подготовки магистра магистерской программы «Государственное и муниципальное управление» | ||
Программа дисциплины Обучение и развитие персонала для направления... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления 030300. 68 «Психология»... | Программа дисциплины «Уголовная политология» для направления 030900. 68 «Юриспруденция» Программа предназначена для преподавателей и ассистентов-аспирантов, ведущих данную дисциплину, студентов направления подготовки... | ||
Программа дисциплины «трудовые споры. Медиация в разрешении индивидуальных... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и обучающихся по магистерской программе... | Программа дисциплины для направления подготовки магистра для магистерской программы Федеральное государственное автономное образовательное учреждение высшего профессионального образования | ||
Программа дисциплины [Введите название дисциплины] для направления/... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки/ специальности,... | Программа дисциплины Консультирование и коучинг персонала Факультет... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 030300.... | ||
Программа дисциплины Поведение потребителей для направления 080200.... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 080200.... | Программа дисциплины Поведение потребителя для направления 080200.... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 080200.... | ||
Программа дисциплины «История политической и правовой мысли зарубежных... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления 030900. 68 “Юриспруденция”... | Программа дисциплины [Введите название дисциплины] для направления/... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 031900.... | ||
Программа дисциплины Моделирование реальных инвестиций и рисков проекта... ... | Программа дисциплины «вления» для направления 081100. 68 "Государственное... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 081100.... |