## Abstract

Because interlocking systems are highly safety-critical complex systems, their automated safety verification is an active research topic investigated by several groups, employing verification techniques to produce important cost and time savings in their certification. However, such systems also pose a big challenge to current verification methodologies, due to the explosion of state space size as soon as large, if not medium sized, multi-station systems have to be controlled.

For these reasons, verification techniques that exploit locality principles related to the topological layout of the controlled system to split in different ways the state space have been investigated. In particular, compositional approaches divide the controlled track network in regions that can be verified separately, once proper assumptions are considered on the way the pieces are glued together.

Basing on a successful method to verify the size of rather large networks, we propose a compositional approach that is particularly suitable to address multi-station interlocking systems which control a whole line composed of stations linked by mainline tracks. Indeed, it turns out that for such networks, and for the adopted verification approach, the verification effort amounts just to the sum of the verification efforts for each intermediate station and for each connecting line.

For these reasons, verification techniques that exploit locality principles related to the topological layout of the controlled system to split in different ways the state space have been investigated. In particular, compositional approaches divide the controlled track network in regions that can be verified separately, once proper assumptions are considered on the way the pieces are glued together.

Basing on a successful method to verify the size of rather large networks, we propose a compositional approach that is particularly suitable to address multi-station interlocking systems which control a whole line composed of stations linked by mainline tracks. Indeed, it turns out that for such networks, and for the adopted verification approach, the verification effort amounts just to the sum of the verification efforts for each intermediate station and for each connecting line.

Original language | English |
---|---|

Title of host publication | Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) : Discussion, Dissemination, Applications - Part II |

Publisher | Springer |

Publication date | 2016 |

Pages | 279-293 |

ISBN (Print) | 978-3-319-47168-6 |

ISBN (Electronic) | 978-3-319-47169-3 |

DOIs | |

Publication status | Published - 2016 |

Event | 7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7 |

### Conference

Conference | 7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation |
---|---|

Number | 7 |

Country/Territory | Greece |

City | Corfu |

Period | 10/10/2016 → 14/10/2016 |

Series | Lecture Notes in Computer Science |
---|---|

Volume | 9953 |

ISSN | 0302-9743 |