Analysis of ACS using mCRL2
Scw Bas Ploeger · TU/e Research Portal · 2009
Introduction. The Atacama Large Millimeter Array (ALMA) is a space observatory system that is currently being developed by astronomical organizations in Europe, North-America and Japan. It will consist of at least 50 antennas that operate in the millimeter and submillimeter wavelength range, and will be built in the Chilean Atacama desert at an altitude of approximately 5000 meters. The ALMA Common Software (ACS) is a software infrastructure for ALMA that is based on CORBA. It is an essential framework within the ALMA software system, providing a collection of common software components and services that other parts of the system rely upon. Therefore, it is important for the ACS platform to be stable and reliable. The purpose of our study is to analyse a part of the ACS framework using formal modelling techniques. In that approach, a model of a software system is constructed, which is subsequently analysed for errors by an exhaustive exploration of all possible states and execution sequences. The aim is to cover a wider range of cases and scenarios than are typically covered by a collection of test cases. We introduce this approach and the modelling framework mCRL2 in more detail in Section 2. The model that we created for ACS is described in Section 3 and the results of the analysis are described in Section 4. The report is concluded in Section 5.