Thomas Schaberreiter

Sébastien Varrette

Pascal Bouvry

Juha Röning

Djamel Khadraoui

Dependency Analysis for Critical Infrastructure Security Modelling: A Case Study within the Grid'5000 Project

Keywords: Critical infrastructures, dependency analysis, risk monitoring, security modelling

Critical infrastructure (CI) services (like electricity, telecommunication or transport) are constantly consumed by the society and are not expected to fail. A common denition states that CIs are so vital to our society that a disruption would have a severe impact on both the society and the economy. CI security modelling was introduced in previous work to enable on-line risk monitoring in CIs that depend on each other by exchanging on-line risk alerts expressed in terms of a breach of Condentiality, a breach of Integrity and degrading Availability (CIA). One important aspect for the accuracy of the model is the decomposition of CIs into CI security modelling elements (CI services, base measurements and dependencies). To assist in CI decomposition and provide more accurate results a methodology based on dependency analysis was presented in previous work.

In this work a proof-of-concept validation of the CI decomposition methodology is presented. We conduct a case study in the context of the Grid'5000 project, an academic computing grid with clusters distributed at several locations in France and Luxembourg. We show how a CI security model can be established by following the proposed CI decomposition methodology and we provide a discussion of the resulting model as well as experiences during the case study.

Introduction

Critical infrastructures (CIs) are complex interacting systems on a nationwide or even international level that provide services to society and economy. More importantly, those infrastructures are so vital to society and economy that a failure in service delivery or a degradation of quality-of-service would have severe consequences.

CIs face a multitude of risks due to for example technical faults, human error or deliberate attacks. Furthermore, dependencies to services provided by other CIs can cascade risks from one CI to another which makes risk monitoring in CI services even more complex. In recent years, research on CI security modelling tried to evaluate on-line risks (breach of Condentiality, breach of Integrity and degrading Availability -CIA) in complex systems like CIs on the CI service level. The basic idea of CI security modelling is to estimate the current risk of a CI service by observing the system state of the components that are used to provide the service as well as by observing the risk experienced by dependencies. The main components of the model are CI services (services provided to customers or internal services utilized to provide services to customers), base measurements (system measurements dening the state of a service) and dependencies among CI services. For each CI service, risk is derived from the observations using a Bayesian network based approach.

A crucial part for accuracy of risk estimates is a well performed analysis of a CI and its dependencies to be able to represent it as a CI security model. In complex systems like CIs, possibly operated on a national or even international level, this can be problematic. To assist with the decomposition necessary for the CI security model, a methodology based on dependency analysis was proposed in [START_REF] Schaberreiter | Risk assessment in critical infrastructure security modelling based on dependency analysis[END_REF]. The main idea of this approach is to use a socio-technological approach of analysing a complex system, meaning that all possible information sources, reaching from written technical documentation or contracts to interviews with employees on all organizational levels of a CI are utilized to get a holistic view of the complex systems and its complex dependencies. Another important aspect of this methodology is a graphical representation of the ndings to get a visual feedback of the analysis.

In this work we present a proof-of-concept validation of the dependency analysis methodology based on a case study conducted within the framework of the Grid'5000 platform. We show that we can decompose parts of the Grid'5000 platform into CI services, base measurements and dependencies and thus build a CI security model. To simplify our work, we only take availability risk into account. The Grid'5000 project maintains an academic computing grid with clusters distributed at several locations in France and Luxembourg to perform large-scale scientic experiments that require substantial processing power and/or storage. The sites of Grid'5000 are geographically distributed and connected via a dedicated high-speed network connection operated by an independent provider, which makes this case study especially interesting for validation of the CI security model since being able to model dependencies to external providers is a major goal of the CI security model. While Grid'5000 is not a CI in the narrow sense, because it lacks its importance to society and economy, it is similar to CIs of the computing or telecommunication sector in technical as well as organizational realization. Therefore the Grid'5000 project is an ideal candidate for validating research related to CIs having in mind that it is hard to get access to data coming from actual CIs. Furthermore, as a second contribution of this work, we provide an analysis of our case study experiences and we detail positive as well as negative aspects.

The remainder of the paper is organized as follows: Section 2 discusses related work. Section 3 introduces the previously proposed dependency analysis methodology as well as the CI security model. Section 4 presents the dependency analysis case study and Section 5 discusses case study results. Finally, Section 6 concludes the paper and gives an outlook on future work.

Related work

Dependency analysis in CIs is a complex task. In [START_REF] Rinaldi | Identifying, understanding, and analyzing critical infrastructure interdependencies[END_REF] Rinaldi et al. provide an excellent introduction to the problem of CI (inter)dependency and its associated problems. Some authors propose CI models that focus on the interdependencies between CIs (e.g. [START_REF] Panzieri | An approach to model complex interdependent infrastructures[END_REF], [START_REF] Tolone | Critical infrastructure integration modeling and simulation[END_REF]), the main goal of those methods is to integrate CI sector-specic behaviour models with each other, whereas in CI security modelling we try to establish a CI model that uses model parameters (CI services and CIA risk) that are valid for each CI sector and thus allows to establish a crosssector model. The rst step of establishing such a model is to analyse the CIs and their dependencies to achieve an abstract representation of CIs as a modelling basis. In this work we use PROTOS-MATINE method for dependency analysis developed by OUSPG (Oulu University Secure Programming Group). The method was originally developed for identifying protocol dependencies [START_REF] Eronen | A case for protocol dependency[END_REF] and is based on analysis of all available information sources to get a holistic picture of dependencies. The method has proven to be especially useful in combination with the semantic tool Graphingwiki [START_REF] Eronen | Graphingwiki -a semantic wiki extension for visualising and inferring protocol dependency[END_REF] which allows to graphically represent the dependency model and rene the model whenever new information arrives.

The PROTOS-MATINE method has furthermore been used to analyse critical dependencies in the context of antivirus software [START_REF] Eronen | Software vulnerability vs. critical infrastructure -a case study of antivirus software[END_REF] and the socio-technical dependencies of a VoIP infrastructure [START_REF] Pietikäinen | Socio-technical security assessment of a voip system[END_REF]. In [START_REF] Schaberreiter | Risk assessment in critical infrastructure security modelling based on dependency analysis[END_REF] the PROTOS-MATINE method was adapted to be used in the context of the CI security model [START_REF] Aubert | Risk-based methodology for real-time security monitoring of interdependent services in critical infrastructures[END_REF], [START_REF] Aubert | Real-time security monitoring of interdependent services in critical infrastructures. case study of a riskbased approach[END_REF], [START_REF] Schaberreiter | Critical infrastructure security modelling and resci-monitor: A risk based critical infrastructure model[END_REF].

The goal of CI security modelling is to propose a risk-based cross-sector CI model to be used for on-line risk monitoring. The model parameters are CI services, dependencies between CI services and base measurements (observable measures that dene a CI service state). The model output is CI service risk, where risk is seen as a breach of Condentiality, a breach of Integrity or degrading Availability (CIA). In [START_REF] Schaberreiter | A bayesian network based critical infrastructure model[END_REF] a Bayesian network based risk estimation methodology was introduced to the CI security model which provides a more sophisticated way of estimating risk as well as some advanced features like risk prediction. Some advantages of the CI security model compared to other CI models (e.g. [START_REF] Rinaldi | Modeling and simulating critical infrastructures and their interdependencies[END_REF], [START_REF] Sokolowski | A conceptual modeling method for critical infrastructure modeling[END_REF]) or CI risk models [START_REF] Tan | Using hidden markov models to evaluate the real-time risks of network[END_REF], [START_REF] Haslum | Multisensor real-time risk assessment using continuoustime hidden markov models[END_REF] is the exibility of the approach that allows to model CI systems to the desired level of detail, the comparability of dierent CI sectors due to abstraction to common, risk related indicators, and the ability to include dependent service risk in CI risk estimation.

CI dependency analysis

