Modeling and Verification of Embedded Real-Time Systems
- Prof. Wang Yi, Uppsala Univ. : 발표자료[1, 2, 3, 4]

In recent years, the international community has made several significant advances in modeling and verification of real time systems. A number of verification tools have been developed, and available for research and education as well as industrial applications. The goal of my lectures is to introduce the theories, algorithms and data structures behind the UPPAAL tool developed jointly by Uppsala University and Aalborg University (sample slides are attached in this application). It will cover models for finite state systems and introduction to temporal logics and model checking. The focus will be put on the theory of timed automata covering the syntax, semantics, verification problems, and techniques for symbolic reachability analysis which is the core of the UPPAAL tool. We will introduce the UPPAAL modelling and specification languages (the GUI) and the model checker as well as case studies to show how to use the tool to model and solve problems. 

Parsing theory -  최광무교수, KAIST

Context-free language를 위한 두가지 파싱 방식인 bottom-up parsing과 top-down parsing에 대한 직관적인 설명를 통해 parsing theory의 이해를 도모하고자 한다. 

효율적인 함수형 언어: Erlang - 이만호교수, 충남대

Erlang은 함수형 언어로서, fault-tolerance가 요구되는 concurrent, real-time, distributed system에 적합한 언어이다. 함수형 언어는 실행 성능이 떨어진다는 것이 일반적인 견해이나, Erlang 언어는 실시간, 병행, 분산 시스템 구현에 매우 우수한 실행 성능을 보여주고 있다. 본 강좌에서는 이런 시스템을 구현하기 위해 필요한 Erlang 언어의 특징에 대해 소개한다.