Analysis and design of correct real-time safety-critical software

• Autorzy: Kosęda B.

Warianty tytułu

PL

Analiza i projektowanie poprawnych systemów czasu rzeczywistego o podwyższonych wymaganiach bezpieczeństwa

• Języki publikacji: EN

Abstrakty

EN

High-energy physics experiments rely on large hardware installations. As these machines become more and more advanced, their maintenance becomes a complex task. The free-electron laser FLASH is not an exception. It is designed for delivering a high quality laser beam to scientific experiments round the clock. Each machine standstill costs extra money. Therefore, the maximization of its uptime plays an important role. Automation software is a means for improving machine availability. One expects to improve the machine uptime by automating routine tasks performed by the operators and by providing auto-recovery supervision software. The efforts presented in this contribution concern the elaboration of a general framework for the design and development of safe and predictable automation software. Devised tools and design methods are evaluated during the implementation of the automation software for a single RF-power station of the FLASH.

PL

Eksperymenty fizyki wysokich energii są możliwe dzięki zastosowaniu skomplikowanych instalacji eksperymentalnych. Z roku na rok urządzenia te stają się coraz bardziej skomplikowane a ich obsługa oraz serwisowanie staje się coraz bardziej złożona. Laser na elektronach swobodnych FLASH nie jest wyjątkiem. Jest to skomplikowane 260-metrowe urządzenie wykorzystujące najnowsze rozwiązania technologiczne. Laser ten produkuje wysokiej jakości wiązkę laserową. Ponieważ FLASH jest projektem komercyjnym, każdy zastój urządzenia wiąże się ze stratami finansowymi, Zadaniem oprogramowania nadzorującego pracę podsystemów akceleratora jest wydłużenie czasu jego poprawnej pracy. Zakłada się, że ten cel może być osiągnięty za pomocą automatyzacji rutynowych zadań wykonywanych przez operatorów oraz opracowania oprogramowania usuwającego symptomy drobnych awarii. Zagadnienia poruszane w artykule dotyczą opracowania metodyki i zestawu narzędzi do projektowania i implementacji oprogramowania automatyzującego. Prezentowane podejście i narzędzia omawiane są w kontekście systemu automatyzacji pojedynczej stacji zasilania lasera FLASH.

Słowa kluczowe

EN

automatization; real-time; formal verification; free electron laser FLASH

PL

automatyzacja; czas rzeczywisty; weryfikacja formalna; laser na elektronach swobodnych FLASH

• Wydawca: Wydawnictwo Politechniki Łódzkiej
• Czasopismo: Zeszyty Naukowe. Elektryka / Politechnika Łódzka
• Rocznik: 2008
• Tom: z. 115
• Strony: 59--67
• Opis fizyczny: Bibliogr. 15 poz.

Twórcy

autor

Kosęda B.

• Technical University of Łódź, Department of Microelectronics and Computer Science

Bibliografia

• [1] Aghababyan A., Altarelli M. et al.: XFEL The European X-Ray Free-Electron Laser Technical Design Report, ISBN 3-935702-17-5 (2006).
• [2] Hensler O., Rehlich K.: DOOCS: a Distributed Object Oriented Control System Proceedings of XV Workshop on Charged Particle Accelerators, Protvino (1996).
• [3] Ayvazyan V., Rehlich K., Simrock S., Sturm N.: Finite State Machine Implementation to Automate RF Operation at the TESLA Test Facility Proceedings of the Particle Accelerator Conference, Chicago (2001).
• [4] Koseda B., Cichalewski W.: Design and Implementation of Finite State Machine for RF Power Station Proceedings of the 12th International Conference Mixed Design of Integrated Circuits and Systems, Cracow, Poland (2005).
• [5] Koseda B., Cichalewski W.: Improvements of Expert System for RF-Power Stations Proceedings of the 13th International Conference Mixed Design of Integrated Circuits and Systems, Gdynia, Poland (2006).
• [6] Brandt A., Cichalewski W., Koseda B., Simrock S.: Automation of Iow level RF control operation for the VUV-FEL at DESY and future accelerators Proceedings of SPIE, Photonics Applications in Industry and Research IV 5948 (2005).
• [7] Wagner F.: Modeling Software with Finite State Machines: A Practical Approach, ISBN 0-8493-8086-3 (2006).
• [8] MathWorks, Inc.: Stateflow and Stateflow Coder User's Guide.
• [9] Cimatti A., Clarke E. et al.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking Proceeding of International Conference on Computer-Aided Verification, Copenhagen, Denmark (2002).
• [10] Huth M., Ryan M.: LOGIC IN COMPUTER SCIENCE, Modelling and Reasoning about Systems, ISBN 0-521-54310-X (2004).
• [11] Holzmann G.: SPIN Model Checker, The: Primer and Reference Manuał, ISBN: 0-321-22862-6 (2004).
• [12] Wielemaker J.: SWI-Prolog 5.6 Reference Manual http://gollem.science.uva.nl/SWI-Prolog/Manual/
• [13] Free On-Line Dictionary of Computing, http://foldoc.org/
• [14] Harel D.: Statecharts: A Visual Formalism for Complex Systems Science of Computer Programming 8 (1987) 231-274.
• [15] Storey N.: Safety Critical Computer Systems, Addison Wesley 1996, ISBN 0-201-42787-7.