Co-located Workshops
Registrants of main conference can attend these workshops without additional fee.
-
Monday 09:00 - 18:15, 27 October 2008
First IEEE International workshop UML and Formal Methods (UML&FM'08)
-
Tuesday, 28 October 2008
First International Workshop on Formal Methods Education and Training (FMET) 2008
Half Day Tutorials
Registrants of main conference can attend these tutorials without additional fee.
-
Monday 13:00 - 17:00, 27 October 2008
Secure stepwise refinement: Beating the Refinement Paradox
Associate Professor of Department of Computing at Macquarie University
Stepwise refinement[Wirth 71] is the top-down presentation of a software system's functionality as a sequence of layers of increasing detail, beginning with the very abstract and ending with the very concrete, and with each layer an incremental refinement of the previous one. Making the separation between layers small means that each refinement step can be kept under conceptual control, in many cases even verified correct. Even though actually developing systems this way remains a theoretical ideal (sometime achieved), the refinement framework is in practice provides a framework for encouraging correct, accountable and even efficient code. In spite of the conceptual and practical impact of Stepwise Refinement, it has not until recently incorporated a general treatment of security properties: this is due to the "Refinement Paradox," a fundamental interaction even confusion between abstraction and ignorance which appears to prevent refinement from preserving security properties. The theme of this tutorialis to explore the relationship between refinement and security properties and to explain how a recent breakthrough has allowed standard refinement to be adjusted so that even security properties can be preserved. The tutorial will describe some of the underlying mathematical principles of refinement and security, will illustrate the paradox, and then will show how -by avoiding it- the refinement method can after all be applied to well-known security problems.
-
Tuesday 09:00 - 12:30, 28 October 2008
Industrial Applications of Formal Methods: The current status and challenges of practical applications (This Tutorial is given in Japanese)
Fumihiro Kumeno
Formal methods are applied for significant systems of avionics, railways, etc. In recent years, practical applications are also reported in the field of operating systems, embedded systems and security. Some Japanese software companies begin to use formal methods for their practical developments. We have surveyed the recent practical applications by reviewing proceedings in the past four years and by interviewing some companies in which formal methods are practically used. In this tutorial, we will overview recent industrial applications based on our research and discuss the success factors and problems for practical uses.
2008 年 10 月 28 日 (火) 午前 9 時 - 午後 0 時 30 分
形式手法の産業応用はどこまで進んでいるか？−現状と課題− （本チュートリアルは日本語で行います。）
粂野 文洋
形式手法は、欧米において、航空・宇宙、鉄道、エネルギーなど重要インフラにおける制御システムなどの開発に適用されてきた。 近年では、OS、組み込みシステム、セキュリティの分野でも利用が始まっており、日本でも実適用を行う企業が現れはじめている。 本チュートリアルでは、国際会議での最新動向調査に基づいた形式手法応用の最新動向を俯瞰するとともに、国内外の企業に対するインタビュー調査から得られた導入に向けての成功要因や課題を説明する。
-
Tuesday 13:30 - 17:00, 28 October 2008
Application of a Formal Specification Language in the Development of the Industrial System (This Tutorial is given in Japanese)
Taro Kurita and Yasumasa Nakatsugawa
Senior Manager, Development Department of FeliCa Networks, Inc., FeliCa Business Div., B2B Solutions Business Group, SONY Corporation
We applied the formal specification language VDM++ in the development of firmware of the "Mobile FeliCa" IC chip. As an outcome, we have achieved successful results and confirmed its effectiveness.
The objectives of applying a formal method were as follows:
(1) Description of rigorous specifications;
(2) Development and application of a scheme and processes for specification development, firmware implementation and testing;
(3) Enhancing the quality of deliverables at the upper stream of development process;
(4) Testing thoroughly with formal specifications for whole software development processes;
(5) Improvement of communication between engineers.
This tutorial is an introduction to the formal methods, the formal specification languages and the construction of industrial system using VDM++ and VDMTools.2008 年 10 月 28 日 (火) 午後 1 時 30 分 - 午後 5 時
実システム開発への形式仕様記述手法の適用 (本チュートリアルは日本語で行います．)
栗田 太郎，中津川 泰正
フェリカネットワークス株式会社 開発部 2 課 統括課長， ソニー株式会社 B2B ソリューション事業本部 FeliCa 事業部
第一部では，まずはじめに，形式手法と形式仕様記述，それらの基礎となる数理論理学の概要を説明し，その後，具体的な仕様記述例とともに，形式仕様記述言語とツールを紹介します．
第二部では，「おサイフケータイ」用モバイル FeliCa IC チップファームウェア開発プロジェクトにおける，形式仕様記述手法の適用事例を報告します．
主たるテーマは，ソフトウェア開発の上流工程における品質確保や，プロジェクト内外のコミュニケーションの活性化方法です．一般的なソフトウェア開発プロジェクトが抱える課題を解決するために，既存の開発プロセスに対する形式手法の適用方法や，自然言語・UML・形式仕様記述言語・モデル検査手法の使い分けについて提案します．