Search

An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to perform the experiments they are designed for. This often leads to the design of configurable software that can absorb these changes and perform the required control and protection actions. This design strategy minimizes the engineering and maintenance costs, but it makes the software verification activities more challenging since safety properties must be guaranteed for any of the possible configurations. Software model checking is a popular automated verification technique in many industries. This verification method explores all possible combinations of the system model to guarantee its compliance with certain properties or specification. This is a very appropriate technique for highly configurable software, since there is usually an enormous amount of combinations to be checked. This paper presents how PLCverif, a CERN model checking platform, has been applied to a highly configurable Programmable Logic Controller (PLC) program, the SPS Personnel Protection System (PPS). The benefits and challenges of this verification approach are also discussed., Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, ICALEPCS2021, Shanghai, China

Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software., 18th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS2021)

In this paper we report the experience from a large-scale upgrade campaign of SCADA control systems performed during the second LHC Long Shutdown at CERN. Such periodical upgrades are dictated by the ever evolving SCADA WinCC OA system and the CERN frameworks evolution used in those control systems. These upgrades concern: accelerator control systems, e.g. quench protection system, powering interlocks, magnet alignment; control systems devoted to accelerator facilities such as cryogenics, vacuum, gas��� and other global technical infrastructure systems as well as the CERN electrical distribution system. Since there are more than 200 SCADA projects covering the CERN accelerator complex and technical infrastructure, any disruption requires careful coordination, planning and execution with process owners. Having gained experience from previous campaigns and reaching a new level of automation we were able to make visible improvements by shortening the required time and reducing the personnel required. Activities, lessons learned and further improvements are presented as well as a comprehensive statistical insight of the whole campaign., Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, ICALEPCS2021, Shanghai, China

The CERN industrial control systems, using WinCC OA as SCADA (Supervisory Control and Data Acquisition), share a common history data archiving system relying on an Oracle infrastructure. It consists of 2 clusters of two nodes for a total of more than 250 schemas. Due to the large number of schemas and of the shared nature of the infrastructure, three basic needs arose: (1) monitor, i.e. get the inventory of all DB nodes and schemas along with their configurations such as the type of partitioning and their retention period; (2) control, i.e. parameterise each schema individually; and (3) supervise, i.e. have an overview of the health of the infrastructure and be notified of misbehaving schemas or database node. In this publication, we are presenting a way to monitor, control and supervise the data archiving system based on a classical SCADA system. The paper is organized in three parts: the first part presents the main functionalities of the application, while the second part digs into its architecture and implementation. The third part presents a set of use cases demonstrating the benefit of using the application., Proceedings of the 17th International Conference on Accelerator and Large Experimental Physics Control Systems, ICALEPCS2019, New York, NY, USA

The Industrial Controls and Safety systems group at CERN, in collaboration with other groups, has developed and currently maintains around 200 controls applications that include domains such as LHC magnet protection, cryogenics and electrical network supervision systems. Millions of value changes and alarms from many devices are archived to a centralised Oracle database but it is not easy to obtain high-level statistics from such an archive. A system based on the Elastic Stack has been implemented in order to provide easy access to these statistics. This system provides aggregated statistics based on the number of value changes and alarms, classified according to several criteria such as time, application domain, system and device. The system can be used, for example, to detect abnormal situations and alarm misconfiguration. In addition to these statistics each application generates text-based log files which are parsed, collected and displayed using the Elastic Stack to provide centralised access to all the application logs. Further work will explore the possibilities of combining the statistics and logs to better understand the behaviour of CERN's controls applications., Proceedings of the 16th Int. Conf. on Accelerator and Large Experimental Control Systems, ICALEPCS2017, Barcelona, Spain

