How to use HYPE to model hybrid systems: a railway crossing example

V.C. Galpin

SICSA Workshop on Probabilistic Modelling, Model-Checking and Planning, University of Glasgow, December 2010


This presentation demonstrates how to model a train gate system in HYPE, a process algebra for hybrid systems. These systems have both continuous and discrete behaviour. In the case of the train gate, the train and the gate show continuous behaviour as they move, and the controller is discrete. This example will illustrate the fine-grained modelling style of HYPE and how compositionality is beneficial when changes are required. The notion of an I-graph is introduced and this enables a checking for whether an infinite number of simultaneous events occurs. 

Slides - PDF