- 国际著名软件和软件理论专家，Z 语言和 B 方法的创建者，软件形式化开发领域的最主要奠基人之一
- 参与和指导了欧洲许多重要的关键性软件开发项目
- 其开发的 B 软件开发方法被欧洲等地区的许多重要企业和部门（如欧洲航天局、西门子、阿尔斯通等）用于轨道交通、高铁、航空、电站等重要领域的信号、控制、调度、自动驾驶等各种关键性系统的建模、验证和系统开发
- 近年领导和参与 B 方法后继的 Event-B 开发和应用的欧共体项目，其参与开发的 Event-B 公开免费工具 Rodin 已被全世界软件/硬件和其他领域的许多理论和实际工作者使用
本课程面向数学、信息等学院研究生和高年级本科生。如果你想了解并掌握
已在国际上成功用于开发许多关键性软件系统的新技术
对软件系统（和一般的基于计算机的系统）的深入分析和建模的严格技术
基于严格的数学和证明的软件（硬件）系统建模和开发过程
本课程适合你的需要。欢迎选课（请到数学学院/研究生课程中选课，接受本科生）
本课程将采用课题讲解和实践相结合的方式。每位上课同学需要带一台笔记本计算机。Abrial 教授将讲授系统的形式化建模和验证技术，并基于 Event-B 给出许多软件（及硬件）系统开发实例。课程中将深入细致地讲解如何严格地分析实际问题，描述系统需求；如何用 Event-B 做系统建模，严格证明所建立的系统模型的正确性；等等。参与本课程的学习，可能帮助人更深入地理解计算机和软件系统，软件开发过程及其问题，并为参与未来的关键性软件的开发打下很好的基础。
Ce cours est destiné aux étudiants diplômés et aux étudiants de dernière année de l'École de mathématiques et d'information. Si vous voulez comprendre et maîtriser De nouvelles technologies qui ont été utilisées avec succès à l’échelle internationale pour développer de nombreux systèmes logiciels critiques Techniques rigoureuses pour l'analyse et la modélisation approfondies des systèmes logiciels (et des systèmes informatiques en général) Processus de modélisation et de développement de systèmes logiciels (matériels) basé sur des mathématiques et des preuves rigoureuses Ce cours est adapté à vos besoins. Bienvenue pour vous inscrire aux cours (veuillez vous rendre à l'École de mathématiques/Cours de deuxième cycle pour vous inscrire aux cours, les étudiants de premier cycle sont acceptés) Ce cours adoptera une combinaison d’explications et de pratiques sur le sujet. Chaque étudiant est tenu d'apporter un ordinateur portable en classe. Le professeur Abrial enseignera les techniques formelles de modélisation et de vérification des systèmes et donnera de nombreux exemples de développement de systèmes logiciels (et matériels) basés sur Event-B. Le cours expliquera en profondeur comment analyser strictement les problèmes pratiques et décrire les exigences du système ; comment utiliser Event-B pour modéliser le système et prouver strictement l'exactitude du modèle de système établi ; et ainsi de suite. La participation à ce cours peut aider les gens à acquérir une compréhension plus approfondie des systèmes informatiques et logiciels, des processus et des problèmes de développement de logiciels, et à jeter de bonnes bases pour participer au développement de futurs logiciels critiques.
相关材料：
- J-R Abrial, Formal Methods in Industry: Achievements, Problems, Future. ICSE2006
- Invited Talk. 中文译文：工业开发中的形式化方法：成就、问题和未来,
- （裘宗燕译）
- J-R Abrial, Faultless Systems: Yes we can! IEEE Computer, Vol.42, No.9, pp30-36. IEEE Computer Society, 2009. 本地下载
- J-R Abrial, Modeling in Event-B: System and
- Software Engineering, Cambridge University Press. 2010
- (Abrial 教授将提供若干章节的文件供选课同学阅读)
Event-B建模 系统和软件工程[法] 简-埃蒙德·阿布瑞尔(Jean-Raymond Abrial)人民邮电出版社
B方法
On y a même des restaurants Z pas loin du labo d'informatique !
Articles
Aucun commentaire:
Enregistrer un commentaire