Title of talk: Can we Communicate? Using Dynamic Logic to Verify Featured Team Automata

Abstract

Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Featured team automata support variability by describing families of concrete product models for specific configurations determined by feature selection. Given a (featured) team automaton one can reason over communication-safety properties, like receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied), but doing so product-wise quickly becomes impractical. Therefore, we lift these notions to the level of family models and show how to identify such communication properties. However, the purely semantic nature of communication properties is a serious burden in practice, making it challenging to automatically verify such properties in concrete cases: one has to go through all reachable states of networks of interacting automata with large state spaces and check compliance for all requirements at each state. Our solution is to provide the first logical characterisation of communication properties for team automata (and subsumed models) using test-free propositional dynamic logic and, subsequently, to use this characterisation to actually verify communication properties by using available model-checking tools for dynamic logic. An open-source prototypical tool supports the developed theory, using a transformation to interact with the mCRL2 toolset for model checking. Future work concerns generalising our logical characterisation and the tool to deal with variability and family-based compatibility checking for featured team automata.