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).
Felica Networks, Japan
Scott Lintelman/Richard Robinson
Towards Rigorous Architectures
Nokia, Services & Software, Finland
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.
Peter Gorm Larsen
Engineering College of Aarhus, Denmark
CLRC Rutherford Appleton Laboratory, UK
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.
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.
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.
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.
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
(Revisiting the project after 10 years)
Acision, The Netherlands
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.
|Email: firstname.lastname@example.org, Phone: +358 2 215 4754, Fax: +358 2 215 4732|