The paper describes planning and execution of large-scale maintenance campaigns of SCADA systems for CERN accelerator and technical infrastructure. These activities, required to keep up with the pace of development of the controlled systems and rapid evolution of software, are constrained by many factors, such as availability for operation and planned interventions on equipment. Experience gathered throughout the past ten years of maintenance campaigns for the SCADA Applications Service at CERN, covering over 230 systems distributed across almost 120 servers, is presented. Further improvements for the procedures and tools are proposed to adapt to the increasing number of applications in the service and reduce maintenance effort and required downtime., Proceedings of the 16th Int. Conf. on Accelerator and Large Experimental Control Systems, ICALEPCS2017, Barcelona, Spain

CERN describes the Detector Control Systems (DCSes) of the experiments of the Large Hadron Collider using finite state machines organised in a hierarchical directed acyclic graph structure. These systems are huge and impossible to understand only with human intervention, so computer checking is needed. Before the introduction of the tool described in this document, the analysis of the code controlling the DCSes was performed few times a week, introducing problem solving delay. The tool proposed allows an online time checking of the detectors’ Control Units, thanks to the integration with the WinCCOA panel. WinCCOA is a SCADA (Supervisory Control and Data Acquisition) system tool that is used to develop the Control System applications at CERN. Chapter breakdown: Chapter 1: introduction to the environment, explaining why the project has been proposed and what is the aim of the tool in solving current problems. Chapter 2: description about the framework that manage the control environment at CERN, and main concepts of the language that must be controlled by the tool. Chapter 3: general illustration of the employed tools, ACE and PEG.js Chapter 4: description on how the work has been implemented, from the setting up of the work environment, to the syntax rules and error reporting Chapter 5: future development of the tool Chapter 7: conclusions

Abstract WinCC OA is a SCADA (Supervisory Control and Data Acquisition) system tool that is used to develop the Control System applications. As most of the control systems used in CERN are developed in WinCC OA, it is better useful to understand how the applications developed by EN/ICE are actually used by the different operators .It becomes more and more important to monitor users’ behavior and analyzing it. The final goal of this project is to develop a generic WinCC OA component to collect data about user interaction which will take advantage of (1) the internal mechanisms already present in WinCC OA to monitor some user interactions such as the internal UI data points; and (2) the commonalities of applications through the use of the standard frameworks JCOP, UNICOS and CPC. The final component developed provides the capability of storing as well as displaying user interaction data on a single timeline. Kewords: WinCC OA, SCADA, JCOP, UNICOS, CPC

Component-Based Software Engineering is quickly becoming a mainstreamapproach to software development. At the same time, there is a massiveshift from desktop applications to embedded communicating systems(e.g. PDAs or smartphones): it is especially the case for multimediaapplications such as video players, music players, etc. Moreover,embedded communicating systems have to deal with open aspect:applications may come or leave the system on the fly. A key point ofthese systems is its ability to rigorously manage Quality of Servicedue to resource constraints. In this thesis, we present acomponent-based QoS architecture well-suited for open systems, calledQinna. Qinna is defined using Fractal components and takes intoconsideration the main QoS concepts (specification, provision andmanagement) through the use of contracts between components. The Qinnaarchitecture allows to deal with QoS of each layer of a system(application, services, operating system, resources) in order to havea fine grain management of resources. The architecture has been firstvalidated thanks to a qualitative evaluation using genericarchitectural pattern. Then, Qinna has been validated from aquantitative point of view in order to demonstrate its low cost.Finally, this work opens many research perspectives such as thegeneralization of the architecture to other non functional properties(security, fault tolerance, etc.)., Les systèmes embarqués communicants sont de plus en plus présents dans notre environnement quotidien sous formes de PDA, téléphones portables, etc. Ces sytèmes se doivent d'être ouverts afin de pouvoir accueillir de nouvelles applications tout au long de leur cycle de vie. Ils possèdent alors des contraintes fortes de types qualité de service, sécurité, tolérance aux fautes, etc. La programmation à base de composants apparaît comme une solution prometteuse pour le développement de tels systèmes. Cependant, un des frein à l'adoption de ce type de programmation est que les modèles à composants n'intègrent pas les aspects de gestion de qualité de service. Ce travail de thèse présente une architecture de gestion de qualité de service pour les systèmes embarqués mobiles à composants. Cette architecture, appelée Qinna, est définie à l'aide de composants Fractal et permet la mise en œuvre, ainsi que la gestion dynamique, de contrats de qualité de service entre les différents composants d'un système. L'originalité de l'approche proposée permet de prendre en compte la qualité de service quelque soit le niveau considéré du système (niveau applicatif, niveau services, niveau système d'exploitation et niveau ressources).L'architecture Qinna a été validée par une évaluation qualitative à base de patrons génériques d'architecture, puis par une évaluation quantitative permettant de montrer que le coût de l'architecture reste faible.Le travail réalisé ouvre de nombreuses perspectives de recherche notamment celle de généraliser l'approche utilisée (définition d'une architecture abstraite de composant pour la prise en charge de la gestion d'une propriété non-fonctionnelle, ici la QdS) à d'autres propriétés non-fonctionnelles (par exemple la sécurité ou la tolérance aux fautes), et d'en tirer des conclusions sur la définition et la génération de conteneurs ouverts.