The dependency analysis method presented in [START_REF] Schaberreiter | Risk assessment in critical infrastructure security modelling based on dependency analysis[END_REF] is used to nd the modelling entities of the CI security model, the CI services, base measurements and dependencies. The core idea of the approach is to nd a suitable model by combining information gathered from all available information sources at dierent organizational levels in a CI (preparedness and business continuity level, process level and technical level). The combination of internal (e.g. contracts, policies, expert interviews, manuals) and external (e.g. news, vulnerability feeds, laws/regulations) information sources provides a holistic view on the analysed system. After gathering the information sources, the dependency analysis is carried out in an iterative manner. The rst step is to generate a high level model of the system, nding the high level services and dependencies that dene the system. In the next steps, the model is rened and detailed low level services/dependencies and base measurements are identied. During the process of better understanding the system by adding more detail, it is expected that the high level system model will be rened as well. It is expected that the high level system model will be mainly composed of services and dependencies, since the base measurements (e.g. sensor outputs), are expected to be rather available on the process level/ technical level than on the preparedness and business continuity level.

One important aspect of the proposed CI dependency analysis method is the graphical representation of the CI model. In order to facilitate discussion and expert input, the model has to be presented in a clear and intuitive way so that errors and wrong assumptions in the model are easier to identify. In this work the model is represented as a graph, where the CI services and base measurements represent nodes (CI services are visualized as elliptic shapes and base measurements as rectangle shapes) and the dependencies among services as well as among services and base measurements are represented as edges.

Bayesian network based CI security model

Since the publication of the CI dependency analysis method in [START_REF] Schaberreiter | Risk assessment in critical infrastructure security modelling based on dependency analysis[END_REF], the CI security model was rened by adding a Bayesian network based component for risk estimation in [START_REF] Schaberreiter | A bayesian network based critical infrastructure model[END_REF]. The core concept of CI dependency analysis (identication of services, dependencies and base measurements) does not change compared to the original proposal, but the concept of how service risk is derived from dependent service risk and base measurement observations did change, therefore the integration of the Bayesian network based CI security model with the CI dependency analysis methodology is presented in this Section.

In the original proposal of the CI security model in [START_REF] Aubert | Risk-based methodology for real-time security monitoring of interdependent services in critical infrastructures[END_REF], [START_REF] Aubert | Real-time security monitoring of interdependent services in critical infrastructures. case study of a riskbased approach[END_REF], [START_REF] Schaberreiter | Critical infrastructure security modelling and resci-monitor: A risk based critical infrastructure model[END_REF], the service risk is calculated using a weighted sum method for which each dependency of a service (another CI service or a base measurement) is weighted by an expert based on the assumed importance to the service. In the Bayesian network based CI security model, service risk is estimated based on the state of dependencies, which is represented by the conditional probability table (CPT) of a node. For Fig. 1: Network backbone interconnection between the sites of the Grid'5000 platform.

each state combination of the dependencies of a service, the most probable service risk is estimated. Those probabilities can be learned from data records as well as estimated by experts where learning is not possible.

During the CI dependency analysis process, the Bayesian network based security model requires identication of following parameters: Normalization values for base measurements based on classication of normal operation/ allowed deviation from normal operation. To avoid state explosion, the CI security model requires that all base measurements are normalized to 5 discrete values, where 1 characterizes a base measurement value during normal operation and 5 the maximum allowed deviation. The classication of the boundaries is assumed to be done using technical specications and expert estimation. For each service, the service risk has to be estimated for incidents that happened during the time period that is used to learn the risk probabilities from data. This is necessary since service risk is an abstract concept that can not be directly measured. Estimating service risk for past incidents will allow to learn the most probable service risk for each dependency state combination. In situations where service risk probabilities can not be learned from data due to missing data records or insucient data, expert estimation is required to estimate the service risk probabilities for each missing dependency state combination.

In this case study we will, besides identifying the CI services, base measurements and dependencies, also describe the normalization process for each identied base measurement. [START_REF] Tolone | Critical infrastructure integration modeling and simulation[END_REF] Grid'5000 case study

In this Section, the CI dependency analysis methodology is validated using the Grid'5000 platform 4 which provides the users with a fully customizable testbed to perform advanced experiments in all areas of computer science related to parallel, large-scale or distributed computing and networking. Grid'5000 is a distributed computing platform featuring clusters located in nine geographical sites eight in France (Bordeaux, Grenoble, Lille, Lyon, Nancy, Reims, Rennes, Sophia, Toulouse) and one in Luxembourg. The interconnect backbone between all sites is illustrated in Figure 1. In addition, international connections to Brazil, Japan and the Netherlands operated via the site of Grenoble are available. The resulting CI security model of the highest decomposition level of Grid'5000 can be seen in Figure 2. The infrastructure is divided into two providers, the Grid'5000 provider and the Network provider, since those infrastructures are operated by separate companies and therefore the organizational structure and day-to-day operation of the infrastructures dier greatly from each other.

Each site of Grid'5000 is represented as as service 5 that will aggregate service risk from the lower-level model described in the following Sections. The Grid'5000 provider depends on all sites which allows to produce a global risk estimate for Grid'5000, taking the risk of the individual sites into account.

The network provider is modelled by dening each network link between two sites as a service. The risk estimate of each link aggregated from lower-level model of the network provider can be used at this decomposition level to estimate a risk for each network segment as well as a global risk estimate for the Network provider. Therefore, each service characterizing a network segment is modelled as a dependency of the Network provider. This representation was used since it follows the geographical structure of the network and it provides a good basis to model the lower decomposition levels as shown in the following Sections.

The dependencies between the network provider and the Grid'5000 provider were modelled in a way that each site physically connected to a network segment, depends on this network segment. In this way a changed risk in a network segment can be easily included in the risk estimation of the site that depends on this segment.

The main information sources to gather the information used at this decomposition level are the internal Grid'5000 documentation containing information about the high-level structure of Grid'5000, like the network backbone shown in Figure 1 and expert knowledge about Grid'5000 to account for the most recent changes in the the structure of Grid'5000. Every network segment of the backbone presented in the Figure 1 is characterized by connection points within the dark bre infrastructure provided by Renater 6 which allocates dedicated 10Gbit/s "lambdas" on a DWDM (Dense Wavelength Division Multiplexing) infrastructure for the Grid'5000 platform. Grid'5000 sites see each other inside the same VLAN at 10Gbps. A few bottleneck still exists, like the Lyon to Paris link, where the 10Gbps are shared between all the sites above Lyon and all the sites under Lyon.

Each network segment can be observed by incident monitoring as well as network performance measures, both of them performed by the backbone provider (Renater in France and Restena in Luxembourg). The incident monitoring takes the form of tickets which can be accessed by Grid'5000 administrators in realtime and are one of the following: incident : a sudden IP service disruption occurs on the network. maintenance : an operation will be performed on a network equipment that will (or not) interrupt the IP service.

Regarding backbone performance, Grid'5000 oers 3 dierent types of monitoring information: The link status (up or down), the packet count (reported by the SNMP counters of Renater/Restena switches) and the packet loss (PL) occurring on the link. Packet Loss can be caused by the saturation of a link. When router or switch buers are unable to store packets, the packets are dropped. It may also be caused by a faulty equipment or a apping link (link up/down/up/down...).

4.3

The network backbone CI security model

The resulting CI security model for the network link Luxembourg-Nancy is presented in Figure 3. To account for space constraints in a publication, only the detailed decomposition of one network segment is presented in this work, but it should be noted here that the decomposition of all network segments follows a similar structure. The network connection between the sites Luxembourg and Nancy is characterized by the three main connection points in Luxembourg, Esch-sur-Alzette and Nancy. In Figure 3 those are represented as services that are characterized by the measurements collected at the level of the routers at those locations (performance measures) and Restena tickets.

Normalization of base measurements according to the CI security model for Restena tickets is done following the information presented in Table 1. No ticket means normal operation or normalization level 1. A maintenance ticket is characterized as normalization level 3, since it will not interrupt the service, but a degradation in service can occur. An incident ticket is characterized as normalization level 5, since it implies an interruption of service.

From the performance measures presented in the previous Section, only link status and packet loss are taken into account, since they fully characterize the service availability status. Link status, as specied in Table 2a can be see as a binary base measurement where link up represents the normalized level 1 and link down represents level 5. The Packet loss measurement is normalized according to the boundaries presented in Table 2b, with rather restrictive bounds to reach level 1 or level 5.

