FM 2008

Industry Day

One day is dedicated to sharing the experience – both positive and negative – with using formal methods in industrial environments. The Industry Day is co-organized by ForTIA, the Formal Techniques Industry Association. This year's Industry Day is supported by Nokia and investigates telecommunications and embedded systems. Invited papers on organizational and technical issues will be presented. Inquiries should be directed to the Industry Day Chairs, Peter G. Larsen (Eng. College of Aarhus) and Sari Leppänen (Nokia, Helsinki).

Morning session

8.45-9.00 Welcome
9.00-10.00"Getting Formal Verification into Design Flow"
Prof. Arvind, MIT, USA

Coffee break

10.30-11.00 Towards Rigorous Architectures
Ari Ahtiainen, Nokia, Finland
11.00-11.30 Survey on industrial applications of formal methods
Prof. Peter Gorm Larsen, Engineering College of Aarhus, Denmark
11.30-12.00 Application of a Formal Specification Language in the Development of the ``Mobile FeliCa'' IC Chip Firmware for Embedding in Mobile Phone
Taro Kurita, FeliCa Networks Inc., Japan

Lunch

Afternoon session

13.30-14.00 Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution
Scott Lintelman, Boeing Phantom Works, USA
14.00-14.30 Safe and Reliable Metro Platform Screen Doors Control/Command Systems
Thierry Lecomte, ClearSy, France
14.30-15.00 An industrial case: pitfalls and benefits of applying formal methods to the development of a network-centric RTOS
Eric Verhulst, Open License Society, Belgium

Coffee break

15.30-16.00 Software Engineering with Formal Methods: Experiences with the development of a Storm Surge Barrier Control System
Klaas Wijbrans, Acision, The Netherlands
16.00 Wrap-up & closing

Speakers/Companies

professor Arvind
Massachusetts Institute of Technology, USA

Arvind is the Johnson Professor of Computer Science and Engineering and a research director of MIT's Computer Science and Artificial Intelligence Laboratory. He leads the Computation Structures Group, which aims at enabling the creation and development of high-performance, reliable and secure computing systems that are easy to interact with. The group is currently conducting research in the areas of hardware synthesis, computer security, computer architecture and VLSI design.

Nokia, Finland
Nokia is the world leader in mobility, driving the transformation and growth of the converging Internet and communications industries. Nokia makes a wide range of mobile devices and provides people with experiences in music, navigation, video, television, imaging, games and business mobility through these devices. Nokia also provides equipment, solutions and services for communications networks.

Felica Networks, Japan
FeliCa Networks is developing a new lifestyle where mobile handsets can be used for various applications such as e-wallet, credit card, transportation tickets etc.

Scott Lintelman/Richard Robinson
Boeing, USA

Boeing is the world's leading aerospace company and the largest manufacturer of commercial jetliners and military aircraft combined. Additionally, Boeing designs and manufactures rotorcraft, electronic and defense systems, missiles, satellites, launch vehicles and advanced information and communication systems. As a major service provider to NASA, Boeing operates the Space Shuttle and International Space Station.

Klaas Wijbrans
Acision/LogicaCMG, the Netherlands

Acision is a subsidiary of LogicaCMG which is one of the major European providers in IT services. They deliver solutions of complex mission critical systems in a number of industrial sectors.

Eric Verhulst
Open License Society, Belgium

The Open License Society is a R&D company aiming at greatly improving the process used to develop systems. The initial approach aims at providing the core tool chain centered round the concept of Communicating Objects, complemented with third party tools and reference platforms. Each tool is made available to a wider member community under the terms of the Open Licensing model, with access to source code and all design documents. With design documents we mean all documents generated during the development phase, a user manual and if applicable the formal analysis and validation.



Abstracts:



Towards Rigorous Architectures

Sari Leppänen
Nokia, Services & Software, Finland

Ari Ahtiainen
Nokia Research Center, Finland

Abstract: Over the past 10 years Nokia Research Center, together with theoretical computer science research teams from several universities, has studied application of formal specification, verification and testing methods in the development of industrial scale distributed systems, like mobile networks and radio system protocols as well as software architectures for mobile multimedia computers. The case studies and pilot projects used in these industry-academy collaboration projects have greatly influenced both the industrial approach for adapting formal methods and the academic research focus and progress in formal methods and tools. However, the size and complexity of such industrial-scale distributed systems still tends to exceed the capabilities of the state of the art methods and tools. One obstacle in bringing the discipline forward is lack of commercially productized tools for creation and analysis of models in such an intuitive manner which would lead to large-scale industrial adoption of the methods for everyday industrial use. We suggest that in further research and tool development the focus will move into rigorous specification of high-level system architectures, where formal methods can play a key role in ensuring that architectural design principles are prevalent throughout the lifecycle of the product.