Component-Based Software Engineering is quickly becoming a mainstreamapproach to software development. At the same time, there is a massiveshift from desktop applications to embedded communicating systems(e.g. PDAs or smartphones): it is especially the case for multimediaapplications such as video players, music players, etc. Moreover,embedded communicating systems have to deal with open aspect:applications may come or leave the system on the fly. A key point ofthese systems is its ability to rigorously manage Quality of Servicedue to resource constraints. In this thesis, we present acomponent-based QoS architecture well-suited for open systems, calledQinna. Qinna is defined using Fractal components and takes intoconsideration the main QoS concepts (specification, provision andmanagement) through the use of contracts between components. The Qinnaarchitecture allows to deal with QoS of each layer of a system(application, services, operating system, resources) in order to havea fine grain management of resources. The architecture has been firstvalidated thanks to a qualitative evaluation using genericarchitectural pattern. Then, Qinna has been validated from aquantitative point of view in order to demonstrate its low cost.Finally, this work opens many research perspectives such as thegeneralization of the architecture to other non functional properties(security, fault tolerance, etc.)., Les systèmes embarqués communicants sont de plus en plus présents dans notre environnement quotidien sous formes de PDA, téléphones portables, etc. Ces sytèmes se doivent d'être ouverts afin de pouvoir accueillir de nouvelles applications tout au long de leur cycle de vie. Ils possèdent alors des contraintes fortes de types qualité de service, sécurité, tolérance aux fautes, etc. La programmation à base de composants apparaît comme une solution prometteuse pour le développement de tels systèmes. Cependant, un des frein à l'adoption de ce type de programmation est que les modèles à composants n'intègrent pas les aspects de gestion de qualité de service. Ce travail de thèse présente une architecture de gestion de qualité de service pour les systèmes embarqués mobiles à composants. Cette architecture, appelée Qinna, est définie à l'aide de composants Fractal et permet la mise en œuvre, ainsi que la gestion dynamique, de contrats de qualité de service entre les différents composants d'un système. L'originalité de l'approche proposée permet de prendre en compte la qualité de service quelque soit le niveau considéré du système (niveau applicatif, niveau services, niveau système d'exploitation et niveau ressources).L'architecture Qinna a été validée par une évaluation qualitative à base de patrons génériques d'architecture, puis par une évaluation quantitative permettant de montrer que le coût de l'architecture reste faible.Le travail réalisé ouvre de nombreuses perspectives de recherche notamment celle de généraliser l'approche utilisée (définition d'une architecture abstraite de composant pour la prise en charge de la gestion d'une propriété non-fonctionnelle, ici la QdS) à d'autres propriétés non-fonctionnelles (par exemple la sécurité ou la tolérance aux fautes), et d'en tirer des conclusions sur la définition et la génération de conteneurs ouverts.