The main information sources at this level of decomposition were Grid'5000 as well as Restena network documentation (as far as available to the Grid'5000 project), manuals and documentation of the used monitoring tools (Passilo) and expert knowledge, especially to dene the base measurement normalization bounds. Each site of Grid'5000 holds one or several computing clusters. The hardware conguration of each site is depicted in Figure 4a and is typically organized in the following way:

An access server which serves as an isolated user frontend to access the resources of the site; one or several adminfront server(s) holding a set of virtual machines dedicated to platform services. the computing nodes, split among one or more clusters (depending on the site capacity). an NFS server (together with its associated disk enclosure) that act as a centralized and shared storage area for the site. the site router which interconnects all site components and enables communication to other sites of Grid'5000. a local interconnect switch, which provides an isolated network for the site internal components.

Apart from the general structure, Grid'5000 consists of several elements crucial for operation, especially in the context of availability: The Puppet infrastructure 7 (responsible for the conguration and the deployment of all grid services within Grid'5000), the Platform Monitoring infrastructure (a set of monitoring tools such as Nagios 8 or Ganglia [START_REF] Massie | The Ganglia Distributed Monitoring System: Design, Implementation, and Experience[END_REF]), OAR [START_REF] Capit | A batch scheduler with high level components[END_REF] (the resource manager of Grid'5000) and Kadeploy 9 (piloting the deployment of the computing nodes) as well as the technical committee (engineers responsible for the maintenance and the development of the platform) and the users of Grid'5000. The Puppet infrastructure Puppet is an IT automation software based on a master/slave approach that helps system administrators to manage their infrastructure throughout its life cycle, from provisioning and conguration to patch management and compliance. Using Puppet, it is easy to automate repetitive tasks, quickly deploy critical applications, and pro-actively manage change in a scalable way. Puppet uses a declarative, model-based approach to IT automation.

In particular, the desired state of the infrastructure's conguration is dened using Puppet's declarative conguration language. After a Puppet conguration is deployed, a Puppet agent is run on each node to automatically enforce the desired node state, correcting any conguration drift. As illustrated in Figure 4b, the Puppet agent of a node sends Facts, or data about its state, to the Puppet Master which compiles a Catalog, or detailed data about how the node should be congured, and sends this back to the Puppet agent. After making any changes to return to the desired state, the Puppet agent sends a complete Report back to the Puppet Master. In this work we propose to use the Puppet agent exit codes to classify the status of a given service. The exit codes are reported every time the Puppet agent is executed, which is every 30 minutes by default.

The Platform Monitoring infrastructure Many monitoring tools are used to reect the status of the platform. The main one is Nagios which evaluates at the moment of writing 160 hosts and more than 629 service status. The dierent services currently monitored by Nagios plugins are summarized in Table 3. Table 3: Nagios services monitored on Grid'5000.

Each service is checked by the Nagios daemon, either at regular intervals or On-demand as needed for predictive service dependency checks (such checks help to ensure that the dependency logic is as accurate as possible.) Services that are checked can be in one of four dierent states (OK, WARNING, UNKNOWN or CRITICAL).

The OAR and Kadeploy infrastructure OAR is a versatile resource and task manager (also called a batch scheduler) for clusters and other computing infrastructures which is used in particular on Grid'5000 and provides a simple and exible exploitation of a cluster. Its design is based on high level tools, more precisely a relational database engine (MySQL or PostgreSQL), a scripting language (Perl), a connement system mechanism based on a feature proposed by recent (2.6) Linux kernels called cpuset and a scalable administrative tool (component of the Taktuk framework). It is composed of modules which interact only with the database and are executed as independent programs. Whereas the OAR service is managed by Puppet on Grid'5000, it integrates a set of internal checks of the computing nodes it pilots such that from the node status reported by OAR, it is possible to get information on the current status of the node.

For node deployment OAR is coupled with the Kadeploy middleware. Kadeploy belongs to the category of disk imaging and cloning tools and is used to install and customize servers. Users are able to deploy a new environment and customize computing nodes during their reservations. In parallel, other tools have been designed internally to qualify the good status of the computing nodes and detect altered environments. Among them, phoenix analyses the production environment deployed after user reservation and restarts the full deployment process up to 3 times if errors are detected (bad disk formatting, unhealthy system etc.), which can be used as measurement to determine the status of computing nodes.

4.5

Grid'5000 site infrastructure CI security model

For each site of Grid'5000 we identied 4 main factors that contribute to the availability risk of the site:

Cluster: The hardware and software components that form a computing cluster. Network connection: The network interconnection between computing sites, as detailed in Section 4.2. Environmental factors: The supporting infrastructure needed to operate the computing cluster. Human factor: This describes how humans can inuence the availability of the infrastructure. In Grid'5000, two types of human interaction was identied, by the sta operating and maintaining the grid and the users that can inuence availability since they are granted substantial user rights to operate the grid.

Cluster

The main information sources at this decomposition level were structural as well as organizational documentation of Grid'5000 as well as interviews with Grid'5000 administrators.

Each site of Grid'5000 follows the same basic structure, but further decomposition reveals dierences in implementation details, for example dierent hardware components that allow dierent levels of monitoring as well as dierences in the number of employed sta. In this work we illustrate the decomposition of the site Luxembourg and while the basic structure of the CI security model remains the same for each site, the outcome of the model depends on the actual implementation of the site.

The resulting CI security model for site Luxembourg can be seen in Figure 5. In the rst level of decomposition, the node Server Room represents the environmental factors of the site, the Site sta and the Site Users represent the human factor, the Network Luxembourg-Nancy represents the network connection and the Cluster represents the actual computing cluster.

The main part of the site Luxembourg is the Cluster which can be further de-composed into the 5 major components (as illustrated in Figure 4a), the Interconnect (local interconnect to other institutions within site) and the Fast Interconnect (interconnect for site internal components), the Computing Nodes, the Shared Storage and the Service Nodes (a summation of supporting services like OAR, Puppet, Kadeploy, supervision or site access server, as listed in Figure 4a). The service state of the Interconnect and Fast Interconnect can be described by the the state of services they are composed of, monitored by nagios plugins N18 and N20 (Interconnect) and N18 (Fast Interconnect). The Shared Storage state can be characterized by the output of the puppet conguration status for shared storage and the state of the services monitored by nagios plugins N1-N5 and N11-N20. The state of the computing nodes can be described by the output of Kadeploy phoenix status, the node status as monitored by OAR 10 and the state of the services monitored by nagios plugins N1-N7, N9 and N11-N20. The Service Nodes state can be characterized by the puppet conguration status for each service node 11 as well as the status of the services monitored by the nagios plugins N1-N20.

The base measurement normalization for the output of the nagios plugins (N1-N20) is listed in Table 4a. The nagios plugins report 4 dierent states for the services they monitor which can be translated to normalization levels. Since only 4 states are available, normalization level 4 was omitted.

Puppet conguration, reports exit codes which are translated into normalization levels as illustrated in Table 4b. The node status reported by OAR is translated into normalization levels according to Table 5a and Kadeploy phoenix node status is normalized according to Table 6a.

The main information sources to obtain the structure of the Cluster were structural documentation of Grid'5000 clusters, the technical documentations as well as log output of the platform monitoring tools to determine base measure-10 Each available computing node has a seperate Kadeploy phoenox as well as OAR status base measurement. To maintain readability of Figure 5, those base measurements are summarized by Kadeploy phoenix status and OAR status.

11 A puppet status base measurement for each monitored service is available. To main- tain readability of Figure 5, only a single base measurement, Puppet status Service Nodes was introduced. ments and base measurement normalization and expert interviews to verify the information.

The second important aspect of each site are the environmental factors. The basic idea of this decomposition is to capture data from the environment the site is located in to be able to monitor not only the Cluster itself, but also be able to react to a changing environment that can inuence the operation of the cluster (like for example res or power shortage). At the site Luxembourg the main place to capture environmental factors is the Server Room the cluster is located in. We identied three main elements which would be Cooling of computing equipment, the Fire Extinction System and the Electricity Supply. The Electricity Supply of the Site Luxembourg is composed of the main public electricity supply as well as backup energy supply by a Diesel generator. The state of the electricity supply can on the one hand be determined by the output of Struxureware software 12 , a tool that monitors several sensors and aggregates a risk level which is presented to the operator. On the other hand, additional information about the availability status of the public electricity provider as well as a backup diesel generator can be given by monitoring notications about planned interruptions of public electricity supply as well as the diesel generator fuel level. The base measurement normalization of the Stuxureware risk levels can be found in Table 5b. The provided risk levels of low, medium and high are mapped to the normalization values 1, 3 and 5 respectively. The base measurement normalization for the planned public electricity supply can is presented in Table 6b. The normalization bounds result from the analysis of the electricity supply: For up to 5 minutes, batteries guarantee operation of the cluster and the backup diesel generator should provide backup electricity supply for up to 30 minutes. The base measurement normalization for the diesel generator fuel level can be seen in Table 7a. Unfortunately, the generator does not report ne grained fuel level status, but only full or not full. The cooling system status can be determined by Stuxureware alerts. The base measurement normalization is identical to the electricity supply status and can be seen in Table 5b. The re extinction system status can be determined by the smoke detector status, each smoke detector can have three dierent states: no alert, defect or alert. The base measurement normalization for the smoke detector status can be found in Table 7b.

The main information sources regarding identication of environmental factors were interviews with personal working in the server room as well as technical documentation of the server rack and the re extinction system.

The human factor in a complex system is generally hard to quantify. In this case study, there are two separate groups that can inuence the availability of the site Luxembourg: The Site Sta and the Site Users. We have identied that the main factor concerning availability in the Site Luxembourg caused by Site Sta is absence due to vacation or sick leave. Collecting and monitoring the availability of each sta member within Grid'5000 is performed via a time tracking system (TTS). Another interesting tool that help to monitor the sta presence is the Grid'5000 Jabber service (a messaging service similar to MSN or Skype). Monitoring the Jabber online status can add additional information about availability of site sta since in the computing sector personal can be available and resolve possible problems without physical presence.

The base measurement normalization of the Jabber and TTS status can be found in Tables 7c and8a. Each member of the site sta will have a base measurement for Jabber status and Time Tracking System (TTS) status , even though in Figure 5 only one of each base measurements is introduced for the sake of readability. The inuence of Site Users to the availability of site Luxembourg is hard to determine. On the one hand, due to the infrastructure-as-a-service approach of Grid'5000, site users have quite substantial rights to interact with Grid'5000 infrastructure. On the other hand, due to the academic nature of Grid'5000 there are not many tools in place to monitor user actions. One factor we could identify is User charter compliance measured by a script designed to check on a regular basis the compliance of the user behaviour with the user charter. The user charter compliance measurement normalization can be found in Table 8b. User charter compliance is measured for each user, but for readability reasons only one base measurement User Charter Compliance was introduced in Figure 5. In this Section we would like to discuss the observations made during the case study in more detail. We want to highlight which parts of the case study provided the expected results according to the proposed dependency analysis methodology, but we also want to highlight some problems and unexpected obstacles we experienced during the case study. At the end we want to summarize our ndings and draw a conclusion regarding the feasibility of the proposed methodology. On the positive side, by conducting this case study we have shown that it is possible to represent a complex system like Grid'5000 using the abstract elements of the CI security model (CI services, base measurements and dependencies) by following the steps of the presented dependency analysis methodology. We have successfully established a model that includes the socio-technical structure of Grid'5000 and takes technical as well as human and environmental components into account allowing us to provide a holistic view on the availability risk of CI services at dierent organizational levels. We have also shown that hierarchical decomposition in this context is possible by decomposing higher level services into sub-components and treating them as services they provide to higher level services. We have shown that we can identify base measurements within the CI systems to be able to observe the system state. And nally, we could show that we could identify enough information sources within Grid'5000 (e.g. documentation or expert interviews) or from external sources (e.g. manuals) to establish the CI security model. It was experienced that expert interviews are a very valuable source of information, especially on the higher levels of decomposition. The lower, more technical levels are usually well described by documentation/manuals. In any case it was experienced that, as expected, the graphical representation of the CI security model is a very useful tool to discuss the model structure and nd aws in the representation.

Aside from the positive aspects, some observations were made during the course of the case study that could have a negative implication on the outcome of future case studies. One major observation was that not all information can be made available due to condentiality or privacy reasons. This was even experienced in this case study (e.g. employee records due to privacy concerns) in an academic environment which is usually more open than a commercial operator.

If the CI security model should be applied in a more competitive commercial environment, restricted access to information due to condentiality reasons could pose a problem. Even though risk alerts are abstract metrics and should help to maintain source condentiality, providers might be reluctant to provide the necessary structural information (CI services and dependencies) to business partners and possibly competitors.

Another observation made during the case study was that information gathering was generally more dicult and time consuming than expected. One problem contributing to this observation were for example the organizational structure of some of the sites. For example, the server room in one site was the responsibility of the universities maintenance department and the administration of the cluster is done by research personnel. Information requests regarding server room equipment and actual hardware caused substantial delays because those requests were treated with dierent urgency by the maintenance department for mainly two reasons: a) The employees were already overworked with other, more important tasks and b) since the maintenance department and research personnel of the university are organized in dierent branches of the organizational hierarchy, there is no direct authority which would give requests for information more urgency. Although this scenario was specic to this case study, similar challenges are expected to be experienced in other big companies or complex infrastructures.