Presentation (PDF)


Survey of industrial applications of formal methods

Peter Gorm Larsen
Engineering College of Aarhus, Denmark

Juan Bicarregui
CLRC Rutherford Appleton Laboratory, UK
John Fitzgerald
Newcastle University, UK

Abstract. We have been conducting a survey of the state of the art in the industrial application of formal methods. We have gathered information about as many industrial formal methods applications as possible with the assistance of many different stakeholders. The prime form for gathering this information has been a questionnaire specially designed for that purpose. This presentation will be the first reporting on the different trends that have come out of this survey. Subsequently we expect to publish a more comprehensive report of our findings.

Presentation (PDF)


Application of a Formal Specification Language in the Development of the ``Mobile FeliCa'' IC Chip Firmware for Embedding in Mobile Phone

Taro Kurita
FeliCa Networks Inc., Japan

Miki Chiba and Yasumasa Nakatsugawa
Sony Corporation, Japan

Abstract: We have adopted formal specification language in the development of firmware of ``Mobile FeliCa'' IC chip and have achieved successful results and confirmed its effectiveness.

Presentation (PDF)
Handouts (PDF)


Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution
Scott Lintelman, Richard Robinson, Mingyan Li, Krishna Sampigethaya
Boeing Phantom Works, USA

Abstract. A recent application in commercial aviation is the electronic distribution of loadable software parts and data. Its safe and beneficial use, however, warrants that information security vulnerabilities are analyzed and mitigated at an adequate assurance level. In our prior work, we have identified security threats and assurance requirements for a generic aircraft asset distribution system or AADS. In this paper, we focus on supporting analytical processes to address security vulnerabilities as well as describing our experiences in applying formal methods to AADS.

Presentation (PDF)


Safe and Reliable Metro Platform Screen Doors Control/Command Systems

Thierry Lecomte
ClearSy, France

Abstract. In this article we would like to present some recent applications of the B formal method to the development of safety critical system. These SIL3/SIL41 compliant systems have their functional specification based on a formal model. This model has been proved, guaranteeing a correct by construction behaviour of the system in absence of failure of its components. The constructive process used during system specification and design leads to a high quality system which has been qualified by French authorities.

Presentation (PDF)


An industrial case: pitfalls and benefits of applying formal methods to the development of a network-centric RTOS

Eric Verhulst, Gjalt de Jong and Vitaliy Mezhuyev
Open License Society, Belgium

Abstract. This paper describes a project to develop a network-centric RTOS from scratch using formal methods. The (initial) purposes of the project was to get acquainted with the use of formal methods for software engineering and to obtain a trustworthy RTOS as a component for building networked embedded systems. The work was done by a small, distributed team that had no prior experience on using formal methods and with a small budget. The outcome is that the use of formal methods is most useful as an architectural design method, more than as a formal verification of software code. The resulting software has many properties that were not anticipated at the beginning and would likely not have been achieved without the use of Formal Methods

Presentation (PDF)


Software Engineering with Formal Methods: Experiences with the development of a Storm Surge Barrier Control System
(Revisiting the project after 10 years)

Klaas Wijbrans
Acision, The Netherlands

Franc Buve
Robin Rijkers
Wouter Geurts
Logica, The Netherlands

Abstract. This paper revisits the experiences with the use of formal methods in the development of the control system for the Maeslant Kering. The Maeslant Kering is the movable barrier which has to protect Rotterdam from floodings while, at almost the same time, not restricting shipping traffic to the port of Rotterdam. The control system, called BOS, completely autonomously decides about closing and opening of the barrier and, when necessary, also performs these tasks without human intervention. BOS is a safety-critical software system of the highest Safety Integrity Level according to the IEC 61508 standard. One of the reliability increasing techniques used during its development is formal methods. This paper revisits the earlier published experiences with the project after the system is now in operation for ten years and has performed its first barrier operation because of a storm on November 11th, 2007.

Presentation (PDF)