Safety by Construction: Well-behaved Scalable Systems

Abstract—This paper presents a formal framework that provides construction principles for well-behaved scalable systems, such that starting with a prototype system satisfying a desired safety property result in a scalable system satisfying a corresponding safety property, called scalable safety property. With respect to different aspects of scalability, the focus of this work is on property preserving structural scalability. At that, we consider systems composed of a varying set of individual components where individual com-ponents of the same type behave in the same manner, which is characteristic for the type. The respective properties can rely on specific component types and a specific number of individual components but not on the specific individuality of the components. Well-behaved scalable systems are characterised by those systems, which fulfil such a kind of property if already one prototype system (depending on the property) fulfils that property. Sufficient conditions to specify a certain kind of basic well-behaved scalable systems are given and it is shown, how to construct more com-plex systems by the composition of several synchro-nisation conditions. Scalable safety properties can be used to express privacy policies as well as security and dependability requirements. It is demonstrated, how the parameterised problem of verifying such a property is reduced to a finite state problem for well-behaved scalable systems. The formal framework for well-behaved scalable systems is developed in terms of prefix closed formal languages and alphabetic lan-guage homomorphisms. Keywords-uniformly parameterised systems, mono-tonic parameterised systems, behaviour-abstraction, self-similarity of behaviour, privacy policies, scalable safety properties. I