The last observation that was made during the case study was that base measurements, although available and observable, are not always recorded. Before the case study it was assumed that sensor data is recorded for a certain time period. In the CI security model, recorded sensor data can be used to learn risk probabilities from events that happened in the past, but without data records learning is not possible. In this case, risk probabilities need to be estimated by experts which makes the estimates more inaccurate and error prone.

To conclude this Section, we want to state that this case study has shown that it is possible to represent complex infrastructures as CI security model, but it requires some eort and dedication by the operators to achieve the goal. We also recognize that every complex infrastructure is dierent and that one case study can not proof or disproof the validity of our approach, but we could make some general positive as well as negative observations that can serve as a basis for future discussions and case studies. In this work we presented a case study to provide a proof-of-concept validation of a CI dependency analysis methodology in the context of CI security modelling. CI security modelling provides a framework for on-line risk monitoring of CI services, taking into account the service state as well as the risk state of dependencies. A crucial part for the success of the model is a well performed CI analysis to identify the elements forming the CI security model, which are CI services (services provided to customers or internal services utilized to provide the service to the customer), base measurements (measurements to determine the state of a CI services) and dependencies between those elements. The presented case study was performed in the context of Grid'5000, a distributed academic computing grid operated by several universities in France and other countries like Luxembourg. The sites of the grid are connected by a dedicated high-speed bre optic network connection. As a result of the case study, we have shown that, following the proposed dependency analysis methodology, it is possible to analyse a complex infrastructure and represent it as a CI security model. We have also seen that it is not trivial to gather the necessary information due to for example organizational reasons. Though it is not possible to provide a nal verdict on the general feasibility of the methodology since every CI is dierent, the results suggest that the methodology will also work in other CI environments.

In future work, Bayesian network based risk estimation within the Grid'5000 CI security model as well as risk simulation based on attack or failure scenarios will be conducted. For this purpose a tool is currently implemented that allows risk estimation as well as risk simulation/emulation in the context of the CI security model. Given the opportunity, we also plan to conduct further case studies to validate the dependency analysis methodology as well as the CI security model in a broader context.

Fig. 2 :

 2 Fig. 2: Grid'5000 high level CI security model for availability risk indicator

  Fig. 3: CI security model for availability risk indicator of network segment Luxembourg-Nancy

Fig. 4 :

 4 Fig. 4: (a): General overview of the hardware organization of each site. (b): General Puppet Workow.

Fig. 5 :

 5 Fig. 5: Site Luxembourg CI security model for availability risk indicator.

Table 4 :

 4 (a): Base measurement normalization for Nagios service checks. (b): Base measurement normalization for Puppet-managed services.

6

  Conclusion and future work

