Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap ....Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap between the informal requirements and the starting point of formally verifiable development. To minimise this gap, we develop a particularly expressive specification language, a calculus for stepwise refinement from such specifications down to distributed systems, and an automated tool for checking and supporting refinement steps in the calculus.Read moreRead less