We addressed the problem of integrating behavioural types to reason about properties of applications running on Actyx platform. In particular, we developed a formal model for the Actyx platform. The main feature of the model is that components (fishes) interact via a weak consistent shared stated; there are no synchronisation mechanisms. As such the expected and observed behaviour of the system can differ. We have explored alternatives for combining static & dynamic techniques based on behavioural description of components to single out execution points in which such discrepancies may occur.

Leave a Reply