Table 1 :

 1 Base measurement normalization for Renater/Restina tickets

			Level	Description
	Level Description	1	Normal: P L = 0%
	1 5	Link up Link down	2 3 4	Degraded: 0 < P L ≤ 33% Really Degraded: 33% < P L ≤ 66% Hightly Degraded: 66% < P L ≤ 99%
		(a)	5	P L > 99%
				(b)

Table 2 :

 2 (a): Base measurement normalization for link status. (b): Base measurement normalization for packet loss.

	4.4	Grid'5000 Site Infrastructure

Table 5 :

 5 (a): Base measurement normalization for OAR based node status checks. (b): Base measurement normalization for Struxureware monitored services.

	Level	Description	Level	Description
	1	Node deployed without error	1	No interruption
	2	Node is re-deployed after error	2	0-5 Minutes
	3	Node is re-deployed a second time after error	3	6-15 Minutes
	4	Node is re-deployed a third time after error	4	16-30 Minutes
	5	Node is down	5	30 Minutes and more
		(a)		(b)

Table 6 :

 6 (a): Base measurement normalization for Kadeploy phoenix status. (b): Base measurement normalization for planned electricity supply interruption.

Table 7

 7

	: (a): Base measurement normalization for diesel generator fuel level. (b):
	Base measurement normalization for smoke detector status. (c): Base measure-
	ment normalization for Jabber status.

Table 8 :

 8

(a): Base measurement normalization for Time Tracking System status. (b): Base measurement normalization for user charter compliance.

5

Results and Discussion

http://www.grid5000.fr

The Sites represented by dotted lines in Figure2are part of the Grid'5000 project, but currently oine.

http://www.renater.fr/

http://puppetlabs.com/

http://www.nagios.org/

http://kadeploy.gforge.inria.fr/

http://www.apc.com/.

Acknowledgements

One of the authors would like to thank the Luxembourgish National Research Fund (FNR) for funding his PhD work under AFR grant number PHD-09-103.


Atif Mashkoor

Osman Hasan

Wolfgang Beer

Using Probabilistic Analysis for the Certification of Machine Control Systems

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Software-controlled systems have become ubiquitous in day to day affairs. The proliferation of software has spanned from transportation to industrial informatics and from power generation to homeland defence. While our domestic as well as defence activities increasingly depend on software-intensive systems, the safety-critical, distributed, heterogeneous, dynamic and often unpredictable nature of such systems produces several complex challenges.

The grand challenge of such systems is that their incorrect use or unsafe development may lead to a compromise on homeland defence and security. We often read such news related to cyber threats, unmanned aerial system crashes, and vulnerability of power generation and chemical plants against terrorist attacks.

One of the integral systems responsible for homeland defence and security is a Machine Control System (MCS). MCS is a device that manages, commands, directs or regulates the behaviour of various processing units. As shown by Figure 1, a typical MCS is composed of some realtime Programmable Logic Controllers (PLCs) and a non-realtime User Interface (UI) that helps interacting with PLCs. PLCs, in turn, are of two types. First type contains some domain-specific commands pertaining to the processing unit that control motors based on signals from sensors and actuators. The other type is comprised of stringent safety regulations that need to be certified before being functional. Besides threatening the homeland defence and security, a faulty MCS can also result into a minor injury, irreversible severe injury, amputation or even death. Although, we do not have detailed publicly available investigation reports of accidents caused by disturbances in MCS performing safety functions, yet some information is presented in [START_REF] Dźwiarek | An analysis of accidents caused by improper functioning of machine control systems[END_REF]. The report is based on an analysis of 700 industrial incidents occurred between 1996-2002 in Poland alone. According to the report, 41% of severe accidents were caused by improper functioning of the system. Software faults were among the notable reasons.

Industrial incidents are not new phenomena. Standard techniques to avoid accidents [START_REF] Heinrich | Industrial Accident Prevention: A Scientific Approach[END_REF] are in place since last several decades. However, with the proliferation of software, industry saw a paradigm shift when mechanical controls were replaced by their software counterparts and along new technology came new challenges. As software started becoming pervasive, it also became unprecedentedly complex.

Due to the critical nature of software components of MCS, there are numerous properties in which they must exceed other software systems, such as resilience, safety, security, and reliability. Such systems must also be certified. Certification, as defined by the charter of Software Certification Consortium (SCC) 3 , demonstrates the assurance that the system has met its relevant technical standards and specifications, and it can be trusted to provide its services safely, securely and effectively.

There are several approaches towards software certification, e.g., argumentbased, process-based and product-based. However, in the past few years, argumentbased safety case approach [START_REF] Bishop | A methodology for safety case development[END_REF] is gaining popularity among regularity regimes for the certification of software-intensive systems. It is also the explicit part of U.K. MoD Defence Standard 00-56. A safety case, in fact, is an evidence based on a convincing and valid argument that the designed system is adequately safe for a given application in the given environment.

Formal methods are usually the part of most of the software certification techniques. Their use is often recommended for the development of safety-critical systems involving higher Safety Integrity Level (SIL), IEC 61508, and DO-178C standards. Formal methods help specifying system requirements and properties using mathematical and logical notations which are then amenable to correctness. Correctness amounts to both verification, the practice where it is determined that product is being built correctly and meets its specification, and validation, the practice where it is ensured that the product meets customers requirements.

Standard verification and validation techniques are comprised of activities like standard theorem proving, model checking, animation and simulation. Each of these techniques has some inherent limitations and do not cope very well with the posed challenges in the development of highly complex and safety-critical MCS.

A standard method to guarantee the safety properties in a formal specification is to show that the invariant, a logical representation of safety, is preserved. We prove a theorem to satisfy the property. While adequate in most of the cases, less so to justify the absence of component failures and emergence of potential hazardous situations. In contrast to safety and deadlock-freedom, fairness and liveness proofs are not so straightforward. The techniques like animation, simulation, model checking can provide help in such cases but only up to some extent.

The problem with the animation is that currently available animators have strong limitations on the types of specifications they can animate. We have seen how the class of executable specifications can be extended with the help of few safe transformations [START_REF] Mashkoor | Stepwise validation of formal specifications[END_REF]. Yet, there are some formal texts on which animators fail [START_REF] Yang | Scaling up with Event-B: a case study[END_REF]. For those texts, we propose to use simulation rather than animation; the specification is translated into a program. But the problem with the translation is that currently available translators are in infancy stages and have their own weaknesses, such as expressiveness of the targeted languages. Approximation using closest counterparts does not fulfil the true purpose.

Model checking involves the construction of a precise state-based mathematical model of the given system. The state-space model is then subjected to exhaustive analysis to automatically verify that it satisfies a set of formally represented properties. The problem of this approach is that it can only be used to analyse systems that can be expressed as finite state machines. Another major limitation is the state-space explosion. The state-space of a real-world MCS can be very large, or sometimes even infinite and thus impossible to be explored completely within the limited resources of time and memory.

Higher-order theorem proving, on the other hand, is very flexible in terms of tackling a variety of systems, thanks to its expressiveness. However, this flexibility comes at the cost of enormous user efforts in terms of manual development of system models and interactive verification due to the undecidable nature of the underlying logic. Thus, developing realistic models of MCS, which usually involve significant amount of continuous and non-deterministic elements, and verifying them for all possible scenarios could be very tedious, if not impossible.

Probabilistic analysis overcomes the above mentioned limitations. Rather than ensuring absolute correctness, the main idea here is to ensure that the system behaves in the desired manner with an acceptable probability. This not only simplifies system modelling but also eases the verification task considerably. Probabilistic analysis is often used as an evidence to justify the claim of safety and reliability [START_REF] Bishop | A methodology for safety case development[END_REF].

The main aim of this paper is to demonstrate how probabilistic analysis approach can provide a subjective evidence that can support the claim of system safety and reliability. Rest of the paper is organized as following: An overview of the existing formal analysis approaches is given in Section 2. Section 3 introduces the main concepts used in this paper, i.e., safety cases and higher-order logic theorem proving. Section 4 describes how probabilistic algorithms can be formalized. Section 5 presents the proposed formal probabilistic analysis approach. Section 6 applies the proposed approach to a simple case-study of multi-robot systems. The paper is finally concluded in Section 7.

Related Work

