SYRF Project

This deliverable describes the case studies submitted by the industrial partners, and the various results of the project on these case studies.

The case study proposed by Schneider Electric is a Source Range Instrumentation System (SRIS) which is part of a nuclear protection system. Using measurements from neutron detectors, the SR IS controls the emergency shutdown of the reactor and other protection actions to avoid accidental damage. A detailed description of the case study is given in Annex 1.a. Annex 1.b gives the properties that should be proved, and assumptions about the system environment. Both of these documents are confidential, their access is limited to the partners and the reviewers of the project. The results of several tasks were applied to this case study:

• Task 2 (Combination of Formalisms): Reingeniering of SRIS with Mode-Automata (see Annex 1.d).
• Task 3.1 (Symbolic Abstraction of Automata): Verification of SRIS properties with XLESAR (see Annex 1.c).
• Task 3.5 (Use of automata technology and synchronous observers for automatic testing) Automatic testing of the SRIS software with Lurette (see deliverable 3.5.2)

Saab case studies are two examples of reactive systems for regulating temperature, airflow and pressure in closed areas. They are different in size, one small and one large system, but they represent the same type of functionality. The small system is a made up "demo" example representing a climatic chamber and the large one is the Environmental Control System (ECS) in the aircraft JAS 39 Gripen.

• The climatic chamber was successful for evaluating the use of mode-structures within Lustre programs (see Annex 1.g ). It serves as an illustration of many steps "in between" going from an informal document and a synchronous program to formal verification of "hybrid" properties (see Annex 7.??).
• The controller of the ECS has been analyzed by Prover Technology.

The EdF case studies

• The Power Transformer Station (PTS): This case study deals with the incremental specification of a part of a power transformer station controller, using the controller synthesis methodology. It concerns the response to electric faults on the line traversing it. The functionality of this controller is to handle the power interruption, the redirection of supply sources and the re-establishment of the power following an interruption.
  A detailed description of this case study is given in Annex 1.e and a review of the controller synthesis problem can be found in [1]. We applied the results of Task 3.1 (Symbolic Abstraction of Automata) to this case study. They concern the
  • verification of the PTS using SIGALI
  • automatic synthesis of a part of the PTS controller (Task 3.1: controller synthesis part)
  • symbolic abstraction by state fusion of the PTS (Task 3.1: Symbolic Abstraction part)

  [1] H. Marchand, M. Le Borgne.The Supervisory Control Problem of Discrete Event Systems using polynomial Methods.  Research Report Irisa, No1271, October 1999. (Postscript)
  
  

• The Steam Boiler Control Problem : This case study investigates the combined use of the synchronous language SIGNAL and of the proof assistant COQ for specifying and verifying properties of the steam boiler problem.
  The implementation of the steam boiler in SIGNAL consists of four processes. The heart of this architecture is the control process which is in charge of operating the pumps and initially the valve. The three other processes form two kinds of filter which enable to provide to the control process an environment in which it can disregard the management of failures. Notably, this process does not consider possible failures of measurement devices when it decides to activate or deactivate some pumps. Moreover, this process does not consider possible failures of pumps and pump controllers when it decides to stop or not the system.
  The results of Appendix 1.f, reporting on the results of specifying and verifying the steam-boiler problem with this method; giving a detailled description of its implementation in SIGNAL and COQ.