DEPLOY Industry Day

Experience in Formal Modelling of Mode-Rich Systems in the Space Sector

• Presenter : Timo, Space Systems (Finland)
• Description : In our talk we would like to reflect on the experience in the industrial-scale development of a satellite embedded software that was undertaken recently in the Deploy project. Space Systems Finland with support from Åbo Akademi and Newcastle universities has undertaken development of the Attitude and Orbit Control System (AOCS).  AOCS is a generic component of satellite onboard software. AOCS is also a typical representative of mode-rich component-based control systems with a complex mode transition scheme.  There are two distinctive characteristics that make AOCS development and verification challenging.  The first one is long running (i.e., non-instantaneous) mode transitions that are caused by slow dynamics of the involved electro-mechanical components.  The second characteristic is an integration of error recovery with mode transition scheme, i.e., error recovery is implemented as rollbacking to certain degraded modes.  Together, these two features may lead to cascading mode transitions, i.e., the situations when a system transition to one mode is preempted by a transition to another (degraded) mode due to failure occurrences.

Formal Methods in the Engineering of Enterprise Applications

• Presenter : Andreas Roth, SAP
• Description : In this talk we will present the experiences with the deployment of formal methods in the engineering of enterprise applications which we made during the DEPLOY project at SAP. This includes the formal modeling of business processes and interactions with the help of Event-B, as well as the use of tooling developed in the context of DEPLOY for verifying and validating enterprise applications with respect to these models.

Possible Applications of Event-B in Small Industries

• Presenter : Aryldo Russo, AeS
• Description : During the last four years we have been applying formal methods, namely B/Event-B, in the context of DEPLOY project, first as partitioner and, at the end, as an Associate. Instead of changing the complete development process, we try to apply formal methods in distinct and different areas in order to extract as much benefits as possible whereas not impacting so much in the current life of the R&D department. In this presentation I present our achievements in these punctual applications, such as, requirements elicitation, requirement inconsistencies (find and fix), support for safety validation among others.

The XCore Instruction Set Architecture in Event-B

• Presenter : Stephen Wright, XMOS
• Description : The XCore microprocessor is an embedded device developed by XMOS Ltd of Bristol, UK, and has been deployed in a range of different markets, including audio, display, communications, robotics and motor control. The Instruction Set Architecture (ISA) contains a range of typical instructions, but also provides support for efficient synchronized multi-threaded programming and parallelism with other devices via fast interconnects. Support for these features is integrated into the ISA of the XCore, greatly improving run-time performance at the cost of introducing specialist instructions to the ISA. As part of a Bristol University Knowledge Transfer Secondment, a formal model of the complete ISA was constructed in Event-B, using the Rodin toolset. This project applied and extended the Event-B and RODIN based techniques for Instruction Set Architecture (ISA) analysis, developed by Dr Stephen Wright during his doctoral research, to an industrial setting. To that end, XMOS Ltd hosted Dr Wright in the period October 2010 to October 2011. In this talk, Dr Wright presents the technical, procedural, and cultural experiences of the project.

Formal proofs for the NYCT line 7 (Flushing) modernization project

• Presenter : Denis Sabatier, ClearSy
• Description : The New York City subway Line 7 (Flushing) modernization project consists in in-stalling a Communication Based Train Control (CBTC) system and updating the existing interlocking system. The CBTC system is designed and installed by THALES Toronto. The main benefits of this modernization will be a reduced headway, signals and track circuits simplification, and extended routing possibilities, for instance in case of track failures. The New York City Transit authority (NYCT) decided to include formal proofs at system level as part of the safety assessment for this project. The French SME ClearSy is responsible for these proofs, using the Event-B method. In this presentation, we discuss the methodology applied to obtain these formal proofs and the conclusions so far.

Event-B for Embedded Systems

• Presenter : Jose Reis, CSWT
• Description : In the scope of EU and UK Mod funded projects, CSWT has been exploring the use of Event-B and the Rodin toolset to verify properties of embedded systems, be it COTS based solutions used in the combat systems of nuclear powered submarines or bespoke solutions such as smart electricity grid components. The scope of verification and validation activities for such systems is often defined by the software criticality and applicable standards such as DO-178 or ECSS-40. The test coverage and the evidence required can vary but the effort needed to generate good findings is usually high and the analysis often relies on the engineering experience and skill.  This presentation will demonstrate the preliminary achievements and conclusions as to how we see Event-B and the Rodin toolset evolving to better support the verification and validation of embedded systems in the future.

Event-B Modelling of a CBTC System and its (3D) Animation

• Presenter : Thomas Muller, Systerel
• Description : The development of highly constrained systems requires advanced studies and rigorous approaches, in order to produce high-quality systems. Event-B, as a formal method for system-level analysis, provides a mathematical way to understand the considered system and mitigate hazards, by modeling it and proving the associated safety requirements. SYSTEREL, SME specialized in safety-critical embedded systems, worked in 2010 on a large railway transportation system using this method, and will relate in its presentation the developed process and gains of adopting such method.

A Collaborative FAQ Approach for Collecting Evidence on Formal Method Industrial Usage

• Presenter : Jean Christophe Deprez & Christophe Ponsard, Cetic
• Description : After several decades, formal methods are gaining ground in Industry. However, as pointed out by the results of Woodcock et al's survey, formal methods still need significant additional effort in several areas, most notably in collecting evidence on the use of formal methods and tools in Industry. Such material is crucial for helping companies considering the adaption of formal methods in their decision and deployment process. This talk presents a practical approach for building a repository of evidence material. The main benefits of the proposed approach are first to make it possible to integrate information for many Industry pilots that have tested diverse formal methods. The secondary benefit is that the current implementation of the repository as a wiki of that project is simple yet efficient in managing access but also contribution rights. We highlight different usage scenarios both as passive user, from different roles in the organization, and as contributors, either to point out missing material or as provider of new material.

Formal Mind, ProB, ProR and Data Validation with B

• Presenter : Michael Leuschel, Formal Mind
• Description : I will briefly present the spin-off company Formal Mind (http://www.formalmind.com/) and the ProB and ProR tools which are at the heart of the services offered by the company. In particular, I will present how ProB is used for data validation at Siemens and Alstom.