In recent years, the use of argument-based safety case approach has emerged as a popular technique for the certification of software-controlled critical systems. In [START_REF] Panesar-Walawege | Characterizing the chain of evidence for software safety cases: A conceptual model based on the IEC 61508 standard[END_REF], authors developed a conceptual model, based on the IEC 61508 standard, to characterize the chain of safety evidence that underlies safety arguments about software. In [START_REF] Fong | Structured assurance case methodology for assessing software trustworthiness[END_REF] and [START_REF] Graydon | Assurance-based development of critical systems[END_REF], authors present approaches that extend the border of safety case analysis towards general software properties. These approaches, though rigorous, are not fully formal.

In [START_REF] Rushby | A safety-case approach for certifying adaptive systems[END_REF], an approach is presented to show how a safety case analysis based on SMT sovlers and infinite bounded model checkers can be used as a certification argument for the adaptive systems. The work is then extended in [START_REF] Rushby | Formalism in safety cases[END_REF] with the proposition of a framework based on probabilistic analysis. The mathematics presented in [START_REF] Rushby | Formalism in safety cases[END_REF] is then formalized by probabilistic kernels-based mathematical approach in [START_REF] Herencia-Zapana | Formalizing probabilistic safety claims[END_REF]. The approach is illustrated using an example of a conflict detection system for an aircraft. Our proposed approach, as compared to these aforementioned works, is much more powerful in terms of handling a larger set of problems, for instance MCS. Moreover, unlike our approach, the mathematical framework of [START_REF] Herencia-Zapana | Formalizing probabilistic safety claims[END_REF] has yet to be formalized in a theorem prover.

Probabilistic model checking [START_REF] Baier | Model Checking Algorithms for Continuous time Markov Chains[END_REF][START_REF] Rutten | Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems[END_REF] is the most widely used formal method for probabilistic analysis of systems that can be modelled as Markov chains. Like traditional model checking, it involves the construction of a precise state-based mathematical model of the given probabilistic system, which is then subjected to exhaustive analysis to verify if it satisfies a set of formally represented probabilistic properties. Some notable probabilistic model checkers include PRISM [START_REF] Kwiatkowska | Prism: Probabilistic symbolic model checker[END_REF], Ymer [START_REF] Younes | Ymer: A statistical model checker[END_REF] and VESTA [START_REF] Sen | Vesta: A statistical model-checker and analyzer for probabilistic systems[END_REF].

Besides the accuracy of the results, the most promising feature of probabilistic model checking is the ability to perform the analysis automatically. But it is only limited to systems that can be expressed as Markov chains. Another major limitation of the probabilistic model checking approach is the state-space explosion. The state-space of a probabilistic system can be very large, or sometimes even infinite. Thus, at the outset, it is impossible to explore the entire state-space with limited resources of time and memory. Thus, the probabilistic model checking approach, even though capable of providing exact solutions, is quite limited in terms of handling a variety of probabilistic analysis problems.

Similarly, some algorithms implemented in model checking tools are based on numerical methods. For example, a well-known iterative method, the power method, is often applied to compute the steady-state probabilities (or limiting probabilities) of the Markov chain in PRISM . For this reason, most of the stationary properties analysed in model checkers are time bounded. Moreover, probabilistic model checking tools often utilize unverified algorithms and optimization techniques. Finally, probabilistic model checking cannot be used to verify generic mathematical expressions corresponding to probabilistic and statistical properties. Thus, the verified properties involve values that are expressed in a computer based notation, such as fixed or floating point numbers, which also introduces some degree of approximation in the results.

The B [START_REF]The B Book[END_REF] and Event-B [START_REF]Modelling in Event-B: System and Software Engineering[END_REF] methods have also been extended to support probabilistic analysis. The main idea here is either to use a probabilistic choice operator to reason about termination conditions [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF] or to use the semantics of a Markov process to reason about the reliability or performance characteristics of the given system [START_REF] Tarasyuk | Towards probabilistic modelling in Event-B[END_REF]. But these extensions of the B-method cannot be used to reason about generic mathematical expressions for probabilistic or statistical properties. Similarly, such formalisms are not mature enough yet to model and reason about all different kinds of continuous probability distributions. Due to the continuous nature of the MCS, both the probabilistic model checking and Event-B based techniques cannot be used to capture their true behaviour and thus, to the best of our knowledge, the use of probabilistic and quantitative assessment for the formal verification of MCS is almost non-existent.

The aforementioned limitations can be overcome by using higher-order logic theorem proving for conducting the formal probabilistic analysis. We can capture the true continuous and randomized behaviour of the given system in higherorder logic by leveraging upon its expressiveness. Moreover, generic mathematical expressions corresponding to the probabilistic and statistical properties of interest can be formally verified within the sound core of a theorem prover. Due to the formal nature of the models and properties and the inherent soundness of the theorem proving approach, probabilistic analysis carried out in this way will be free from any approximation and precision issues. The foremost criteria for conducting the formal probabilistic analysis of MCS in a theorem prover is the availability of a formalized probability theory, which will in turn allow us to express probabilistic notions in higher-order logic, and formal reasoning support for the probability distribution and statistical properties of random variables in a theorem prover.

Various higher-order-logic formalizations of probability theory can be found in the literature, e.g., [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF][START_REF] Mhamdi | Formalization of Entropy Measures in HOL[END_REF][START_REF] Holzl | Three Chapters of Measure Theory in Isabelle/HOL[END_REF]. The formalizations by Mhamdi [START_REF] Mhamdi | Formalization of Entropy Measures in HOL[END_REF] and Hölzl [START_REF] Holzl | Three Chapters of Measure Theory in Isabelle/HOL[END_REF] are based on extended real numbers (including ±∞) and also include the formalization of Lebesgue integral for reasoning about statistical properties. This way, they are more mature than Hurd's [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF] formalization of measure and probability theories, which is based on simple real numbers and offers a limited support for reasoning about statistical properties [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF].

However, the former formalizations do not support a particular probability space like the one presented in Hurd's work. Due to this distinguishing feature, Hurd's formalization [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF] has been utilized to verify sampling algorithms of a number of commonly used discrete and continuous random variables based on their probabilistic and statistical properties [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. Since formalized random variables and their formally verified properties play a vital role in the probabilistic analysis of MCS systems, as illustrated later in this paper, we propose to utilize Hurd's formalization of measure and probability theories. Hurd's theories are already available in the HOL4 theorem prover therefore the current work make an extensive use of them.

Background

A brief introduction to safety cases and high-order logic theorem proving using the HOL4 theorem prover is provided in this section to facilitate the understanding of the paper.

Safety case

A safety case, as described by [START_REF] Bishop | A methodology for safety case development[END_REF], is an evidence that provides a convincing and valid argument about the safety of a system in a given domain. The main elements of a safety case are the claim about a property, its evidence, and its argument.

A claim is usually about a system meeting certain properties, such as reliability, availability, safety and accuracy. An evidence provides the basis of a safety argument. This can be either facts, assumptions, or even sub-claims. Arguments link an evidence to claims. An argument can either be deterministic, probabilistic, or qualitative. The choice of the argument will depend upon the available evidence and the type of claim. System reliability claims are often justified in terms of probability of failure of its components. Arguments can be based on the design of a system, its development process, or simulated and prior field experiences.

HOL4 theorem prover

HOL4 is an interactive theorem prover that allows conducting proofs in higherorder logic, which is implemented by using the simple type theory of Church [START_REF] Church | A Formulation of the Simple Theory of Types[END_REF] along with Hindley-Milner polymorphism [START_REF] Milner | A Theory of Type Polymorphism in Programming[END_REF]. The logic in HOL4 is represented by Meta Language (ML), which is a strongly-typed functional programming language. The core of HOL4 consists of only 5 axioms and 8 inference rules. Building upon these foundations, HOL4 has been successfully used to formalize many classical mathematical theories and verify a wide variety of software and hardware systems.

HOL4 allows four kinds of terms, i.e., constants, variables, function applications, and lambda-expressions. It also supports polymorphism, i.e., types containing type variables, which is a distinguishing feature of higher-order logic. Semantically, types are denoted by sets and terms are denoted by memberships of these sets. Formulas, sequents, axioms, and theorems are represented by terms of Boolean types.

The formal definitions and theorems can be stored as a HOL4 theory file in computers. These theories can then be reused by loading them in a HOL4 session. This kind of reusability feature is very helpful in reducing the human interaction as we do not have to go through the tedious process of regenerating already available proofs using the basic axioms and primitive inference rules. Various classical mathematical results have been formalized and saved as HOL4 theories. The HOL4 theories that are of particular interest to the current work include the theory of Booleans, lists, positive integers and real analysis, measure and probability theory. One of the primary motivations of selecting the HOL4 theorem prover for our work was to benefit from these existing mathematical theories.

The formal proofs in HOL4 can be conducted in both forward and backward manner. In the forward proof method, the previously proven theorems are used along with the inference rules to verify the desired theorem. The forward proof method usually requires the exact details of a proof in advance and is thus not very straightforward. In the backward proof method, ML functions called tactics are used to break the main proof goals into simple sub-goals. Some of these intermediate sub-goals can be discharged by matching axioms or assumptions or by applying built-in automatic decision procedures. This process is repeated until all the sub goals are discharged, which concludes the proof for the given theorem.

Formalization of probabilistic algorithms

Building upon the recently developed measure-theoretic formalization of probability theory [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF], we can conduct formal probabilistic analysis [START_REF] Mashkoor | Formal probabilistic analysis of cyber-physical transportation systems[END_REF] in the sound core of a higher-order logic theorem prover. The system can be modelled as a probabilistic algorithm where its randomized components can be specified using appropriate random variables and its probabilistic and statistical properties can be verified using the proven probability axioms. The ability of higher-order logic to formalize continuous and randomized systems, and to verify all sorts of probabilistic and statistical properties makes it the meritorious approach for the formal probabilistic analysis of MCS.

The unpredictable components of a system can be modelled as higher-order logic functions that make random choices by using the required number of bits from an infinite sequence of random bits B ∞ . These functions return the result along with the remaining portion of the infinite Boolean sequence to be used by other programs. Thus, the data type of a probabilistic algorithm that takes a parameter of type α and returns a value of type β is:

F : α → B ∞ → β × B ∞
For illustration, consider the example of a Bernoulli( 12 ) random variable that returns 1 or 0 with equal probability 1 2 . It can be formally modelled as follows:

bit s = (if shd s then 1 else 0, stl s)

where variable s represents the infinite Boolean sequence and functions shd and stl return the head and tail of their sequence argument, respectively. Probabilistic algorithms can be expressed in a more compact way without explicitly mentioning the Boolean sequence that is passed around by using more general state-transforming monads where the states are the infinite Boolean sequences.

∀ a s. unit a s = (a,s) ∀ f g s. bind f g s = g (fst (f s)) (snd (f s))

The unit operator is used to lift values to the monad, and the bind is the monadic analogue of function application. The function bit can be defined using the monadic notation as:

bit monad = bind sdest (λb.if b then unit 1 else unit 0)

where sdest provides the head and tail of a sequence as a pair (shd s, stl s).

Hurd [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF] constructed a probability space on infinite Boolean sequence and formalized a measure theoretic formalization of probability theory in the higherorder-logic theorem prover HOL. Building upon these foundations, we can verify all the basic laws of probability as well as probabilistic properties of any algorithm that is specified using the infinite Boolean sequence. For example, we can verify the Probability Mass Function (PMF) of the function bit as:

P {s | fst (bit s) = 1} = 1 2
where the HOL function fst selects the first component of a pair and P is the probability function that maps sets of infinite Boolean sequences to real numbers between 0 and 1 .

Just like the bit function, we can formalize and verify any random variable using the above mentioned approach. For example, the Bernoulli and Uniform random variables have been verified using the following PMF relations [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF]: The function ber rv models an experiment with two outcomes; 1 and 0, whereas p represents the probability of obtaining a 1. Similarly, the function unif rv assigns equal probability to each element in the set {0, 1, • • • , (m -1)} and thus ranges over a finite number of positive integers. Such pre-formalized random variables and their proven properties greatly facilitate the analysis of MCS as, in most cases, the unpredictable nature of its components can be expressed in terms of well-known random variables. Expectation theory also plays a vital role in probabilistic analysis as it is lot easier to judge performance issues based on the average of a characteristic, which is a single number, rather than its distribution function. The expectation of a discrete random variable can be defined as a higher-order logic function as follows [START_REF] Hasan | Using theorem proving to verify expectation and variance for discrete random variables[END_REF]:

Definition 1: Expectation of Discrete Random Variables ∀R. expec R = suminf (λn.n * P {s | fst (R s) = n})
where suminf represents the HOL formalization of the infinite summation of a real sequence f , i.e., lim k→∞ k n=0 f (n). The function expec can be used to verify the expectation of any discrete random variable that attains values in positive integers. For example, the higher-order logic theorem corresponding to the expectation of the Bernoulli random variable has been formally verified in [START_REF] Hasan | Using theorem proving to verify expectation and variance for discrete random variables[END_REF] as follows:

Lemma 3: Expectation of Bernoulli(p) Random Variable ∀p. 0 ≤ p ∧ p ≤ 1 ⇒ expec (λs.bern rv p s) = p
where (λx.t) represents a lambda abstraction function in HOL that maps its argument x to t(x).

The continuous random variables can also be formalized by building upon the above mentioned measure-theoretic formalization of probability theory. The main idea behind their formalization is to transform a Standard Uniform random variable to other continuous random variables based on the principles of the non-uniform random number generation [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. The Standard Uniform random variable can be modeled by using the formalization approach for discrete random variables and the formalization of the mathematical concept of limit of a real sequence [START_REF] Harrison | Theorem Proving with the Real Numbers[END_REF]:

lim n→∞ (λn. n-1 k=0 ( 1 2 ) k+1 X k ) (1)
where X k denotes the outcome of the k th random bit; T rue or F alse represented as 1 or 0, respectively. This formalization [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF] is used along with the formalization of the CDF function to formally verify the correctness of the Inverse Transform Method (ITM), i.e., a well known non-uniform random generation technique for generating non-uniform random variables for continuous probability distributions for which the inverse of the CDF can be represented in a closed mathematical form. Formally, it can be verified for a random variable X with CDF F using the Standard Uniform random variable U as follows [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF].

P r(F -1 (U ) ≤ x) = F (x) (2)
The formalized Standard Uniform random variable can now be used to formally specify any continuous random variable for which the inverse of the CDF can be expressed in a closed mathematical form as X = F -1 (U ). Whereas, its CDF can be verified based on simple arithmetic reasoning, using the formally verified ITM, given in Equation ( 2). This approach has been successfully utilized to formalize and verify Exponential, Uniform, Rayleigh and Triangular random variables [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF].

The expectation for a continuous random variable X is defined on a probability space (Ω, Σ, P ) [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF], is as follows:

E[X] = Ω XdP (3)
where the integral represents the Lebesgue integral. In order to facilitate the formal reasoning about statistical properties of continuous random variables, the following two alternate expressions for the expectation have been verified [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. The first expression is for the case when the given continuous random variable

X is bounded in the positive interval [a, b] E[X] = lim n→∞ 2 n -1 i=0 (a + i 2 n (b -a)) P a + i 2 n (b -a) ≤ X < a + i + 1 2 n (b -a) (4)
and the second one is for an unbounded positive random variable.

E[X] = lim n→∞ n2 n -1 i=0 i 2 n P i 2 n ≤ X < i + 1 2 n + nP(X ≥ n) (5)
Both of the above expressions do not involve any concepts from Lebesgue integration theory and are based on the well-known arithmetic operations like summation, limit of a real sequence, etc. Thus, users can simply utilize them, instead of Equation ( 3), to reason about the expectation properties of their random variables and gain the benefits of the original Lebesgue based definition. The formal verification details for these expressions are given in [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. These expressions are further utilized to verify the expected values of Uniform, Triangular and Exponential random variables [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. The above mentioned formalization plays a pivotal role for the formal probabilistic analysis of MCS. In the next section, we illustrate the usefulness and practical effectiveness of the foundational formalization, presented in this section, by providing a step-wise approach for analyzing a MCS using HOL4.

The triptych analysis approach

Figure 2 depicts the proposed triptych formal probabilistic analysis approach. It primarily builds upon the existing formalization of probability theory (including the infinite Boolean sequence space), and commonly used random variables and their proved properties. The approach is as follows:

1. The first step is to formalize the true behaviour of the given MCS including its unpredictable and continuous components in higher-order logic. The randomized behaviours would be captured using appropriate discrete [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF] and continuous random variables [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF] and the continuous aspects can be modeled using the formalized real numbers [START_REF] Harrison | Theorem Proving with the Real Numbers[END_REF]. 2. The second step is to utilize the formally specified model, i.e., the higherorder-logic function that represents the behavior of the given MCS, to formally express desired system properties as higher-order logic proof goals. Due to the random nature of the model, the properties are also either probabilistic or statistical. For this purpose, the existing higher-order-logic functions of probability [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF], expectation and variance [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF] can be utilized. 3. The third and final step is to formally verify the developed higher-order logic proof goals using a theorem prover. The existing theorems corresponding to probability distribution functions, expectation and variance of commonly used random variables [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF][START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF] greatly facilitate in minimizing the required user interaction to prove these goals.

We now illustrate the utilization and practical effectiveness of this approach by providing a simple case study.

Collision detection in multi-robot systems: a case study

Our case study is based on multi-robot systems described in [START_REF] Parker | Multiple mobile robot teams, path planning and motion coordination in[END_REF]. The use of such systems is on rise in the development of MCS. They offer numerous advantages over single-robot systems, e.g., more spacial coverage, redundancy, reconfigurability and throughput. However, the design of these robots involves many challenges due to their potentially unknown and dynamic environments. Moreover, due to their autonomous nature, avoiding collisions with other robots of the system is also a major challenge. The number of robots and the arena size is chosen at the design time such that potential collisions are minimized. However, estimating these parameters is not a straightforward task due to the unpredictable nature of the potential collisions. Probabilistic techniques can help in this realm.

We are interested in finding the average number of collisions for the given system with k mobile robots moving in an arena of n distinct locations. A collision happens when two or more robots are on the same location at the same time. The randomized behavior of the collision can be modelled as a Bernoulli random variable X with two outcomes, 1 or 0, as follows:

X ij =
1 if robot i and j are using the same location; 0 otherwise. [START_REF] Panesar-Walawege | Characterizing the chain of evidence for software safety cases: A conceptual model based on the IEC 61508 standard[END_REF] corresponding to each pair (i, j) of the k robots in the group such that 0 ≤ i ≤ j < k. We can reasonably assume that the location of any robot at any particular time instant is uniformly and independently distributed among the n available slots. Under these conditions, the total number of collisions can be computed as follows:

k-1 i=0 k-1 j=i+1 X ij (7)
The formal probabilistic analysis of the above mentioned collision detection problem can now be done by following the triptych approach outlined in Figure 2.

The first step is to formalize the system in higher-order logic. The behaviour of the given system can be expressed in terms of the Bernoulli and Uniform random variables using the following recursive functions. The functions col detect helper and col detect model the inner and outer summations of Equation ( 7), respectively. The variable bern rv models the randomness given in Equation ( 6), with the probability of success equal to the probability of the event when two independent Uniform(n) random variables generate the same values. The two Uniform random variables in the above definition correspond to the locations of two robots in the system based on the above mentioned assumptions. The independence between the two Uniform(n) random variables is ensured because of the fact that the second uniform random variable on the right-hand-side of the equality utilizes the remaining portion of the infinite Boolean sequence from the first Uniform(n) random variable that is on the left-hand-side of the equality. Thus, the function col detect accepts two parameters k and n, which represents the number of robots in the system and the number of available locations in the areana, respectively, and it returns the total number of pairs of robots having the same location at a given time, which is the number of collisions. The second step is to formalize the property of interest in higher-order logic. We are interested in the average number of collisions and that can be expressed using the expectation function, given in Definition 1, as follows:

Theorem 1: Average Number of Collisions ∀k n. 0 < n ∧ 2 ≤ k ⇒ expec (col detect k n) = k(k-1) 2n
The assumptions in the above theorem ensure that the number of locations are more than 0 and the population is at least 2 in order to have 1 pair at minimum. The third step is to verify the proof goal in a theorem prover. We verify it using the HOL4 theorem prover. The interactive reasoning process was primarily based on performing induction on the variable k, Lemmas 1, 2 and 3, and some formally verified probability theory laws like the linearity of expectation. The manually developed proof script for this verification relied heavily on already existing formalizations of probability theory [START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF] and random variables [START_REF] Hasan | Formal Probabilistic Analysis: A Higher-order Logic based approach[END_REF]. Theorem 1 provides very useful insights into the collision detection in a multi-robot system. It can be clearly observed that the expected number of collisions would be less than 1 if k(k -1) ≤ 2n. This means that if we have √ 2n + 1 or more robots in the system, then on average we can expect at least one collision.

The above example clearly demonstrates the effectiveness of the proposed approach in analysing MCS. Due to the formal nature of the model and the inherent soundness of higher-order logic theorem proving, we have been able to verify the desired property with full precision. Same results could not be obtained using simulation or animation techniques, neither the problem could be described as a Markov chain and thus could not be analysed using a probabilistic model checker. Another distinguishing feature of Theorem 1 is its generic nature and the universal quantification on all the variables. Thus, the theorem can be instantiated with any possible values to obtain the average number of collisions for any specific system. Finally, the theorem explicitly provides all the assumptions under which it has been verified. This is usually not the case when we are verifying theorems by hand using the traditional paper-and-pencil proof methods as mathematicians may forget to pen down all the required assumptions that are required for the validity of their analysis. These missing assumptions may lead to erroneous designs as well and thus the proposed approach overcomes this problem.

These additional benefits have been gained at the cost of time and effort spent while formalizing the system and formally reasoning about its properties, by the user. But, the fact that we were building on top of already verified results in the theorem prover helped significantly in this regard as the analysis, described in this section, only consumed approximately 500 lines of HOL code and 30 man-hours by an expert HOL user.

Conclusion

We have presented a framework that enables us to unify the formal verification technique with quantitative reasoning for the engineering of safe and reliable MCS. The point is that in addition to analyse the absolute correctness, which at times is not possible, a probabilistic analysis can provide a better insight about the model. In this fashion, it is easier for stakeholders to obtain a probability of occurrence of a hazard in terms of the likelihood of components failures. We can now provide an evidence, as a certification argument, that the probability of violation of a safety requirement is sufficiently and acceptably small. Moreover, given the soundness of higher-order logic theorem proving, the analysis results are completely reliable. Similarly, the high expressiveness of higher-order logic enables us to analyse a wide range of MCS. Thus, the proposed approach can be beneficial for the analysis of industrial MCS where safety and reliability are coveted system traits.

Fig. 1 .

 1 Fig. 1. A typical MCS

Lemma 1 :Lemma 2 :

 12 PMF of Bernoulli(p) Random Variable ∀p. 0 ≤ p ∧ p ≤ 1 ⇒ P {s | fst (bern rv p s)=1} = p PMF of Uniform(m) Random Variable ∀m x. x < m ⇒ P {s | fst (unif rv m s) = x} = 1 m

Fig. 2 .

 2 Fig. 2. The triptych probabilistic analysis of MCS

Definition 2 :

 2 Collision Detection in Multi-Robot System (∀ n. col detect helper 0 n = unit 0) ∧ (∀ k n. col detect helper(k+1) n = bind (col detect helper k n) (λa. bind (bern rv (P{s | fst(unif rv n s) = fst(unif rv n (snd (unif rv n s)))})) (λb. unit (b + a)))) (∀ n. col detect 0 n = unit 0) ∧ (∀ k n. col detect (k + 1) n = bind (col detect k n) (λa. bind (col detect helper k n) (λb. unit (b + a))))

http://cps-vo.org/group/scc

Acknowledgement

This paper has been partially written with the support of the project Vertical Model Integration (VMI) that is financed within the program "Regionale Wettbewerbsfähigkeit O Ö 2007-2013" by the European Fund for Regional Development as well as the State of Upper Austria.